":
[]
+ pgf = case files of
+ (abstract,_):_ -> "%20"++take (length abstract-3) abstract++".pgf"
+ _ -> ""
+
listing = concatMap listfile files
listfile (name,source) =
@@ -246,6 +252,13 @@ resultpage dir cmd (ecode,stdout,stderr) files =
num n s = pad (show n)++" "++escape s
pad s = replicate (5-length s) ' '++s
+ rel = unlines . map relative . lines
+
+ -- remove absolute file paths from error messages:
+ relative s = case stripPrefix cwd s of
+ Just ('/':rest) -> rest
+ _ -> s
+
escape = concatMap escape1
escape1 '<' = "<"
escape1 '&' = "&"
diff --git a/src/www/minibar/about.html b/src/www/minibar/about.html
index 08f891bbc..ddf897073 100644
--- a/src/www/minibar/about.html
+++ b/src/www/minibar/about.html
@@ -170,11 +170,13 @@ Some implementation details:
[Added 2011-10-18] Added a button to display some grammar info and a
start category menu. The start category menu can be turned off by passing
the option {startcat_menu:false} when starting the minibar.
+
[Added 2012-02-10] New minibar option initial_grammar to
+ control which of the available grammars is selected initially.
- Last modified: Tue Oct 18 17:18:42 CEST 2011
+ Last modified: Fri Feb 10 15:55:30 CET 2012
TH
diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js
index a94cc5629..e37b33a7c 100644
--- a/src/www/minibar/minibar.js
+++ b/src/www/minibar/minibar.js
@@ -32,7 +32,8 @@ function Minibar(server,opts) {
target: "minibar",
try_google: true,
feedback_url: null,
- help_url: null
+ help_url: null,
+ initial_grammar: null
}
// Apply supplied options
@@ -81,7 +82,9 @@ Minibar.prototype.show_grammarlist=function(grammars) {
}
if(options.help_url)
menubar.appendChild(button("Help",bind(open_help,this)));
- select_grammar(grammars[0]);
+ var grammar0=options.initial_grammar || grammars[0];
+ grammar_menu.value=grammar0;
+ select_grammar(grammar0);
}
}
diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js
index 1c15e87bf..e6693f7a0 100644
--- a/src/www/minibar/minibar_online.js
+++ b/src/www/minibar/minibar_online.js
@@ -7,13 +7,6 @@ var online_options={
//grammar_list: ["Foods.pgf"], // leave undefined to get list from server
}
-
-if(/^\?\/tmp\//.test(location.search)) {
- online_options.grammars_url=location.search.substr(1);
-}
-
-var server=pgf_online(online_options);
-
var minibar_options= {
show_abstract: true,
show_trees: true,
@@ -22,4 +15,12 @@ var minibar_options= {
//feedback_url: "feedback.html",
try_google: true
}
+
+if(/^\?\/tmp\//.test(location.search)) {
+ var args=decodeURIComponent(location.search.substr(1)).split(" ")
+ if(args[0]) online_options.grammars_url=args[0];
+ if(args[1]) minibar_options.initial_grammar=args[1];
+}
+
+var server=pgf_online(online_options);
var minibar=new Minibar(server,minibar_options);