diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 33 |
1 files changed, 26 insertions, 7 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 121981110..baff54d62 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -275,6 +275,8 @@ type coqtop = { sup_args : string list; (* called whenever coqtop dies *) mutable reset_handler : reset_kind -> unit task; + (* called whenever coqtop sends a feedback message *) + mutable feedback_handler : Interface.feedback -> unit; (* actual coqtop process and its status *) mutable handle : handle; mutable status : status; @@ -360,6 +362,11 @@ let handle_intermediate_message logger xml = let content = message.Interface.message_content in logger level content +let handle_feedback feedback_processor xml = + let () = Minilib.log "Handling some feedback" in + let feedback = Serialize.to_feedback xml in + feedback_processor feedback + let handle_final_answer handle ccb xml = let () = Minilib.log "Handling coqtop answer" in let () = handle.waiting_for <- None in @@ -370,7 +377,7 @@ type input_state = { mutable lexerror : int option; } -let unsafe_handle_input handle state conds = +let unsafe_handle_input handle feedback_processor state conds = let chan = Glib.Io.channel_of_descr handle.cout in let () = check_errors conds in let s = io_read_all chan in @@ -392,6 +399,12 @@ let unsafe_handle_input handle state conds = let () = state.lexerror <- None in let () = handle_intermediate_message logger xml in loop () + else if Serialize.is_feedback xml then + let remaining = String.sub s l_end (String.length s - l_end) in + let () = state.fragment <- remaining in + let () = state.lexerror <- None in + let () = handle_feedback feedback_processor xml in + loop () else (* We should have finished decoding s *) let () = if not (is_blank s l_end) then raise AnswerWithoutRequest in @@ -413,7 +426,7 @@ let unsafe_handle_input handle state conds = let () = state.lexerror <- Some l_end in () -let install_input_watch handle respawner = +let install_input_watch handle respawner feedback_processor = let io_chan = Glib.Io.channel_of_descr handle.cout in let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *) let state = { @@ -429,7 +442,7 @@ let install_input_watch handle respawner = if not handle.alive then false (* coqtop already terminated *) else try - let () = unsafe_handle_input handle state conds in + let () = unsafe_handle_input handle feedback_processor state conds in true with e -> let () = Minilib.log ("Coqtop reader failed, resetting: "^print_exception e) in @@ -472,7 +485,9 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop = If not, there isn't much we can do ... *) assert (coqtop.handle.alive = true); coqtop.status <- New; - install_input_watch coqtop.handle (fun () -> respawn_coqtop coqtop); + install_input_watch coqtop.handle + (fun () -> respawn_coqtop coqtop) + (fun msg -> coqtop.feedback_handler msg); ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop)) let spawn_coqtop sup_args = @@ -481,14 +496,18 @@ let spawn_coqtop sup_args = handle = spawn_handle sup_args; sup_args = sup_args; reset_handler = (fun _ _ k -> k ()); + feedback_handler = (fun _ -> ()); status = New; } in - install_input_watch ct.handle (fun () -> respawn_coqtop ct); + install_input_watch ct.handle + (fun () -> respawn_coqtop ct) (fun msg -> ct.feedback_handler msg); ct let set_reset_handler coqtop hook = coqtop.reset_handler <- hook +let set_feedback_handler coqtop hook = coqtop.feedback_handler <- hook + let is_computing coqtop = (coqtop.status = Busy) (* For closing a coqtop, we don't try to send it a Quit call anymore, @@ -540,8 +559,8 @@ let eval_call ?(logger=default_logger) call handle k = Minilib.log "End eval_call"; Void -let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s h k = - eval_call ~logger (Serialize.interp (raw,verbose,s)) h +let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s h k = + eval_call ~logger (Serialize.interp (i,raw,verbose,s)) h (function | Interface.Good (Util.Inl v) -> k (Interface.Good v) | Interface.Good (Util.Inr v) -> k (Interface.Unsafe v) |