diff options
| author | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-20 13:56:56 +0000 |
|---|---|---|
| committer | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-20 13:56:56 +0000 |
| commit | 09c4f8410eba31bafc567a7d4115d62681665938 (patch) | |
| tree | 929de876163c301a6d3bea28a59d018c3a11eda7 /src/www/syntax-editor/editor.html | |
| parent | 3eaeaed8fd741bb1f33c76032e7292df08b35a9f (diff) | |
Syntax editor: update to use common js files
Diffstat (limited to 'src/www/syntax-editor/editor.html')
| -rw-r--r-- | src/www/syntax-editor/editor.html | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/www/syntax-editor/editor.html b/src/www/syntax-editor/editor.html index d641998ab..bb6b49fa8 100644 --- a/src/www/syntax-editor/editor.html +++ b/src/www/syntax-editor/editor.html @@ -5,7 +5,7 @@ <link rel="author" href="http://www.grammaticalframework.org/~john/" title="John J. Camilleri"> <title>Syntax Editor</title> <link rel="stylesheet" type="text/css" href="http://cloud.grammaticalframework.org/minibar/minibar.css" /> - <link rel="stylesheet" type="text/css" href="ui/style.css" /> + <link rel="stylesheet" type="text/css" href="editor.css" /> </head> <body> <h2>Syntax Editor</h2> @@ -17,16 +17,15 @@ John J. Camilleri, November 2012 </small> - <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/ast.js"></script> - <script type="text/javascript" src="js/editor_menu.js"></script> - <script type="text/javascript" src="js/editor.js"></script> + <script type="text/javascript" src="../js/support.js"></script> + <script type="text/javascript" src="../js/pgf_online.js"></script> + <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"> - // Code taken from minibar_online.js var server_options = { - //grammars_url: "http://www.grammaticalframework.org/grammars/", - //grammars_url: "http://localhost:41296/grammars/", + // grammars_url: "http://www.grammaticalframework.org/grammars/", + grammars_url: "http://localhost:41296/grammars/", } var editor_options = { target: "editor" |