GF cloud: work on syntax editor integration

+ The syntax editor is now accessible from the Simple Translaton Tool.
+ The minibar now automatically provides access to the syntax editor (provided
  the necessary JavaScript files and style sheets have been loaded).
+ Preparations for making the syntax editor accessible from the grammar editor.

3 files changed, 7 insertions, 4 deletions

diff --git a/src/www/gfse/editor.css b/src/www/gfse/editor.css
index fa5d21306..c6973f2d5 100644
--- a/src/www/gfse/editor.css
+++ b/src/www/gfse/editor.css
@@ -129,7 +129,7 @@ textarea.text_mode {
     width: 99%;
 }
 
-div#minibar {
+div#minibar, div#syntax_editor {
     border: 1px solid black;
     padding: 5px;
     background: #ccc url("../minibar/brushed-metal.png");
diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js
index f3f5bf98f..11ba18b37 100644
--- a/src/www/gfse/editor.js
+++ b/src/www/gfse/editor.js
@@ -370,6 +370,7 @@ function compile_button(g,err_ind) {
 function minibar_button(g,files,err_ind,comp_btn) {
     var b2;
     var minibar_div=div_id("minibar");
+    var editor_div= div_id("syntax_editor");
 
     function page_overlay(inner) {
 	return wrap_class("table","page_overlay",tr(td(inner)))
@@ -530,7 +531,7 @@ function minibar_button(g,files,err_ind,comp_btn) {
 
     function goto_minibar() {
 	clear(files);
-	files.appendChild(minibar_div);
+	appendChildren(files,[minibar_div,editor_div]);
 	var online_options={grammars_url: local.get("dir")+"/",
 			    grammar_list: [g.basename+".pgf"]}
 	var pgf_server=pgf_online(online_options)
diff --git a/src/www/gfse/index.html b/src/www/gfse/index.html
index cfa89762d..12f50ef7e 100644
--- a/src/www/gfse/index.html
+++ b/src/www/gfse/index.html
@@ -33,23 +33,25 @@ This page does not work without JavaScript.
 <hr>
 <div class=modtime><small>
 HTML
-<!-- hhmts start -->Last modified: Wed Apr  3 20:30:24 CEST 2013 <!-- hhmts end -->
+<!-- hhmts start -->Last modified: Fri Apr 12 20:22:01 CEST 2013 <!-- hhmts end -->
 </small></div>
 <a href="about.html">About</a>
 <pre id=debug></pre>
 <script type="text/javascript" src="config.js"></script> <!-- optional -->
 <script type="text/javascript" src="../js/support.js"></script>
+<script type="text/JavaScript" src="../js/pgf_online.js"></script>
 <script type="text/javascript" src="../js/localstorage.js"></script>
+
 <script type="text/javascript" src="localstorage.js"></script>
 <script type="text/javascript" src="gf_abs.js"></script>
 <script type="text/javascript" src="example_based.js"></script>
 <script type="text/javascript" src="sort.js"></script>
 <script type="text/javascript" src="cloud2.js"></script>
 <script type="text/javascript" src="editor.js"></script>
+
 <script type="text/JavaScript" src="../minibar/minibar.js"></script>
 <script type="text/JavaScript" src="../minibar/minibar_input.js"></script>
 <script type="text/JavaScript" src="../minibar/minibar_translations.js"></script>
 <script type="text/JavaScript" src="../minibar/minibar_support.js"></script>
-<script type="text/JavaScript" src="../js/pgf_online.js"></script>
 </body>
 </html>