diff options
| author | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-23 15:03:36 +0000 |
|---|---|---|
| committer | john.j.camilleri <john.j.camilleri@chalmers.se> | 2012-11-23 15:03:36 +0000 |
| commit | d9867893f83c801b37a4fe0acf0fa7289e857031 (patch) | |
| tree | 33af1fe9716a507a6047148441ae9a749e238def /src/www/syntax-editor/editor.html | |
| parent | 9e430184ba5063110e5ec72c6137e4d38f92e206 (diff) | |
Syntax editor: now uses common GrammarManager object
Diffstat (limited to 'src/www/syntax-editor/editor.html')
| -rw-r--r-- | src/www/syntax-editor/editor.html | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/www/syntax-editor/editor.html b/src/www/syntax-editor/editor.html index b9cfa0ec2..403b4bbeb 100644 --- a/src/www/syntax-editor/editor.html +++ b/src/www/syntax-editor/editor.html @@ -7,18 +7,20 @@ <link rel="stylesheet" type="text/css" href="../minibar/minibar.css" /> <link rel="stylesheet" type="text/css" href="editor.css" /> </head> -<body class=syntax_editor> +<body class="syntax-editor"> <h2>Syntax Editor</h2> - <div id=minibar></div> - <div id=editor></div> + <div id="minibar"></div> + <div id="editor"></div> <noscript>This page doesn't works unless JavaScript is enabled.</noscript> <hr /> <small class="modtime"> John J. Camilleri, November 2012 </small> + <div id="debug" class="hidden"></div> <!-- Common --> + <script type="text/javascript" src="../js/grammar_manager.js"></script> <script type="text/javascript" src="../js/support.js"></script> <script type="text/javascript" src="../js/pgf_online.js"></script> |