diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | ide/coq.ml | 33 | ||||
| -rw-r--r-- | ide/coq.mli | 10 | ||||
| -rw-r--r-- | ide/coqOps.ml | 133 | ||||
| -rw-r--r-- | ide/coqOps.mli | 1 | ||||
| -rw-r--r-- | ide/session.ml | 4 | ||||
| -rw-r--r-- | ide/wg_Command.ml | 5 | ||||
| -rw-r--r-- | lib/interface.mli | 28 | ||||
| -rw-r--r-- | lib/pp.ml | 12 | ||||
| -rw-r--r-- | lib/pp.mli | 16 | ||||
| -rw-r--r-- | lib/serialize.ml | 36 | ||||
| -rw-r--r-- | lib/serialize.mli | 4 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 10 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 9 |
14 files changed, 231 insertions, 72 deletions
diff --git a/Makefile.build b/Makefile.build index b42432d48d..80ff59f716 100644 --- a/Makefile.build +++ b/Makefile.build @@ -541,7 +541,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) lib/serialize$(BESTOBJ) tools/fake_ide$(BESTOBJ) +$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) tools/fake_ide$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,unix) diff --git a/ide/coq.ml b/ide/coq.ml index 1219811104..baff54d627 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) diff --git a/ide/coq.mli b/ide/coq.mli index 0210d0b41b..84ef466d72 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -63,6 +63,9 @@ val spawn_coqtop : string list -> coqtop val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit (** Register a handler called when a coqtop dies (badly or on purpose) *) +val set_feedback_handler : coqtop -> (Interface.feedback -> unit) -> unit +(** Register a handler called when coqtop sends a feedback message *) + val init_coqtop : coqtop -> unit task -> unit (** Finish initializing a freshly spawned coqtop, by running a first task on it. The task should run its inner continuation at the end. *) @@ -113,8 +116,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit type 'a query = 'a Interface.value task (** A type abbreviation for coqtop specific answers *) -val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool -> - string -> string query +val interp : + ?logger:Ideutils.logger -> + ?raw:bool -> + ?verbose:bool -> + int -> string -> string query val rewind : int -> int query val status : Interface.status query val goals : Interface.goals option query diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 3e76b94b20..2647f923c0 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -11,11 +11,40 @@ open Ideutils type flag = [ `COMMENT | `UNSAFE ] -type ide_info = { - start : GText.mark; - stop : GText.mark; - flags : flag list; -} +module SentenceId : sig + + type sentence = private { + start : GText.mark; + stop : GText.mark; + mutable flags : flag list; + id : int; + } + + val mk_sentence : + start:GText.mark -> stop:GText.mark -> flag list -> sentence + val set_flags : sentence -> flag list -> unit + +end = struct + + type sentence = { + start : GText.mark; + stop : GText.mark; + mutable flags : flag list; + id : int; + } + + let id = ref 0 + let mk_sentence ~start ~stop flags = decr id; { + start = start; + stop = stop; + flags = flags; + id = !id; + } + + let set_flags s f = s.flags <- f + +end +open SentenceId let prefs = Preferences.current @@ -39,6 +68,7 @@ class coqops (_script:Wg_ScriptView.script_view) (_pv:Wg_ProofView.proof_view) (_mv:Wg_MessageView.message_view) + (_ct:Coq.coqtop) get_filename = object(self) val script = _script @@ -48,6 +78,9 @@ object(self) val cmd_stack = Stack.create () + initializer + Coq.set_feedback_handler _ct self#process_feedback + method private get_start_of_input = buffer#get_iter_at_mark (`NAME "start_of_input") @@ -81,7 +114,8 @@ object(self) flash_info "This error is so nasty that I can't even display it." else messages#add s; in - let query = Coq.interp ~logger:messages#push ~raw:true ~verbose:false phrase in + let query = + Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in let next = function | Interface.Fail (_, err) -> display_error err; Coq.return () | Interface.Good msg | Interface.Unsafe msg -> @@ -103,12 +137,12 @@ object(self) let is_comment = stop#backward_char#has_tag Tags.Script.comment_sentence in - let payload = { - start = `MARK (buffer#create_mark start); - stop = `MARK (buffer#create_mark stop); - flags = if is_comment then [`COMMENT] else []; - } in - Queue.push payload queue; + let sentence = + mk_sentence + ~start:(`MARK (buffer#create_mark start)) + ~stop:(`MARK (buffer#create_mark stop)) + (if is_comment then [`COMMENT] else []) in + Queue.push sentence queue; if not stop#is_end then loop (succ len) stop in try loop 0 self#get_start_of_input with Exit -> () @@ -123,22 +157,37 @@ object(self) buffer#delete_mark sentence.stop; done - method private commit_queue_transaction queue sentence newflags = + method private mark_as_needed sentence = + let start = buffer#get_iter_at_mark sentence.start in + let stop = buffer#get_iter_at_mark sentence.stop in + let tag = + if List.mem `UNSAFE sentence.flags then Tags.Script.unjustified + else Tags.Script.processed in + buffer#apply_tag tag ~start ~stop + + method private process_feedback msg = + let id = msg.Interface.edit_id in + if id = 0 || Stack.is_empty cmd_stack then () else + let sentence = + let last_sentence = Stack.top cmd_stack in + if last_sentence.id = id then Some last_sentence else None in + match msg.Interface.content, sentence with + | Interface.AddedAxiom, Some sentence -> + set_flags sentence (CList.add_set `UNSAFE sentence.flags); + self#mark_as_needed sentence + | Interface.Processed, Some sentence -> self#mark_as_needed sentence + | _, None -> Minilib.log "Coqide/Coq is really asynchronous now!" + (* In this case we shoud look for (exec_)id into cmd_stack *) + + method private commit_queue_transaction sentence = (* A queued command has been successfully done, we push it to [cmd_stack]. We reget the iters here because Gtk is unable to warranty that they were not modified meanwhile. Not really necessary but who knows... *) + self#mark_as_needed sentence; let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in - let sentence = { sentence with flags = newflags @ sentence.flags } in - let tag = - if List.mem `UNSAFE newflags then Tags.Script.unjustified - else Tags.Script.processed - in buffer#move_mark ~where:stop (`NAME "start_of_input"); - buffer#apply_tag tag ~start ~stop; - buffer#remove_tag Tags.Script.to_process ~start ~stop; - ignore (Queue.pop queue); - Stack.push sentence cmd_stack + buffer#remove_tag Tags.Script.to_process ~start ~stop method private process_error queue phrase loc msg = Coq.bind (Coq.return ()) (function () -> @@ -153,6 +202,10 @@ object(self) buffer#apply_tag Tags.Script.error ~start ~stop; buffer#place_cursor ~where:start in + let sentence = Stack.pop cmd_stack in + let start = buffer#get_iter_at_mark sentence.start in + let stop = buffer#get_iter_at_mark sentence.stop in + buffer#remove_tag Tags.Script.to_process ~start ~stop; self#discard_command_queue queue; pop_info (); position_error loc; @@ -183,9 +236,10 @@ object(self) let () = script#recenter_insert in self#show_goals else - let sentence = Queue.peek queue in + let sentence = Queue.pop queue in + Stack.push sentence cmd_stack; if List.mem `COMMENT sentence.flags then - (self#commit_queue_transaction queue sentence []; loop ()) + (self#commit_queue_transaction sentence; loop ()) else (* If the line is not a comment, we interpret it. *) let phrase = @@ -193,17 +247,18 @@ object(self) let stop = buffer#get_iter_at_mark sentence.stop in start#get_slice ~stop in - let commit_and_continue msg flags = + let commit_and_continue msg = push_msg Interface.Notice msg; - self#commit_queue_transaction queue sentence flags; + self#commit_queue_transaction sentence; loop () in - let query = Coq.interp ~logger:push_msg ~verbose phrase in + let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in let next = function - | Interface.Good msg -> commit_and_continue msg [] - | Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE] - | Interface.Fail (loc, msg) -> - self#process_error queue phrase loc msg + | Interface.Good msg -> commit_and_continue msg + | Interface.Unsafe msg -> + set_flags sentence (CList.add_set `UNSAFE sentence.flags); + commit_and_continue msg + | Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg in Coq.bind query next in @@ -329,12 +384,12 @@ object(self) buffer#apply_tag tag ~start ~stop; if self#get_insert#compare stop <= 0 then buffer#place_cursor ~where:stop; - let ide_payload = { - start = `MARK (buffer#create_mark start); - stop = `MARK (buffer#create_mark stop); - flags = []; - } in - Stack.push ide_payload cmd_stack; + let sentence = + mk_sentence + ~start:(`MARK (buffer#create_mark start)) + ~stop:(`MARK (buffer#create_mark stop)) + [] in + Stack.push sentence cmd_stack; messages#clear; self#show_goals in @@ -345,7 +400,7 @@ object(self) in let try_phrase phrase stop more = let action = log "Sending to coq now" in - let query = Coq.interp ~verbose:false phrase in + let query = Coq.interp ~verbose:false 0 phrase in let next = function | Interface.Fail (l, str) -> display_error (l, str); @@ -400,7 +455,7 @@ object(self) | Interface.Good true | Interface.Unsafe true -> Coq.return () | Interface.Good false | Interface.Unsafe false -> let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in - let cmd = Coq.interp cmd in + let cmd = Coq.interp 0 cmd in let next = function | Interface.Fail (l, str) -> messages#set ("Couln't add loadpath:\n"^str); diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 7e47ca23f7..48a07f48ba 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -25,5 +25,6 @@ class coqops : Wg_ScriptView.script_view -> Wg_ProofView.proof_view -> Wg_MessageView.message_view -> + coqtop -> (unit -> string option) -> ops diff --git a/ide/session.ml b/ide/session.ml index 8eeb3c6f9e..4e95fefca3 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -155,8 +155,8 @@ let create file coqtop_args = let finder = new Wg_Find.finder (script :> GText.view) in let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in let _ = fops#update_stats in - let cops = new CoqOps.coqops script proof messages (fun () -> fops#filename) - in + let cops = + new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in let _ = Coq.init_coqtop coqtop cops#initialize in { diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index e0a7427798..dd8896cba0 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -111,10 +111,9 @@ object(self) if String.get com (String.length com - 1) = '.' then com ^ " " else com ^ " " ^ entry#text ^" . " in - let log level message = result#buffer#insert (message^"\n") - in + let log level message = result#buffer#insert (message^"\n") in let process = - Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function + Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function | Interface.Fail (l,str) -> result#buffer#insert ("Error while interpreting "^phrase^":\n"^str); Coq.return () diff --git a/lib/interface.mli b/lib/interface.mli index 349f7baf98..d54fb84760 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -103,7 +103,7 @@ type coq_info = { compile_date : string; } -(** Coq messages *) +(** Coq unstructured messages *) type message_level = | Debug of string @@ -117,6 +117,20 @@ type message = { message_content : string; } +(** Coq "semantic" infos obtained during parsing/execution *) +type edit_id = int + +type feedback_content = + | AddedAxiom + | Processed + +type feedback = { + edit_id : edit_id; + content : feedback_content; +} + +(** Calls result *) + type location = (int * int) option (* start and end of the error *) type 'a value = @@ -126,18 +140,16 @@ type 'a value = (* Request/Reply message protocol between Coq and CoqIde *) -(** Running a command (given as a string). - The 1st flag indicates whether to use "raw" mode - (less sanity checks, no impact on the undo stack). - Suitable e.g. for queries, or for the Set/Unset +(** Running a command (given as its id and its text). + "raw" mode (less sanity checks, no impact on the undo stack) + is suitable for queries, or for the Set/Unset of display options that coqide performs all the time. - The 2nd flag controls the verbosity. The returned string contains the messages produced - by this command, but not the updated goals (they are + but not the updated goals (they are to be fetch by a separated [current_goals]). *) -type interp_sty = raw * verbose * string (* spiwack: [Inl] for safe and [Inr] for unsafe. *) type interp_rty = (string,string) Util.union +type interp_sty = edit_id * raw * verbose * string (** Backtracking by at least a certain number of phrases. No finished proofs will be re-opened. Instead, @@ -354,6 +354,18 @@ let msg_debug x = !logger (Debug "_") x let set_logger l = logger := l +(** Feedback *) + +let feeder = ref ignore +let feedback_id = ref 0 +let set_id_for_feedback i = feedback_id := i +let feedback what = + !feeder { + Interface.edit_id = !feedback_id; + Interface.content = what + } +let set_feeder f = feeder := f + (** Utility *) let string_of_ppcmds c = diff --git a/lib/pp.mli b/lib/pp.mli index b46115fd4a..bc7441836b 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -106,6 +106,22 @@ val std_logger : logger val set_logger : logger -> unit +(** {6 Feedback sent, even asynchronously, to the user interface *) + +(* This stuff should be available to most of the system, line msg_* above. + * But I'm unsure this is the right place, especially for the global edit_id. + * + * Morally the parser gets a string and an edit_id, and gives back an AST. + * Feedbacks during the parsing phase are attached to this edit_id. + * The interpreter assignes an exec_id to the ast, and feedbacks happening + * during interpretation are attached to the exec_id (still unimplemented, + * since the two phases are performed sequentially) *) + +val feedback : Interface.feedback_content -> unit + +val set_id_for_feedback : Interface.edit_id -> unit +val set_feeder : (Interface.feedback -> unit) -> unit + (** {6 Utilities} *) val string_of_ppcmds : std_ppcmds -> string diff --git a/lib/serialize.ml b/lib/serialize.ml index 0b9cc0a14f..fd8c7e7e4e 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -359,9 +359,10 @@ let to_value f = function | _ -> raise Marshal_error let of_call = function -| Interp (raw, vrb, cmd) -> +| Interp (id,raw, vrb, cmd) -> let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in - Element ("call", ("val", "interp") :: flags, [PCData cmd]) + Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags, + [PCData cmd]) | Rewind n -> Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) | Goal () -> @@ -394,9 +395,10 @@ let to_call = function let ans = massoc "val" attrs in begin match ans with | "interp" -> + let id = List.assoc "id" attrs in let raw = List.mem_assoc "raw" attrs in let vrb = List.mem_assoc "verbose" attrs in - Interp (raw, vrb, raw_string l) + Interp (int_of_string id, raw, vrb, raw_string l) | "rewind" -> let steps = int_of_string (massoc "steps" attrs) in Rewind steps @@ -525,6 +527,30 @@ let is_message = function | Element ("message", _, _) -> true | _ -> false +let to_feedback_content xml = do_match xml "feedback_content" + (fun s args -> match s with + | "addedaxiom" -> AddedAxiom + | "processed" -> Processed + | _ -> raise Marshal_error) + +let of_feedback_content = function +| AddedAxiom -> constructor "feedback_content" "addedaxiom" [] +| Processed -> constructor "feedback_content" "processed" [] + +let of_feedback msg = + let content = of_feedback_content msg.content in + Element ("feedback", ["id",string_of_int msg.edit_id], [content]) + +let to_feedback xml = match xml with +| Element ("feedback", ["id",id], [content]) -> + { edit_id = int_of_string id; + content = to_feedback_content content } +| _ -> raise Marshal_error + +let is_feedback = function +| Element ("feedback", _, _) -> true +| _ -> false + (** Conversions between ['a value] and xml answers When decoding an xml answer, we dynamically check that it is compatible @@ -617,10 +643,10 @@ let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x let pr_call = function - | Interp (r,b,s) -> + | Interp (id,r,b,s) -> let raw = if r then "RAW" else "" in let verb = if b then "" else "SILENT" in - "INTERP"^raw^verb^" ["^s^"]" + "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]" | Rewind i -> "REWIND "^(string_of_int i) | Goal _ -> "GOALS" | Evars _ -> "EVARS" diff --git a/lib/serialize.mli b/lib/serialize.mli index 3ecf066bef..4af4d09749 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -48,6 +48,10 @@ val of_message : message -> xml val to_message : xml -> message val is_message : xml -> bool +val of_feedback : feedback -> xml +val to_feedback : xml -> feedback +val is_feedback : xml -> bool + val of_answer : 'a call -> 'a value -> xml val to_answer : xml -> 'a call -> 'a value diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index d3b927a590..6a4823ee0f 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -31,6 +31,8 @@ let eval_call call coqtop = let content = message.Interface.message_content in let () = logger level content in loop () + else if Serialize.is_feedback xml then + loop () else (Serialize.to_answer xml call) in let res = loop () in @@ -38,10 +40,10 @@ let eval_call call coqtop = match res with Interface.Fail _ -> exit 1 | _ -> () let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (true,false,s))); - "INTERPRAW", (fun s -> eval_call (Serialize.interp (true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Serialize.interp (false,false,s))); - "INTERP", (fun s -> eval_call (Serialize.interp (false,true,s))); + [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (0,true,false,s))); + "INTERPRAW", (fun s -> eval_call (Serialize.interp (0,true,true,s))); + "INTERPSILENT", (fun s -> eval_call (Serialize.interp (0,false,false,s))); + "INTERP", (fun s -> eval_call (Serialize.interp (0,false,true,s))); "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s))); "GOALS", (fun _ -> eval_call (Serialize.goals ())); "HINTS", (fun _ -> eval_call (Serialize.hints ())); diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index bd3067d969..fd5fa85cba 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -114,7 +114,8 @@ let coqide_cmd_checks (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) -let interp (raw,verbosely,s) = +let interp (id,raw,verbosely,s) = + Pp.set_id_for_feedback id; let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Vernac.parse_sentence (pa,None) in if not raw then coqide_cmd_checks loc_ast; @@ -338,6 +339,11 @@ let slave_logger level message = Xml_utils.print_xml !orig_stdout xml; flush !orig_stdout +let slave_feeder msg = + let xml = Serialize.of_feedback msg in + Xml_utils.print_xml !orig_stdout xml; + flush !orig_stdout + (** The main loop *) (** Exceptions during eval_call should be converted into [Interface.Fail] @@ -348,6 +354,7 @@ let loop () = init_signal_handler (); catch_break := false; Pp.set_logger slave_logger; + Pp.set_feeder slave_feeder; (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; |