PGF service & minibar: put a limit on the number of parse trees

+ In the PGF web service API, the commands parse, translate and translategroup
  now accept a limit parameter. It limits the number of parse trees returned.
  If no limit is given, the behaviour is backwards compatible, i.e. no limit
  is applied.
+ In minibar, the limit is now set to 25 by default.

This change is based on a suggestion by Kaarel Kaljurand.

src/www/minibar/minibar-api.html

@@ -70,12 +70,14 @@ For an example, see <a href="minibar.html">minibar.html</a>.
   can be set to override various default options:
     <table class=border>
         <tr><th>Option<th>Default<th>Description
-        <tr><td>show_abstract<td>false<td rowspan=5>See Translations,
+        <tr><td>show_abstract<td>false<td rowspan=6>See Translations,
 	  not used directly by Minibar
 	<tr><td>show_trees<td>false
 	<tr><td>tree_img_format<td>"png"
 	<tr><td>show_grouped_translations<td>true
 	<tr><td>show_brackets<td>false
+	<tr><td>translate_limit<td>25
+
 	<tr><td>delete_button_text<td>"⌫"<td rowspan=5>See Input,
 	  not used directly by Minibar
 	<tr><td>default_source_language<td>null
@@ -212,7 +214,7 @@ HTML file, you would normally include at least the following:
 	<tr><td>show_grouped_translations<td>true<td>in case there are
 	  multiple translations, group them by concrete language
 	<tr><td>show_brackets<td>false<td>show bracketed string
-    </table>
+	<tr><td>translate_limit<td>25<td>maximum number of parse trees to retrieve    </table>
 
 </ul>
 
@@ -247,7 +249,7 @@ the user interface:
 <hr>
 <div class=modtime>
 <small class=modtime>
-HTML <!-- hhmts start -->Last modified: Mon Sep 17 17:52:22 CEST 2012 <!-- hhmts end -->
+HTML <!-- hhmts start -->Last modified: Sun Sep 30 17:33:51 CEST 2012 <!-- hhmts end -->
 </small>
 </div>
 

src/www/minibar/minibar_translations.js

@@ -14,7 +14,8 @@ function Translations(server,opts) {
 	tree_img_format: "png", // format for trees & alignment images,
 	                        // can be "gif", "png" or "svg"
 	show_grouped_translations: true,
-	show_brackets: false // show bracketed string
+	show_brackets: false, // show bracketed string
+	translate_limit: 25 // maximum number of parse trees to retrieve
     }
 
     // Apply supplied options
@@ -53,6 +54,7 @@ Translations.prototype.get_translations=function() {
     with(this) {
 	var c=current;
 	var args={from:c.from,input:gf_unlex(c.input),cat:startcat}
+	if(options.translate_limit) args.limit=options.translate_limit
 	if(options.show_grouped_translations)
 	    server.translategroup(args,bind(show_groupedtranslations,this));
 	else