From 8f257940134af892f57dd85dae9270bd7ffcefd0 Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Thu, 25 Jul 2013 07:36:34 +0000
Subject: [PATCH] RGL Browser: now includes Syntax Editor tab!

---
 doc/browse/index.html | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/doc/browse/index.html b/doc/browse/index.html
index a552bc097..78501ba52 100644
--- a/doc/browse/index.html
+++ b/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">