RGL Browser: now includes Syntax Editor tab!

lib/doc/browse/index.html

@@ -11,6 +11,8 @@
     <link rel="stylesheet" href="layout-default-latest.css" />
     <link rel="stylesheet" href="style.css">
 
+    <link rel="stylesheet" type="text/css" href="http://cloud.grammaticalframework.org/syntax-editor/editor.css" />
+
     <script type="text/javascript" src="http://code.jquery.com/jquery-1.10.2.min.js"></script>
     <script type="text/javascript" src="http://code.jquery.com/ui/1.10.3/jquery-ui.min.js"></script>
     <script type="text/javascript" src="jquery.layout-latest.js"></script>
@@ -65,6 +67,35 @@
         <table id="results"></table>
       </div><!-- panel api -->
 
+      <!-- Syntax editor -->
+      <script type="text/javascript" src="http://cloud.grammaticalframework.org/js/grammar_manager.js"></script>
+      <script type="text/javascript" src="http://cloud.grammaticalframework.org/js/support.js"></script>
+      <script type="text/JavaScript" src="http://cloud.grammaticalframework.org/js/localstorage.js"></script>
+      <script type="text/javascript" src="http://cloud.grammaticalframework.org/js/pgf_online.js"></script>
+      <script type="text/javascript" src="http://cloud.grammaticalframework.org/syntax-editor/ast.js"></script>
+      <script type="text/javascript" src="http://cloud.grammaticalframework.org/syntax-editor/editor_menu.js"></script>
+      <script type="text/javascript" src="http://cloud.grammaticalframework.org/syntax-editor/editor.js"></script>
+      <script type="text/javascript">
+      $(document).ready(function(){
+        var server = pgf_online({
+          grammars_url: "http://www.grammaticalframework.org/grammars/"
+        });
+        var gm = new GrammarManager(server, {
+          initial: {
+            grammar: "http://www.grammaticalframework.org/grammars/LibraryBrowser.pgf",
+            startcat: "Utt"
+          }
+        });
+        var editor = new Editor(gm, {
+          target: "editor",
+          show_grammar_menu: false
+        });
+      });
+      </script>
+
+      <div id="editor" class="panel editor">
+      </div><!-- panel editor -->
+
       <div id="help" class="panel help">
 
         <h3>About</h3>
@@ -119,11 +150,11 @@
           <a class="tab code" href="#code">code</a>
         </span>
         <a class="tab api" href="#api">API</a>
+        <a class="tab editor" href="#editor">Tree Builder</a>
         <a class="tab help" href="#help">Help</a>
         <a class="synopsis" href="http://www.grammaticalframework.org/lib/doc/synopsis.html" target="_blank">Synopsis</a>
       </div>
 
-
       </header>
 
       <footer id="footer">

src/www/syntax-editor/editor_menu.js

@@ -11,6 +11,7 @@ function EditorMenu(editor,opts) {
         show_to_menu: true,
         show_random_button: true,
         show_import: true,
+        show_debug: false,
     }
 
     // Apply supplied options
@@ -92,7 +93,9 @@ function EditorMenu(editor,opts) {
         ]);
     }
 
-    appendChildren(t.container, [t.ui.debug_toggle]);
+    if (t.options.show_debug) {
+        appendChildren(t.container, [t.ui.debug_toggle]);
+    }
 
     /* --- Client state initialisation -------------------------------------- */
     this.editor = editor;