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 c69f69ee9c
commit c6c9b994d2
2 changed files with 25 additions and 3 deletions

View File

@@ -25,7 +25,7 @@
&amp; <a href="http://www.grammaticalframework.org:41296/translate/">Translator</a>]
</small>
<small class=modtime>
HTML <!-- hhmts start --> Last modified: Mon Feb 13 18:07:42 CET 2012 <!-- hhmts end -->
HTML <!-- hhmts start --> Last modified: Fri Apr 27 15:53:46 CEST 2012 <!-- hhmts end -->
</small>
<address>
@@ -36,6 +36,7 @@ HTML <!-- hhmts start --> Last modified: Mon Feb 13 18:07:42 CET 2012 <!-- hhmts
<script type="text/JavaScript" src="minibar_support.js"></script>
<script type="text/JavaScript" src="pgf_online.js"></script>
<script type="text/javascript" src="minibar_online.js"></script>
<script type="text/javascript" src="../gfse/gf_abs.js"></script>
</body>
</html>

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;
}