blob: bb6b49fa896e7aed6d9ec1ffcff817d58374978d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
<!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="editor.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="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>
</body>
</html>
|
