Coqide: display initial connection errors in popups instead of on stderr

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

5 files changed, 95 insertions, 64 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index d46a98738..e0da0c3dc 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -55,60 +55,104 @@ let rec read_all_lines in_chan =
     arg::(read_all_lines in_chan)
   with End_of_file -> []
 
+let fatal_error_popup msg =
+  let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok
+    ~message_type:`ERROR ~message:msg ()
+  in ignore (popup#run ()); exit 1
+
+let final_info_popup small msg =
+  if small then
+    let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok
+      ~message_type:`INFO ~message:msg ()
+    in
+    let _ = popup#run () in
+    exit 0
+  else
+    let popup = GWindow.dialog () in
+    let button = GButton.button ~label:"ok" ~packing:popup#action_area#add ()
+    in
+    let scroll = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
+      ~packing:popup#vbox#add ~height:500 ()
+    in
+    let _ = GMisc.label ~text:msg ~packing:scroll#add_with_viewport () in
+    let _ = popup#connect#destroy ~callback:(fun _ -> exit 0) in
+    let _ = button#connect#clicked ~callback:(fun _ -> exit 0) in
+    let _ = popup#run () in
+    exit 0
+
+let connection_error cmd lines exn =
+  fatal_error_popup
+    ("Connection with coqtop failed!\n"^
+     "Command was: "^cmd^"\n"^
+     "Answer was: "^(String.concat "\n  " lines)^
+     "Exception was: "^Printexc.to_string exn)
+
+let display_coqtop_answer cmd lines =
+  final_info_popup (List.length lines < 30)
+    ("Coqtop exited\n"^
+     "Command was: "^cmd^"\n"^
+     "Answer was: "^(String.concat "\n  " lines))
+
+let check_remaining_opt arg =
+  if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
+
 let rec filter_coq_opts args =
