Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server

et Set Whelp Getter pour changer le nom des serveurs (report 10105 de
la 8.1 vers le trunk)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 46 insertions, 3 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 1a53adf69..8f0eb1429 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -341,10 +341,31 @@ directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
 graphical environment is also running. The browser to use can be
 selected by setting the environment variable {\tt
 COQREMOTEBROWSER}. If not explicitly set, it defaults to
-\verb!netscape -remote "OpenURL(%s)"!  or
+\verb!firefox -remote "OpenURL(%s)"!  or
 \verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
 underlying operating system (in the command, the string \verb!%s!
 serves as metavariable for the url to open).
+The Whelp tool relies on a dedicated Whelp server and on another server
+called Getter that retrieves formal documents. The default Whelp server name
+can be obtained using the command {\tt Test Whelp Server}
+\comindex{Test Whelp Server} and the default Getter can be obtained
+using the command: {\tt Test Whelp Getter} \comindex{Test Whelp
+Getter}. The Whelp server name can be changed using the command:
+
+\smallskip
+\noindent {\tt Set Whelp Server {\str}}.\\
+where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}).
+\comindex{Set Whelp Server}
+\smallskip
+
+\noindent The Getter can be changed using the command:
+\smallskip
+
+\noindent {\tt Set Whelp Getter {\str}}.\\
+where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}).  
+\comindex{Set Whelp Getter}
+
+\bigskip
 
 The {\sc Whelp} commands are:
 
diff --git a/lib/options.ml b/lib/options.ml
index 848b08611..589069567 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -125,4 +125,4 @@ let browser_cmd_fmt =
   Not_found ->
    if Sys.os_type = "Win32"
    then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
-   else "netscape -remote \"OpenURL(", ")\""
+   else "firefox -remote \"OpenURL(", ")\""
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index b41bcec8b..67ba2bd52 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -32,8 +32,30 @@ open Tacmach
 (* Coq interface to the Whelp query engine developed at 
    the University of Bologna *)
 
+let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080"
+let getter_server_name = ref "http://mowgli.cs.unibo.it:58081"
+
+open Goptions
+
+let _ =
+  declare_string_option 
+    { optsync  = false;
+      optname  = "Whelp server";
+      optkey   = (SecondaryTable ("Whelp","Server"));
+      optread  = (fun () -> !whelp_server_name);
+      optwrite = (fun s -> whelp_server_name := s) }
+
+let _ =
+  declare_string_option 
+    { optsync  = false;
+      optname  = "Whelp getter";
+      optkey   = (SecondaryTable ("Whelp","Getter"));
+      optread  = (fun () -> !getter_server_name);
+      optwrite = (fun s -> getter_server_name := s) }
+
+
 let make_whelp_request req c =
-  "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
+  !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
 
 let b = Buffer.create 16