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.

2 files changed, 25 insertions, 3 deletions

diff --git a/src/www/minibar/minibar.html b/src/www/minibar/minibar.html
index 9f9735ad0..06938a4b8 100644
--- a/src/www/minibar/minibar.html
+++ b/src/www/minibar/minibar.html
@@ -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>
diff --git a/src/www/minibar/minibar_input.js b/src/www/minibar/minibar_input.js
index af3d5054e..dd32b6f05 100644
--- a/src/www/minibar/minibar_input.js
+++ b/src/www/minibar/minibar_input.js
@@ -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;
+}