-  let coqprog = coqtop_path () in
-  let asks_for_coqtop () =
-    let pb_mes = GWindow.message_dialog ~message:"Fail to load coqtop. Reset the preference to default ?"
-      ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
-    match pb_mes#run () with
-      | `YES ->
- 	let () = current.cmd_coqtop  <- None in
-	    let () = custom_coqtop := None in
-	let () = pb_mes#destroy () in
-	filter_coq_opts args
-      | `DELETE_EVENT | `NO ->
-	let () = pb_mes#destroy () in
-	let cmd_sel = GWindow.file_selection ~title:"Coqtop to execute (edit your preference then)"
-	  ~filename:coqprog ~urgency_hint:true () in
-	match cmd_sel#run () with
-	  | `OK ->
-	    let () = custom_coqtop := (Some cmd_sel#filename) in
-	    let () = cmd_sel#destroy () in
-	    filter_coq_opts args
-	  | `HELP -> exit 0
-	  | `CANCEL | `DELETE_EVENT -> exit 0
-  in
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote coqprog ^" -nois -filteropts " ^ argstr in
+  let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
+  let filtered_args = ref [] in
+  let errlines = ref [] in
   try
     let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
-    let filtered_args = read_all_lines oc in
-    let pbs_blabla = read_all_lines ec in
+    filtered_args := read_all_lines oc;
+    errlines := read_all_lines ec;
     match Unix.close_process_full (oc,ic,ec) with
-      | Unix.WEXITED 0 -> true,filtered_args
-      | Unix.WEXITED 127 -> asks_for_coqtop ()
-      | _ -> false,filtered_args@pbs_blabla
-  with Sys_error _ -> asks_for_coqtop ()
-
-exception Coqtop_output of string list
+      | Unix.WEXITED 0 ->
+	List.iter check_remaining_opt !filtered_args; !filtered_args
+      | Unix.WEXITED 127 -> asks_for_coqtop args
+      | _ -> display_coqtop_answer cmd (!filtered_args @ !errlines)
+  with Sys_error _ -> asks_for_coqtop args
+    | e -> connection_error cmd (!filtered_args @ !errlines) e
+
+and asks_for_coqtop args =
+  let pb_mes = GWindow.message_dialog
+    ~message:"Failed to load coqtop. Reset the preference to default ?"
+    ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
+  match pb_mes#run () with
+    | `YES ->
+      let () = current.cmd_coqtop  <- None in
+      let () = custom_coqtop := None in
+      let () = pb_mes#destroy () in
+      filter_coq_opts args
+    | `DELETE_EVENT | `NO ->
+      let () = pb_mes#destroy () in
+      let cmd_sel = GWindow.file_selection
+	~title:"Coqtop to execute (edit your preference then)"
+	~filename:(coqtop_path ()) ~urgency_hint:true () in
+      match cmd_sel#run () with
+	| `OK ->
+	  let () = custom_coqtop := (Some cmd_sel#filename) in
+	  let () = cmd_sel#destroy () in
+	  filter_coq_opts args
+	| `CANCEL | `DELETE_EVENT | `HELP -> exit 0
+
+exception WrongExitStatus of string
+
+let print_status = function
+  | Unix.WEXITED n -> "WEXITED "^string_of_int n
+  | Unix.WSIGNALED n -> "WSIGNALED "^string_of_int n
+  | Unix.WSTOPPED n -> "WSTOPPED "^string_of_int n
 
 let check_connection args =
+  let lines = ref [] in
+  let argstr = String.concat " " (List.map Filename.quote args) in
+  let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
   try
-    let argstr = String.concat " " (List.map Filename.quote args) in
-    let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
     let ic = Unix.open_process_in cmd in
-    let lines = read_all_lines ic in
+    lines := read_all_lines ic;
     match Unix.close_process_in ic with
-    | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok"
-    | _ -> raise (Coqtop_output lines)
-  with
-    | End_of_file ->
-      Minilib.safe_prerr_endline "Cannot start connection with coqtop";
-      exit 1
-    | Coqtop_output lines ->
-      Minilib.safe_prerr_endline "Connection with coqtop failed:";
-      List.iter Minilib.safe_prerr_endline lines;
-      exit 1
+    | Unix.WEXITED 0 -> () (* coqtop seems ok *)
+    | st -> raise (WrongExitStatus (print_status st))
+  with e -> connection_error cmd !lines e
 
 (** Useful stuff *)
 
diff --git a/ide/coq.mli b/ide/coq.mli
index a0f5c30f8..4bce3af9a 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -14,12 +14,14 @@ val short_version : unit -> string
 val version : unit -> string
 
 (** * Launch a test coqtop processes, ask for a correct coqtop if it fails.
-    @return if coqide should go further & the list of arguments that coqtop
-    did not understand. (the files probably ..) *)
-val filter_coq_opts : string list -> bool * string list
+    @return the list of arguments that coqtop did not understand
+    (the files probably ..). This command may terminate coqide in
+    case of trouble.  *)
+val filter_coq_opts : string list -> string list
 
 (** Launch a coqtop with the user args in order to be sure that it works,
-    checking in particular that initial.coq is found *)
+    checking in particular that initial.coq is found. This command
+    may terminate coqide in case of trouble *)
 val check_connection : string list -> unit
 
 (** * The structure describing a coqtop sub-process *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index de4474c16..c49cea11e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2381,15 +2381,3 @@ let read_coqide_args argv =
     Ideutils.custom_coqtop := coqtop;
     custom_project_files := project_files;
   argv
-
-let process_argv argv =
-  try
-    let continue,filtered = Coq.filter_coq_opts (List.tl argv) in
-    if not continue then
-      (List.iter Minilib.safe_prerr_endline filtered; exit 0);
-    let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
-    if opts <> [] then
-      (Minilib.safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1);
-    filtered
-  with _ ->
-    (Minilib.safe_prerr_endline "coqtop choked on one of your option"; exit 1)
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 38b0fab0d..57158a6a5 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -16,9 +16,6 @@ val sup_args : string list ref
     Minilib.coqtop_path accordingly *)
 val read_coqide_args : string list -> string list
 
-(** Ask coqtop the remaining options it doesn't recognize *)
-val process_argv : string list -> string list
-
 (** Prepare the widgets, load the given files in tabs *)
 val main : string list -> unit
 
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 1e71b8da4..4c546ab7f 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -85,7 +85,7 @@ let () =
 		  else failwith ("Coqide internal error: " ^ msg)));
   let argl = Array.to_list Sys.argv in
   let argl = Coqide.read_coqide_args argl in
-  let files = Coqide.process_argv argl in
+  let files = Coq.filter_coq_opts (List.tl argl) in
   let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
   Coq.check_connection args;
   Coqide.sup_args := args;