From 3a7d9fcafedc4987d0748a8717b2b012a779de39 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 14:14:34 +0100 Subject: [stm] Remove edit_id. We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. --- ide/coqOps.ml | 12 +++--------- ide/ide_slave.ml | 4 ++-- ide/interface.mli | 6 ++++-- ide/xmlprotocol.ml | 10 ++-------- 4 files changed, 11 insertions(+), 21 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 45b5a1007a..15150dce99 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -415,11 +415,7 @@ object(self) buffer#apply_tag Tags.Script.tooltip ~start ~stop; add_tooltip sentence pre post markup - method private is_dummy_id id = - match id with - | Edit 0 -> true - | State id when Stateid.equal id Stateid.dummy -> true - | _ -> false + method private is_dummy_id id = Stateid.equal id Stateid.dummy method private enqueue_feedback msg = (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) @@ -434,8 +430,7 @@ object(self) let sentence = let finder _ state_id s = match state_id, id with - | Some id', State id when Stateid.equal id id' -> Some (state_id, s) - | _, Edit id when id = s.edit_id -> Some (state_id, s) + | Some id', id when Stateid.equal id id' -> Some (state_id, s) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in @@ -505,8 +500,7 @@ object(self) else try match id, Doc.tip document with - | Edit _, _ -> () - | State id1, id2 when Stateid.newer_than id2 id1 -> () + | id1, id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks end; diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8cadf1a263..2d2b54678f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -95,7 +95,7 @@ let ide_cmd_checks (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in + let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -379,7 +379,7 @@ let init = let initial_id, _ = if not (is_in_load_paths (physical_path_of_string dir)) then Stm.add false ~ontop:(Stm.get_current_state ()) - 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) + (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; diff --git a/ide/interface.mli b/ide/interface.mli index 9ed6062588..62f63aefb9 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -111,8 +111,10 @@ type coq_info = { (** Calls result *) type location = (int * int) option (* start and end of the error *) -type state_id = Feedback.state_id -type edit_id = Feedback.edit_id +type state_id = Stateid.t + +(* Obsolete *) +type edit_id = int (* The fail case carries the current state_id of the prover, the GUI should probably retract to that point *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d7950e5fd5..bf52b0b52b 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -907,9 +907,7 @@ let of_feedback_content = function of_string filename ] | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] -let of_edit_or_state_id = function - | Edit id -> ["object","edit"], of_edit_id id - | State id -> ["object","state"], of_stateid id +let of_edit_or_state_id id = ["object","state"], of_stateid id let of_feedback msg = let content = of_feedback_content msg.contents in @@ -921,12 +919,8 @@ let of_feedback msg_fmt = msg_format := msg_fmt; of_feedback let to_feedback xml = match xml with - | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { - id = Edit(to_edit_id id); - route = int_of_string route; - contents = to_feedback_content content } | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = State(to_stateid id); + id = to_stateid id; route = int_of_string route; contents = to_feedback_content content } | x -> raise (Marshal_error("feedback",x)) -- cgit v1.2.3 From 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 16 Feb 2017 22:31:13 +0100 Subject: [stm] Move main parsing entry point to the STM. Mainly due to notations, proof modes and plugins, parsing in Coq is stateful, so we expose a state-aware parsing API in the STM. This is a first move to unify all the parsing entry points in the Stm and the toplevel, and allows STM clients to control their input stream properly. This greatly helps for instance, with whole-document parsing. This commit supersedes PR#204. --- ide/ide_slave.ml | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 2d2b54678f..8897577640 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -86,16 +86,19 @@ let ide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning (strbrk "Set this option from the IDE menu instead"); + Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning (strbrk "Use IDE navigation instead"); + Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then - Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") + Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks s in + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Stm.parse_sentence sid pa in + ide_cmd_checks loc_ast; + let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -122,7 +125,9 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = Stm.query ~at:id s; "" +let query (s,id) = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Stm.query ~at:id pa; "" let annotate phrase = let (loc, ast) = @@ -370,17 +375,19 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized") else begin + let init_sid = Stm.get_current_state () in initialized := true; match file with - | None -> Stm.get_current_state () + | None -> init_sid | Some file -> let dir = Filename.dirname file in let open Loadpath in let open CUnix in let initial_id, _ = - if not (is_in_load_paths (physical_path_of_string dir)) then - Stm.add false ~ontop:(Stm.get_current_state ()) - (Printf.sprintf "Add LoadPath \"%s\". " dir) - else Stm.get_current_state (), `NewTip in + if not (is_in_load_paths (physical_path_of_string dir)) then begin + let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in + let loc_ast = Stm.parse_sentence init_sid pa in + Stm.add false ~ontop:init_sid loc_ast + end else init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; Stm.finish (); -- cgit v1.2.3 From ce2b2058587224ade9261cd4127ef4f6e94d356b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 27 Feb 2017 20:16:40 +0100 Subject: [stm] Port the toplevel to the STM. - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. --- ide/ide_slave.ml | 45 +++++---------------------------------------- 1 file changed, 5 insertions(+), 40 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8897577640..bc7ce38836 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -8,6 +8,7 @@ (************************************************************************) open Vernacexpr +open Vernacprop open CErrors open Util open Pp @@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with | VernacUnsetOption o -> coqide_known_option o | _ -> false -let is_debug cmd = match cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true - | _ -> false - -let is_query cmd = match cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - -let is_undo cmd = match cmd with - | VernacUndo _ | VernacUndoTo _ -> true - | _ -> false - (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks (loc,ast) = @@ -87,7 +69,7 @@ let ide_cmd_checks (loc,ast) = user_error "Debug mode not available in the IDE"; if is_known_option ast then Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); - if Vernac.is_navigation_vernac ast || is_undo ast then + if is_navigation_vernac ast || is_undo ast then Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") @@ -132,7 +114,7 @@ let query (s,id) = let annotate phrase = let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Vernac.parse_sentence (pa,None) + Stm.parse_sentence (Stm.get_current_state ()) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -394,26 +376,9 @@ let init = initial_id end -(* Retrocompatibility stuff *) +(* Retrocompatibility stuff, disabled since 8.7 *) let interp ((_raw, verbose), s) = - let vernac_parse s = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () in - Stm.interp verbose (vernac_parse s); - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - Stm.get_current_state (), CSig.Inl "" + Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer -- cgit v1.2.3 From 46856a80958f1aaa3242b6d37f018df9528e5e5f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 02:08:29 +0100 Subject: [vernac] vernacentries.mli cleanup This header file had accumulated quite a bit of cruft over the years, we clean it up while we are at it. No functional change as all the removed variables/methods were noops long time ago. --- ide/ide_slave.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bc7ce38836..65eececf7f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -466,9 +466,6 @@ let loop () = let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); - (* We'll handle goal fetching and display in our own way *) - Vernacentries.enable_goal_printing := false; - Vernacentries.qed_display_script := false; while not !quit do try let xml_query = Xml_parser.parse xml_ic in -- cgit v1.2.3