diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 75 |
1 files changed, 40 insertions, 35 deletions
@@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines = "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 (coqtop_path ()) ^" -nois -filteropts " ^ argstr in @@ -125,7 +122,7 @@ and asks_for_coqtop args = ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in match pb_mes#run () with | `YES -> - let () = current.cmd_coqtop <- None in + let () = cmd_coqtop#set None in let () = custom_coqtop := None in let () = pb_mes#destroy () in filter_coq_opts args @@ -200,8 +197,6 @@ module GlibMainLoop = struct let read_all = Ideutils.io_read_all let async_chan_of_file fd = Glib.Io.channel_of_descr fd let async_chan_of_socket s = !gio_channel_of_descr_socket s - let add_timeout ~sec callback = - ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback) end module CoqTop = Spawn.Async(GlibMainLoop) @@ -232,7 +227,7 @@ type coqtop = { (* non quoted command-line arguments of coqtop *) mutable sup_args : string list; (* called whenever coqtop dies *) - mutable reset_handler : reset_kind -> unit task; + mutable reset_handler : unit task; (* called whenever coqtop sends a feedback message *) mutable feedback_handler : Feedback.feedback -> unit; (* actual coqtop process and its status *) @@ -295,23 +290,20 @@ let rec check_errors = function | `NVAL :: _ -> raise (TubeError "NVAL") | `OUT :: _ -> raise (TubeError "OUT") -let handle_intermediate_message handle xml = - let message = Pp.to_message xml in - let level = message.Pp.message_level in - let content = message.Pp.message_content in - let logger = match handle.waiting_for with - | Some (_, l) -> l +let handle_intermediate_message handle level content = + let logger = match handle.waiting_for with + | Some (_, l) -> l | None -> function - | Pp.Error -> Minilib.log ~level:`ERROR - | Pp.Info -> Minilib.log ~level:`INFO - | Pp.Notice -> Minilib.log ~level:`NOTICE - | Pp.Warning -> Minilib.log ~level:`WARNING - | Pp.Debug _ -> Minilib.log ~level:`DEBUG + | Feedback.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) + | Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) + | Feedback.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) + | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) + | Feedback.Debug -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) in logger level content let handle_feedback feedback_processor xml = - let feedback = Feedback.to_feedback xml in + let feedback = Xmlprotocol.to_feedback xml in feedback_processor feedback let handle_final_answer handle xml = @@ -336,19 +328,22 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let lex = Lexing.from_string s in let p = Xml_parser.make (Xml_parser.SLexbuf lex) in let rec loop () = - let xml = Xml_parser.parse p in + let xml = Xml_parser.parse ~do_not_canonicalize:true p in let l_end = Lexing.lexeme_end lex in state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; - if Pp.is_message xml then begin - handle_intermediate_message handle xml; - loop () - end else if Feedback.is_feedback xml then begin - handle_feedback feedback_processor xml; + match Xmlprotocol.is_message xml with + | Some (lvl, _loc, msg) -> + handle_intermediate_message handle lvl msg; loop () - end else begin - ignore (handle_final_answer handle xml) - end + | None -> + if Xmlprotocol.is_feedback xml then begin + handle_feedback feedback_processor xml; + loop () + end else + begin + ignore (handle_final_answer handle xml) + end in try loop () with Xml_parser.Error _ as e -> @@ -362,7 +357,9 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let print_exception = function | Xml_parser.Error e -> Xml_parser.error e - | Serialize.Marshal_error -> "Protocol violation" + | Serialize.Marshal_error(expected,actual) -> + "Protocol violation. Expected: " ^ expected ^ " Actual: " + ^ Xml_printer.to_string actual | e -> Printexc.to_string e let input_watch handle respawner feedback_processor = @@ -424,6 +421,7 @@ let mkready coqtop = fun () -> coqtop.status <- Ready; Void let rec respawn_coqtop ?(why=Unexpected) coqtop = + if why = Unexpected then warning "Coqtop died badly. Resetting."; clear_handle coqtop.handle; ignore_error (fun () -> coqtop.handle <- @@ -435,7 +433,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop = If not, there isn't much we can do ... *) assert (coqtop.handle.alive = true); coqtop.status <- New; - ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop)) + ignore (coqtop.reset_handler coqtop.handle (mkready coqtop)) let spawn_coqtop sup_args = bind_self_as (fun this -> { @@ -443,7 +441,7 @@ let spawn_coqtop sup_args = (fun () -> respawn_coqtop (this ())) (fun msg -> (this ()).feedback_handler msg); sup_args = sup_args; - reset_handler = (fun _ _ k -> k ()); + reset_handler = (fun _ k -> k ()); feedback_handler = (fun _ -> ()); status = New; }) @@ -465,10 +463,6 @@ let close_coqtop coqtop = let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop -let break_coqtop coqtop = - try !interrupter (CoqTop.unixpid coqtop.handle.proc) - with _ -> Minilib.log "Error while sending Ctrl-C" - let get_arguments coqtop = coqtop.sup_args let set_arguments coqtop args = @@ -518,6 +512,17 @@ let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) +let break_coqtop coqtop workers = + if coqtop.status = Busy then + try !interrupter (CoqTop.unixpid coqtop.handle.proc) + with _ -> Minilib.log "Error while sending Ctrl-C" + else + let rec aux = function + | [] -> Void + | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws) + in + let Void = aux workers in () + module PrintOpt = struct type t = string list |