From 69066a7ecdfef73cdc03e1de896c7cd608f1fb2b Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Fri, 24 Feb 2012 15:16:37 +0000
Subject: [PATCH] gfse: text mode tweaks

---
 src/www/gfse/editor.css | 5 +++++
 src/www/gfse/editor.js  | 1 +
 src/www/gfse/gf_abs.js  | 4 ++--
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/www/gfse/editor.css b/src/www/gfse/editor.css
index 100e5b35b..2c930d849 100644
--- a/src/www/gfse/editor.css
+++ b/src/www/gfse/editor.css
@@ -99,6 +99,11 @@ li { margin-top: 0.5ex; margin-bottom: 0.5ex; }
 
 div.compiler_output .back_to_editor { display: none; }
 
+textarea.text_mode {
+    /*font-family: inherit; font-size: inherit;*/
+    width: 99%;
+}
+
 div#minibar {
     border: 1px solid black;
     padding: 5px;
diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js
index 03cef9dec..64b44e36c 100644
--- a/src/www/gfse/editor.js
+++ b/src/www/gfse/editor.js
@@ -536,6 +536,7 @@ function text_mode(g,file,ix) {
 	var mode_button=div_class("right",[button("Guided mode",switch_to_guided_mode)])
 	clear(file)
 	appendChildren(file,[mode_button,ta])
+	ta.style.height=ta.scrollHeight+"px";
 	ta.focus();
     }
     var mode_button=div_class("right",[button("Text mode",switch_to_text_mode)])
diff --git a/src/www/gfse/gf_abs.js b/src/www/gfse/gf_abs.js
index 2809b2e32..2530a20db 100644
--- a/src/www/gfse/gf_abs.js
+++ b/src/www/gfse/gf_abs.js
@@ -271,10 +271,10 @@ function show_concrete(g) {
 	    +show_extends((g.extends || []).map(conc_extends(conc)))
             +show_opens(conc.opens)
 	    +"{\n\nflags coding = utf8 ;\n\n"
-	    +show_params(conc.params)
 	    +show_lincats(conc.lincats)
-	    +show_opers(conc.opers)
 	    +show_lins(conc.lins)
+	    +show_params(conc.params)
+	    +show_opers(conc.opers)
 	    +"}\n"
     }
 }