minibar: define grammar_list in config.js to restrict the grammar menu

minibar.html now reads config.js and if it defines grammar_list, only the
grammars listed there will show up in the grammar menu.

src/www/minibar/minibar.html

@@ -27,11 +27,12 @@
 &amp; <a href="http://www.grammaticalframework.org:41296/translate/">Translator</a>]
 </small>
 <small class=modtime>
-HTML <!-- hhmts start -->Last modified: Mon May 18 17:31:07 CEST 2015 <!-- hhmts end -->
+HTML <!-- hhmts start -->Last modified: Thu Jun  9 16:13:26 CEST 2016 <!-- hhmts end -->
 </small>
 
 <div id="debug" class="hidden"></div>
 
+<script type="text/javascript" src="config.js"></script> <!-- optional -->
 <script type="text/JavaScript" src="../js/grammar_manager.js"></script>
 <script type="text/JavaScript" src="../js/support.js"></script>
 <script type="text/JavaScript" src="../js/localstorage.js"></script>

src/www/minibar/minibar_online.js

@@ -7,6 +7,8 @@ var online_options={
   //grammar_list: ["Foods.pgf"], // leave undefined to get list from server
 }
 
+if(window.grammar_list) online_options.grammar_list=grammar_list
+
 var minibar_options= {
     show_abstract: true,
     show_trees: true,