diff options
| author | hallgren <hallgren@chalmers.se> | 2012-03-26 17:17:54 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2012-03-26 17:17:54 +0000 |
| commit | a8ddb8fe5cc671a82102101690f0a624eae057fe (patch) | |
| tree | 5bddf1f969085f929a638f8647ad005dd83efa0a /src/www/minibar/pgf_online.js | |
| parent | 9a6887aa496dcdb579e46915fd6d3c737e3dbb99 (diff) | |
minibar: support for adding grammars from several servers to the grammar menu
You can also add grammars from several directories on the same server of course.
The included minibar configuration file adds the user's own grammars from the
grammar editor.
Diffstat (limited to 'src/www/minibar/pgf_online.js')
| -rw-r--r-- | src/www/minibar/pgf_online.js | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/www/minibar/pgf_online.js b/src/www/minibar/pgf_online.js index b6329daba..970aae062 100644 --- a/src/www/minibar/pgf_online.js +++ b/src/www/minibar/pgf_online.js @@ -27,12 +27,13 @@ function pgf_online(options) { else http_get_json(this.grammars_url+"grammars.cgi",cont,err); }, get_grammarlists: function(cont,err) { // May call cont several times! + var ds=this.other_grammars_urls; + var n=1+ds.length; function pair(dir) { - return function(grammar_list){cont(dir,grammar_list)} + return function(grammar_list){cont(dir,grammar_list,n)} } function ignore_error(err) { console.log(err) } this.get_grammarlist(pair(this.grammars_url),err) - var ds=this.other_grammars_urls; for(var i in ds) http_get_json(ds[i]+"grammars.cgi",pair(ds[i]),ignore_error); }, |