GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-25 12:32:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

Add first demo of new syntax editor

Browse Source 
As part of the GF cloud stuff, it can be accessed from
http://cloud.grammaticalframework.org/syntax-editor/editor.html
This commit is contained in:
john.j.camilleri
2012-11-13 15:14:49 +00:00
parent b6f392b4e1
commit 7a69d9d5e5
9 changed files with 1021 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

43
src/www/syntax-editor/editor.html Normal file
View File

@@ -0,0 +1,43 @@
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<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" />
</head>
<body>
<h2>Syntax Editor</h2>
<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>
<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">
// Code taken from minibar_online.js
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>
</body>
</html>