diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 12 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 4 | ||||
| -rw-r--r-- | ide/interface.mli | 6 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 10 |
4 files changed, 11 insertions, 21 deletions
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)) |