diff options
| author | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-22 12:45:20 +0000 |
|---|---|---|
| committer | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-22 12:45:20 +0000 |
| commit | bac6b7fe6438d06fab3451263d4d94e9055f6f88 (patch) | |
| tree | abcb68ac3df3fa2e17fd3ba38cc9f5f899c9b913 /src/www/syntax-editor/editor.html | |
| parent | 486a510611b72d4daf551f30156fa59608d099af (diff) | |
Syntax editor: can now load minibar (in-place) from a linearised tree
Diffstat (limited to 'src/www/syntax-editor/editor.html')
| -rw-r--r-- | src/www/syntax-editor/editor.html | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/src/www/syntax-editor/editor.html b/src/www/syntax-editor/editor.html index 36045957c..1d4cc401c 100644 --- a/src/www/syntax-editor/editor.html +++ b/src/www/syntax-editor/editor.html @@ -9,7 +9,7 @@ </head> <body class=syntax_editor> <h2>Syntax Editor</h2> - <div id="editor"></div> + <div id="editor" class="test"></div> <noscript>This page doesn't works unless JavaScript is enabled.</noscript> <hr /> @@ -17,26 +17,23 @@ John J. Camilleri, November 2012 </small> + <!-- Common --> <script type="text/javascript" src="../js/support.js"></script> <script type="text/javascript" src="../js/pgf_online.js"></script> + + <!-- Editor --> <script type="text/javascript" src="ast.js"></script> <script type="text/javascript" src="editor_menu.js"></script> <script type="text/javascript" src="editor.js"></script> - <script type="text/javascript"> - var server_options = { - // grammars_url: "http://www.grammaticalframework.org/grammars/", - grammars_url: "http://localhost:41296/grammars/", - } - var editor_options = { - target: "editor" - } - if(/^\?\/tmp\//.test(location.search)) { - var args=decodeURIComponent(location.search.substr(1)).split(" ") - if(args[0]) server_options.grammars_url=args[0]; - } - var server = pgf_online(server_options); - var editor = new Editor(server, editor_options); - </script> + + <!-- Minibar --> + <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> + + <!-- Get us rolling! --> + <script type="text/javascript" src="editor_online.js"></script> </body> </html> |