Improved error messages in CoqIDE:

- add a check that coqtop can be run before starting the interface
- returns the error message in case of problem
- made illegal option message more informative
- use coqtop.byte when coqide.byte (is it a good heuristic?)
- made debugging messages silent by default in ide/undo.ml (Ctrl-C was
  calling Pervasives.prerr_endline instead of Ideutils.prerr_endline)

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

4 files changed, 36 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index c114e2c46..0b2e9b13e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -83,16 +83,21 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-let filter_coq_opts argv =
+let rec read_all_lines in_chan =
+  try
+    let arg = input_line in_chan in
+    arg::(read_all_lines in_chan)
+  with End_of_file -> []
+
+let coqtop_path () =
   let prog = Sys.executable_name in
   let dir = Filename.dirname prog in
+  if Filename.check_suffix prog ".byte" then dir^"/coqtop.byte"
+  else dir^"/coqtop.opt"
+
+let filter_coq_opts argv =
   let argstr = String.concat " " argv in
-  let oc,ic,ec = Unix.open_process_full (dir^"/coqtop.opt -filteropts "^argstr) (Unix.environment ()) in
-  let rec read_all_lines in_chan =
-    try
-      let arg = input_line in_chan in
-        arg::(read_all_lines in_chan)
-    with End_of_file -> [] in
+  let oc,ic,ec = Unix.open_process_full (coqtop_path () ^" -filteropts "^argstr) (Unix.environment ()) in
   let filtered_argv = read_all_lines oc in
   let message = read_all_lines ec in
   match Unix.close_process_full (oc,ic,ec) with
@@ -100,6 +105,22 @@ let filter_coq_opts argv =
     | Unix.WEXITED 2 -> false,filtered_argv
     | _ -> false,message
 
+exception Coqtop_output of string list
+
+let check_connection args =
+  try
+    let ic = Unix.open_process_in (coqtop_path () ^ " -batch "^args) in
+    let lines = read_all_lines ic in
+    match (Unix.close_process_in ic) with
+    | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok"
+    | _ -> raise (Coqtop_output lines)
+  with End_of_file ->
+    Pervasives.prerr_endline "Cannot start connection with coqtop";
+    | Coqtop_output lines ->
+      Pervasives.prerr_endline "Connection with coqtop failed:";
+      List.iter Pervasives.prerr_endline lines;
+      exit 1
+
 let eval_call coqtop (c:'a Ide_blob.call) =
   Safe_marshal.send coqtop.cin c;
   (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout
@@ -119,11 +140,9 @@ let toplvl_ctr = ref 0
 let toplvl_ctr_mtx = Mutex.create ()
 
 let spawn_coqtop sup_args =
-  let prog = Sys.executable_name in
-  let dir = Filename.dirname prog in
   Mutex.lock toplvl_ctr_mtx;
   try 
-    let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave "^sup_args) in
+    let oc,ic = Unix.open_process (coqtop_path ()^" -ideslave "^sup_args) in
     incr toplvl_ctr;
     Mutex.unlock toplvl_ctr_mtx;
     { cin = ic; cout = oc ; sup_args = sup_args ; version = 0 }
diff --git a/ide/coq.mli b/ide/coq.mli
index a6928eaba..6bc593477 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -15,6 +15,7 @@ open Ide_blob
 val short_version : unit -> string
 val version : unit -> string
 val filter_coq_opts : string list -> bool * string list
+val check_connection : string -> unit
 
 type coqtop
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2d22ca1fa..05f93863c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3085,8 +3085,10 @@ let process_argv argv =
     let continue,filtered = filter_coq_opts (List.tl argv) in
     if not continue then
       (List.iter Pervasives.prerr_endline filtered; exit 0);
-    if List.exists (fun arg -> String.get arg 0 == '-') filtered then
-      (output_string stderr "illegal coqide option\n"; exit 1);
+    let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
+    if opts <> [] then
+      (output_string stderr ("Illegal option: "^List.hd opts^"\n");
+       exit 1);
     filtered
   with _ ->
     (output_string stderr "coqtop choked on one of your option"; exit 1)
@@ -3095,6 +3097,7 @@ let start () =
   let argl = Array.to_list Sys.argv in
   let files = process_argv argl in
   sup_args := String.concat " " (List.filter (fun x -> not (List.mem x files)) (List.tl argl));
+  check_connection !sup_args;
   ignore_break ();
     GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
     (try
diff --git a/ide/undo.ml b/ide/undo.ml
index 917fc8816..57724297d 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ideutils
 open GText
 type action =
   | Insert of string * int * int (* content*pos*length *)