diff options
| author | hallgren <hallgren@chalmers.se> | 2012-04-27 14:00:01 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2012-04-27 14:00:01 +0000 |
| commit | c6c9b994d21af42a2dc7b8145967bf8c24bc2f7d (patch) | |
| tree | a2503604622305c6cae12be4b385ff1bc7141f87 /src/www/minibar/minibar.html | |
| parent | c69f69ee9c176322e9d385e5d103e8f05247b6b2 (diff) | |
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.
Diffstat (limited to 'src/www/minibar/minibar.html')
| -rw-r--r-- | src/www/minibar/minibar.html | 3 |
1 files changed, 2 insertions, 1 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 @@ & <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> |