From 568b0b82e229535ce1355dcc4f959ac8f4f13921 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 26 May 2005 11:54:30 +0000
Subject: New environment variable COQREMOTEBROWSER to set the command used by
 Coq and coqide to control a remote browser. It uses the standard syntax where
 "%s" is the placeholder for the URL.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7077 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES        |  6 ++++++
 lib/options.ml | 21 +++++++++++++++++----
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/CHANGES b/CHANGES
index 52adfe4aaf..c47a6e7a78 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes from V8.0
 =================
 
+Environment variables
+
+- COQREMOTEBROWSER to set the command invoked to start the remote browser
+  both in Coq and coqide. Standard syntax: "%s" is the placeholder for the
+  URL (doc TODO)
+
 Vernacular commands
 
 - Added "Print Ltac qualid" to print a user defined tactic (doc TODO)
diff --git a/lib/options.ml b/lib/options.ml
index 45f27107e3..17e8af1820 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -120,7 +120,20 @@ let boxed_definitions _ = !boxed_definitions
 (* Options for external tools *)
 
 let browser_cmd_fmt =
-  if Sys.os_type = "Win32"
-  then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
-  else "netscape -remote \"OpenURL(", ")\""
-  
+ try
+  let coq_netscape_remote_var = "COQREMOTEBROWSER" in
+  let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in
+  let i = Util.string_index_from coq_netscape_remote 0 "%s" in
+  let pre = String.sub coq_netscape_remote 0 i in
+  let post = String.sub coq_netscape_remote (i + 2)
+              (String.length coq_netscape_remote - (i + 2)) in
+   if Util.string_string_contains ~where:post ~what:"%s" then
+    error ("The environment variable \"" ^
+           coq_netscape_remote_var ^
+           "\" must contain exactly one placeholder \"%s\".")
+   else pre,post
+ with
+  Not_found ->
+   if Sys.os_type = "Win32"
+   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
+   else "netscape -remote \"OpenURL(", ")\""
-- 
cgit v1.2.3