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

Syntax editor: select subset of available languages

Browse Source 
Also added a basic readme file with a list of todo's
This commit is contained in:
john.j.camilleri
2012-11-16 09:33:55 +00:00
parent 225cebf121
commit 67ca0a1eae
4 changed files with 67 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
src/www/syntax-editor/js/editor.js
View File

@@ -108,14 +108,16 @@ Editor.prototype.get_refinements=function(cat) {
Editor.prototype.select_refinement=function(fun) {
with (this) {
clear(ui.refinements);
ast.removeChildren();
ast.setFun(fun);
// redraw_tree();
var args = {
id: fun,
format: "json"
};
var err = function(data){
clear(refinements);
alert("no refinements");
};
server.browse(args, bind(complete_refinement,this), err);
@@ -139,7 +141,7 @@ Editor.prototype.complete_refinement=function(data) {
}
}
// Update vis
// Update ui
redraw_tree();
update_linearisation();

25
src/www/syntax-editor/js/editor_menu.js
View File

@@ -15,11 +15,22 @@ function EditorMenu(editor,opts) {
this.container = editor.ui.menubar;
this.ui = {
startcat_menu: empty("select"),
to_menu: empty_id("select","to_menu")
to_toggle: button("...", function(){
var sel = t.ui.to_menu;
if (sel.classList.contains("hidden"))
sel.classList.remove("hidden")
else
sel.classList.add("hidden")
}),
to_menu: node("select",{
id: "to_menu",
multiple: "multiple",
class: "hidden"
} )
};
with(this.ui) {
appendChildren(this.container, [text(" Startcat: "),startcat_menu]);
appendChildren(this.container, [text(" To: "), to_menu]);
appendChildren(this.container, [text(" To: "), to_toggle, to_menu]);
startcat_menu.onchange=bind(this.change_startcat,this);
to_menu.onchange=bind(this.change_language,this);
}
@@ -119,10 +130,12 @@ EditorMenu.prototype.change_startcat=function () {
//
EditorMenu.prototype.change_language=function () {
if (this.ui.to_menu.value == "All")
this.editor.languages = new Array();
else
this.editor.languages = new Array(this.ui.to_menu.value);
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();
}