minibar: word-for-word replacements: use concrete syntax for replacement words when possible

Instead of showing the name of a function in the abstract syntax, linearize it
and show the result. For functions with argument, e.g. That : Kind -> Item,
the function is applied to the right number of placeholder arguments: 'That ?'.
If the linearization fails, the name of the function is shown anyway.
This commit is contained in:
hallgren
2012-04-27 14:00:01 +00:00
parent 5241469c8e
commit 82e1ee4a95
2 changed files with 25 additions and 3 deletions

View File

@@ -393,8 +393,17 @@ Input.prototype.show_replacements=function(brackets,parent,tree) {
function replace() {
t.replace_word(brackets,parent,rfun,tree);
}
if(rfun_type==fun_type)
t.words.insertBefore(button(rfun,replace),extb);
function show_replacement(lin) {
//console.log(lin)
t.words.insertBefore(button(lin[0].text || rfun,replace),extb);
}
if(rfun_type==fun_type) {
var tmpl=fun_template(rfun,rfun_type)
if(tmpl)
t.server.linearize({to:t.current.from,cat:cat,tree:tmpl},show_replacement)
else
t.words.insertBefore(button(rfun,replace),extb)
}
}
t.browse(rfun,browse3)
}
@@ -533,3 +542,15 @@ function modify_tree(tree,fid,fun) {
}
return tree;
}
function fun_template(fname,ftype) {
if(window.parse_fun) {
var fun=parse_fun(fname+" : "+ftype).ok
if(fun) {
var t=fname;
for(var i=1;i<fun.type.length;i++) t+=" ?"
return t;
}
}
return null;
}