diff --git a/src/www/js/grammar_manager.js b/src/www/js/grammar_manager.js
new file mode 100644
index 000000000..a2bf3b830
--- /dev/null
+++ b/src/www/js/grammar_manager.js
@@ -0,0 +1,173 @@
+/* --- Grammar Manager object ----------------------------------------------- */
+/*
+This object stores the state for:
+- grammar
+- startcat
+- languages
+
+Hooks which actions can be hooked to:
+- onload
+- change_grammar
+- change_startcat
+- change_languages
+
+*/
+function GrammarManager(server,opts) {
+ var t = this;
+ /* --- Configuration ---------------------------------------------------- */
+
+ // default values
+ this.options = {
+ initial: {}
+ };
+ this.hooks = {
+ onload: [
+ function(gm){ debug("default action: onload"); }
+ ],
+ change_grammar: [
+ function(grammar){ debug("default action: change grammar"); }
+ ],
+ change_startcat: [
+ function(startcat){ debug("default action: change startcat"); }
+ ],
+ change_languages: [
+ function(languages){ debug("default action: change languages"); }
+ ]
+ }
+
+ // Apply supplied options
+// if(opts) for(var o in opts) this.options[o]=opts[o];
+
+ /* --- Client state initialisation -------------------------------------- */
+ this.server = server;
+ this.grammar = null; // current grammar
+ // this.grammars=[];
+ // this.grammar_dirs=[];
+ this.startcat = null; // current startcat
+ this.languages = []; // current languages (empty means all langs)
+
+ /* --- Main program, this gets things going ----------------------------- */
+ this.init=function(){
+ this.server.get_grammarlists(bind(this.onload,this));
+ }
+ this.init();
+}
+
+//
+//GrammarManager.prototype.update_grammar_list=function(dir,grammar_names,dir_count) {
+GrammarManager.prototype.onload=function(dir,grammar_names,dir_count) {
+ var t=this;
+ t.grammars=[];
+ t.grammar_dirs=[];
+ t.grammar_dirs.push(dir);
+ t.grammars=t.grammars.concat(grammar_names.map(function(g){return dir+g}));
+ var grammar0=t.options.initial.grammar || t.grammars[0];
+ t.change_grammar(grammar0);
+
+ // Execute hooked actions
+ t.run_actions("onload",dir,grammar_names,dir_count);
+}
+
+/* --- Registering / unregistering actions to hooks ------------------------- */
+
+GrammarManager.prototype.register_action=function(hook,action) {
+ this.hooks[hook].push(action);
+}
+
+GrammarManager.prototype.unregister_action=function(hook,action) {
+ // TODO!
+}
+
+// Execute actions for a given hook
+// TODO: any number of arguments
+GrammarManager.prototype.run_actions=function(hook,arg1,arg2,arg3) {
+ var acts = this.hooks[hook];
+ for (f in acts) {
+ acts[f](arg1,arg2,arg3);
+ }
+}
+
+/* --- Grammar -------------------------------------------------------------- */
+
+// API
+GrammarManager.prototype.change_grammar=function(grammar_url) {
+ var t=this;
+ t.server.switch_to_other_grammar(grammar_url, function() {
+ t.server.grammar_info(function(grammar){
+ // Set internal state
+ t.grammar = grammar;
+
+ // Call internal functions
+ t.update_startcat(grammar);
+ t.update_language_list(grammar);
+
+ // Execute hooked actions
+ t.run_actions("change_grammar",grammar);
+ });
+ });
+}
+
+/* --- Start category ------------------------------------------------------- */
+
+// Internal
+// Sets default startcat for grammar
+GrammarManager.prototype.update_startcat=function(grammar) {
+ var t=this;
+ var cats=grammar.categories;
+ var startcat0 = t.options.initial.startcat;
+ if (elem(startcat0, cats))
+ t.startcat = startcat0;
+ else
+ t.startcat = grammar.startcat;
+}
+
+// API
+GrammarManager.prototype.change_startcat=function(startcat) {
+ var t = this;
+
+ // Set internal state
+ t.startcat = startcat;
+
+ // Call internal functions
+ // ...
+
+ // Execute hooked actions
+ t.run_actions("change_startcat",startcat);
+}
+
+/* --- Languages ------------------------------------------------------------ */
+
+// Internal
+// Sets default languages for grammar
+GrammarManager.prototype.update_language_list=function(grammar) {
+ var t = this;
+ function langpart(conc,abs) { // langpart("FoodsEng","Foods") == "Eng"
+ return hasPrefix(conc,abs) ? conc.substr(abs.length) : conc;
+ }
+ // Replace the options in the menu with the languages in the grammar
+ var langs=grammar.languages;
+ for(var i=0; i
-
+
Syntax Editor
-
-
+
+
John J. Camilleri, November 2012
+
+
diff --git a/src/www/syntax-editor/editor.js b/src/www/syntax-editor/editor.js
index ca4e8628f..031a461a2 100644
--- a/src/www/syntax-editor/editor.js
+++ b/src/www/syntax-editor/editor.js
@@ -15,7 +15,7 @@ new EditorMenu
Editor.redraw_tree();
Editor.get_refinements();
*/
-function Editor(server,opts) {
+function Editor(gm,opts) {
var t = this;
/* --- Configuration ---------------------------------------------------- */
@@ -57,16 +57,34 @@ function Editor(server,opts) {
]);
/* --- Client state initialisation -------------------------------------- */
- this.server = server;
+ this.gm = gm;
+ this.server = gm.server;
this.ast = null;
- this.grammar = null;
- this.startcat = null;
- this.languages = [];
+
+ /* --- Register Grammar Manager hooks ----------------------------------- */
+ this.gm.register_action("change_grammar",function(grammar){
+ debug("Editor: change grammar");
+ var startcat0 = t.options.initial.startcat;
+ if (elem(startcat0, grammar.categories))
+ t.startcat = startcat0;
+ else
+ t.startcat = null;
+ t.get_grammar_constructors(bind(t.start_fresh,t));
+ });
+ this.gm.register_action("change_startcat",function(startcat){
+ debug("Editor: change startcat");
+ t.startcat = startcat;
+ t.start_fresh();
+ });
+ this.gm.register_action("change_languages",function(languages){
+ debug("Editor: change languages");
+ t.update_linearisation();
+ });
/* --- Main program, this gets things going ----------------------------- */
this.menu = new EditorMenu(this, this.options);
- /* --- Shutdown the editor nicely --------------------------------------- */
+ /* --- Other basic stuff ------------------------------------------------ */
this.shutdown = function() {
clear(this.container);
this.container.classList.remove("editor");
@@ -102,26 +120,17 @@ Editor.prototype.get_ast=function() {
}
Editor.prototype.get_startcat=function() {
- return this.startcat || this.grammar.startcat;
+ return this.gm.startcat;
}
-/* --- These get called from EditorMenu, or some custom code */
-
-Editor.prototype.change_grammar=function(grammar_info) {
- var t = this;
- t.grammar = grammar_info;
- var startcat0 = t.options.initial.startcat
- if (elem(startcat0, grammar_info.categories))
- t.startcat = startcat0;
- else
- t.startcat = null;
- t.get_grammar_constructors(bind(t.start_fresh,t));
-}
-
-Editor.prototype.change_startcat=function(startcat) {
- var t = this;
- t.startcat = startcat;
- t.start_fresh();
+// TODO
+Editor.prototype.initialize_from=function(opts) {
+ var t=this;
+ if (opts.startcat)
+ t.options.initial_startcat=opts.startcat;
+ t.change_grammar();
+ if (opts.abstr)
+ t.import_ast(opts.abstr);
}
// Called after changing grammar or startcat
@@ -247,7 +256,7 @@ Editor.prototype.update_linearisation=function(){
return hasPrefix(conc,abs) ? conc.substr(abs.length) : conc;
}
function row(lang, lin) {
- var langname = langpart(lang, t.grammar.name);
+ var langname = langpart(lang, t.gm.grammar.name);
var btn = button(langname, function(){
bind(t.options.lin_action,t)(lin,lang);
});
@@ -264,7 +273,7 @@ Editor.prototype.update_linearisation=function(){
var tbody=empty("tbody");
for (i in data) {
var lang = data[i].to;
- if (t.languages.length < 1 || elem(lang, t.languages)) {
+ if (t.gm.languages.length < 1 || elem(lang, t.gm.languages)) {
tbody.appendChild(row(lang, data[i].text))
}
}
diff --git a/src/www/syntax-editor/editor_menu.js b/src/www/syntax-editor/editor_menu.js
index 2caa5a658..e207133e7 100644
--- a/src/www/syntax-editor/editor_menu.js
+++ b/src/www/syntax-editor/editor_menu.js
@@ -34,39 +34,64 @@ function EditorMenu(editor,opts) {
random_button: button("Random", function(){
t.editor.generate_random();
}),
+ debug_toggle: button("⚙", function(){
+ var sel = element("debug");
+ if (sel.classList.contains("hidden"))
+ sel.classList.remove("hidden")
+ else
+ sel.classList.add("hidden")
+ }),
};
- with(this.ui) {
- if (this.options.show.grammar_menu) {
- appendChildren(this.container, [text(" Grammar: "), grammar_menu]);
- grammar_menu.onchange = bind(this.change_grammar,this);
- }
- if (this.options.show.startcat_menu) {
- appendChildren(this.container, [text(" Startcat: "), startcat_menu]);
- startcat_menu.onchange = bind(this.change_startcat,this);
- }
- if (this.options.show.to_menu) {
- appendChildren(this.container, [text(" To: "), to_toggle, to_menu]);
- to_menu.onchange = bind(this.change_language,this);
- }
- appendChildren(this.container, [clear_button]);
- if (this.options.show.random_button) {
- appendChildren(this.container, [random_button]);
+ if (t.options.show.grammar_menu) {
+ appendChildren(t.container, [text(" Grammar: "), t.ui.grammar_menu]);
+ t.ui.grammar_menu.onchange = function(){
+ var grammar_url = t.ui.grammar_menu.value;
+ t.gm.change_grammar(grammar_url);
}
}
+ if (t.options.show.startcat_menu) {
+ appendChildren(t.container, [text(" Startcat: "), t.ui.startcat_menu]);
+ t.ui.startcat_menu.onchange = function(){
+ var startcat = t.ui.startcat_menu.value;
+ t.gm.change_startcat(startcat);
+ }
+ }
+ if (t.options.show.to_menu) {
+ appendChildren(t.container, [text(" To: "), t.ui.to_toggle, t.ui.to_menu]);
+ t.ui.to_menu.onchange = function(){
+ var languages = new Array();
+ for (i in t.ui.to_menu.options) {
+ var opt = t.ui.to_menu.options[i];
+ if (opt.selected)
+ languages.push(opt.value);
+ }
+ t.gm.change_languages(languages);
+ }
+ }
+ appendChildren(t.container, [t.ui.clear_button]);
+ if (t.options.show.random_button) {
+ appendChildren(t.container, [t.ui.random_button]);
+ }
+ appendChildren(t.container, [t.ui.debug_toggle]);
/* --- Client state initialisation -------------------------------------- */
this.editor = editor;
+ this.gm = editor.gm;
this.server = editor.server;
- /* --- Main program, this gets things going ----------------------------- */
- this.server.get_grammarlists(bind(this.show_grammarlist,this));
+ /* --- Register Grammar Manager hooks ----------------------------------- */
+ this.gm.register_action("onload", bind(this.hook_onload, this));
+ this.gm.register_action("change_grammar", bind(this.hook_change_grammar, this));
+ // this.gm.register_action("change_startcat", bind(this.hook_change_startcat, this));
+ // this.gm.register_action("change_languages", bind(this.hook_change_languages, this));
+
}
/* --- Grammar menu --------------------------------------------------------- */
-// Basically called once, when initializing
-// Copied from minibar.js
-EditorMenu.prototype.show_grammarlist=function(dir,grammar_names,dir_count) {
+// show the grammar list
+EditorMenu.prototype.hook_onload=function(dir,grammar_names,dir_count) {
+ debug("EditorMenu: onload");
var t=this;
var first_time=t.ui.grammar_menu.options.length == 0;
if(first_time) {
@@ -85,7 +110,7 @@ EditorMenu.prototype.show_grammarlist=function(dir,grammar_names,dir_count) {
var grammar0=t.options.initial.grammar;
if(!grammar0) grammar0=t.grammars[0];
t.ui.grammar_menu.value=grammar0;
- t.change_grammar();
+// t.change_grammar();
}
// Wait at most 1.5s before showing the grammar menu.
if(first_time) t.timeout=setTimeout(pick_first_grammar,1500);
@@ -93,24 +118,21 @@ EditorMenu.prototype.show_grammarlist=function(dir,grammar_names,dir_count) {
}
// Copied from minibar.js
-EditorMenu.prototype.change_grammar=function() {
+EditorMenu.prototype.hook_change_grammar=function() {
+ debug("EditorMenu: change grammar");
var t=this;
var grammar_url = t.ui.grammar_menu.value;
t.server.switch_to_other_grammar(grammar_url, function() {
t.server.grammar_info(function(grammar){
t.update_startcat_menu(grammar);
t.update_language_menu(t.ui.to_menu, grammar);
-
- // Call in main Editor object
- t.editor.change_grammar(grammar);
});
});
}
/* --- Start category menu -------------------------------------------------- */
-// Called each time the current grammar is changed!
-// Copied from minibar_input.js
+// Called from hook_change_grammar
EditorMenu.prototype.update_startcat_menu=function(grammar) {
var t=this;
var menu=this.ui.startcat_menu;
@@ -129,16 +151,9 @@ EditorMenu.prototype.update_startcat_menu=function(grammar) {
// }
}
-//
-EditorMenu.prototype.change_startcat=function() {
- var new_startcat = this.ui.startcat_menu.value;
- this.editor.change_startcat(new_startcat);
-}
-
/* --- Langugage (to) menu -------------------------------------------------- */
-// Called each time the current grammar is changed!
-// Copied from minibar_support.js
+// Called from hook_change_grammar
EditorMenu.prototype.update_language_menu=function(menu,grammar) {
var t = this;
function langpart(conc,abs) { // langpart("FoodsEng","Foods") == "Eng"
@@ -162,14 +177,3 @@ EditorMenu.prototype.update_language_menu=function(menu,grammar) {
}
}
-//
-EditorMenu.prototype.change_language=function() {
- this.editor.languages = new Array();
- for (i in this.ui.to_menu.options) {
- var opt = this.ui.to_menu.options[i];
- if (opt.selected)
- this.editor.languages.push(opt.value);
- }
- this.editor.update_linearisation();
-}
-
diff --git a/src/www/syntax-editor/editor_online.js b/src/www/syntax-editor/editor_online.js
index a519d28ce..5ca81c9fa 100644
--- a/src/www/syntax-editor/editor_online.js
+++ b/src/www/syntax-editor/editor_online.js
@@ -8,8 +8,7 @@ var editor_options = {
// grammar: "http://localhost:41296/grammars/Phrasebook.pgf",
// startcat: "Proposition",
// languages: ["Eng","Swe","Ita"],
- // abstr: "PropOpenDate (SuperlPlace TheMostExpensive School) Tomorrow",
- // node_id: null
+ // abstr: "PropOpenDate (SuperlPlace TheMostExpensive School) Tomorrow"
// },
show: {
grammar_menu: true,
@@ -35,8 +34,6 @@ if(window.Minibar) // Minibar loaded?
},
// get us back to the editor!
abstract_action: function(tree) {
- //var minibar=this;
- // how to get hold of new minibar?
var editor_options = {
target: "editor",
initial: {
@@ -52,13 +49,14 @@ if(window.Minibar) // Minibar loaded?
editor.hide();
editor.minibar=new Minibar(server,minibar_options);
//editor.minibar.editor = editor; // :S
- editor.minibar.show()
+ editor.minibar.show();
}
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);
-
+// var editor = new Editor(server, editor_options);
+var gm = new GrammarManager(server);
+var editor = new Editor(gm, editor_options);