From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- ide/coq.ml | 120 ++++++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 95 insertions(+), 25 deletions(-) (limited to 'ide/coq.ml') 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; -- cgit v1.2.3