mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
gfse: text mode tweaks
This commit is contained in:
@@ -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;
|
||||
|
||||
@@ -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)])
|
||||
|
||||
@@ -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"
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user