diff --git a/src/editor/simple/editor.js b/src/editor/simple/editor.js index f829c12f8..fe2c5f0b2 100644 --- a/src/editor/simple/editor.js +++ b/src/editor/simple/editor.js @@ -164,7 +164,7 @@ function add_concrete(g,el) { list.push(li([a(jsurl("add_concrete2("+g.index+",'"+c+"')"), [text(l.name)])])); } - file.appendChild(text("Pick a language for the new concrete syntax:")); + file.appendChild(p(text("Pick a language for the new concrete syntax:"))); file.appendChild(node("ul",{},list)); } @@ -276,13 +276,6 @@ function add_cat(g,el) { string_editor(el,"",add); } -function delete_ix(old,ix) { - var a=[]; -// for(var i=0;i0) { + var file=element("file"); + file.innerHTML=""; + file.appendChild(p(text("Pick a resource library module to open:"))); + file.appendChild(node("ul",{},list)); + } + } +} + +function add_open2(ix,ci,m) { + var g=local.get(ix); + var conc=g.concretes[ci]; + conc.opens || (conc.opens=[]); + conc.opens.push(m); + save_grammar(g); + open_concrete(g,ci); +} + +function delete_open(g,ci,ix) { + with(g.concretes[ci]) opens=delete_ix(opens,ix); + reload_grammar(g); +} + +function draw_opens(g,ci) { + var conc=g.concretes[ci]; + var os=conc.opens || [] ; + var es=[]; + function del(i) { return function() { delete_open(g,ci,i); }} + var first=true; + for(var i in os) { + if(!first) es.push(sep(", ")) + es.push(deletable(del(i),ident(os[i]),"Don't open this module")); + first=false; + } + es.push(more(g,add_open(ci),"Open more modules")); + return indent(es); +} function draw_param(p,dp) { function check(el) { @@ -718,6 +763,13 @@ function hidden(name,value) { /* -------------------------------------------------------------------------- */ +function delete_ix(old,ix) { + var a=[]; +// for(var i=0;i0 ? "\n\nopen "+opens.join(", ")+" in" : "" +} + function show_params(params) { return show_list("param",show_param,params); } function show_lincats(lincats) { return show_list("lincat",show_lincat,lincats); } function show_opers(opers) { return show_list("oper",show_oper,opers); }