summaryrefslogtreecommitdiff
path: root/ide/coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml120
1 files changed, 95 insertions, 25 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 16a07b01..76dc5650 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -54,36 +54,106 @@ let rec read_all_lines in_chan =
arg::(read_all_lines in_chan)
with End_of_file -> []
-let filter_coq_opts args =
+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)^"\n"^
+ "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 argstr = String.concat " " (List.map Filename.quote args) in
- let cmd = Filename.quote !Minilib.coqtop_path ^" -nois -filteropts " ^ argstr in
- let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
- let filtered_args = read_all_lines oc in
- let message = read_all_lines ec in
- match Unix.close_process_full (oc,ic,ec) with
- | Unix.WEXITED 0 -> true,filtered_args
- | Unix.WEXITED 2 -> false,filtered_args
- | _ -> false,message
-
-exception Coqtop_output of string list
+ let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
+ let cmd = requote cmd in
+ let filtered_args = ref [] in
+ let errlines = ref [] in
+ try
+ let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
+ filtered_args := read_all_lines oc;
+ errlines := read_all_lines ec;
+ match Unix.close_process_full (oc,ic,ec) with
+ | 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 () = !Preferences.current.Preferences.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
+ let cmd = requote cmd in
try
- let argstr = String.concat " " (List.map Filename.quote args) in
- let cmd = Filename.quote !Minilib.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
(** * The structure describing a coqtop sub-process *)
@@ -139,7 +209,7 @@ let open_process_pid prog args =
let spawn_coqtop sup_args =
Mutex.lock toplvl_ctr_mtx;
try
- let prog = !Minilib.coqtop_path in
+ let prog = coqtop_path () in
let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
let (pid,ic,oc) = open_process_pid prog args in
incr toplvl_ctr;