diff options
| author | hallgren <hallgren@chalmers.se> | 2016-06-09 14:20:24 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2016-06-09 14:20:24 +0000 |
| commit | 18f17ba857dbcdff789410e98f95dd30c6786021 (patch) | |
| tree | 1aff61e6cbe2bd0ef04360cf48741f8f5e9695a8 | |
| parent | 096b4cfceea03007ae1ac7d46080c2a5f8e99688 (diff) | |
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.
| -rw-r--r-- | src/www/minibar/minibar.html | 3 | ||||
| -rw-r--r-- | src/www/minibar/minibar_online.js | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/www/minibar/minibar.html b/src/www/minibar/minibar.html index 3eea85c22..b1382339e 100644 --- a/src/www/minibar/minibar.html +++ b/src/www/minibar/minibar.html @@ -27,11 +27,12 @@ & <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> diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js index 0f35f4514..8ff10f7fb 100644 --- a/src/www/minibar/minibar_online.js +++ b/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, |