aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqOps.ml12
-rw-r--r--ide/ide_slave.ml4
-rw-r--r--ide/interface.mli6
-rw-r--r--ide/xmlprotocol.ml10
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--lib/feedback.ml10
-rw-r--r--lib/feedback.mli23
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--stm/stm.ml53
-rw-r--r--stm/stm.mli9
11 files changed, 58 insertions, 75 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 45b5a1007..15150dce9 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 8cadf1a26..2d2b54678 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 9ed606258..62f63aefb 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 d7950e5fd..bf52b0b52 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))
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 6dfa64357..88a4fa529 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -194,7 +194,7 @@ let rec unzip ctx j =
let feedback_completion_typecheck =
let open Feedback in
Option.iter (fun state_id ->
- feedback ~id:(State state_id) Feedback.Complete)
+ feedback ~id:state_id Feedback.Complete)
let infer_declaration ~trust env kn dcl =
match dcl with
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 7d9d6bf7f..df6fe3a62 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,9 +15,6 @@ type level =
| Warning
| Error
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
type route_id = int
type feedback_content =
@@ -38,9 +35,9 @@ type feedback_content =
| Message of level * Loc.t option * Pp.std_ppcmds
type feedback = {
- id : edit_or_state_id;
+ id : Stateid.t;
+ route : route_id;
contents : feedback_content;
- route : route_id;
}
let default_route = 0
@@ -56,7 +53,8 @@ let add_feeder =
let del_feeder fid = Hashtbl.remove feeders fid
-let feedback_id = ref (Edit 0)
+let default_route = 0
+let feedback_id = ref Stateid.dummy
let feedback_route = ref default_route
let set_id_for_feedback ?(route=default_route) i =
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 4bbdfcb5b..bdd236ac7 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -16,11 +16,8 @@ type level =
| Warning
| Error
-(** Coq "semantic" infos obtained during parsing/execution *)
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
+(** Coq "semantic" infos obtained during execution *)
type route_id = int
val default_route : route_id
@@ -46,17 +43,16 @@ type feedback_content =
| Message of level * Loc.t option * Pp.std_ppcmds
type feedback = {
- id : edit_or_state_id; (* The document part concerned *)
- contents : feedback_content; (* The payload *)
+ id : Stateid.t; (* The document part concerned *)
route : route_id; (* Extra routing info *)
+ contents : feedback_content; (* The payload *)
}
(** {6 Feedback sent, even asynchronously, to the user interface} *)
-(* 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.
- * Only one among state_id and edit_id can be provided. *)
+
+(* The interpreter assignes an state_id to the ast, and feedbacks happening
+ * during interpretation are attached to it.
+ *)
(** [add_feeder f] adds a feeder listiner [f], returning its id *)
val add_feeder : (feedback -> unit) -> int
@@ -67,11 +63,10 @@ val del_feeder : int -> unit
(** [feedback ?id ?route fb] produces feedback fb, with [route] and
[id] set appropiatedly, if absent, it will use the defaults set by
[set_id_for_feedback] *)
-val feedback :
- ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
(** [set_id_for_feedback route id] Set the defaults for feedback *)
-val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit
(** {6 output functions}
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 58123f63e..bcb28f77c 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -374,7 +374,7 @@ let data = ref SM.empty
let _ =
Feedback.(add_feeder (function
- | { id = State s; contents = Custom (_, "ltacprof_results", xml) } ->
+ | { id = s; contents = Custom (_, "ltacprof_results", xml) } ->
let results = to_ltacprof_results xml in
let other_results = (* Multi success can cause this *)
try SM.find s !data
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 125491988..3459156a4 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -105,7 +105,7 @@ module Make(T : Task) = struct
let report_status ?(id = !Flags.async_proofs_worker_id) s =
let open Feedback in
- feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
+ feedback ~id:Stateid.initial (WorkerStatus(id, s))
module Worker = Spawn.Sync(struct end)
diff --git a/stm/stm.ml b/stm/stm.ml
index ba5e8a11f..f8d959f97 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -24,14 +24,14 @@ open Vernac_classifier
open Feedback
let execution_error state_id loc msg =
- feedback ~id:(State state_id)
+ feedback ~id:state_id
(Message (Error, Some loc, msg))
module Hooks = struct
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
- feedback ~id:(State state_id) Processed) ()
+ feedback ~id:state_id Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
@@ -43,10 +43,6 @@ let forward_feedback, forward_feedback_hook =
try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
with e -> Mutex.unlock m; raise e) ()
-let parse_error, parse_error_hook = Hook.make
- ~default:(fun id loc msg ->
- feedback ~id (Message(Error, Some loc, msg))) ()
-
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
@@ -109,24 +105,30 @@ let indentation_of_string s =
| _ -> n, precise, len in
aux 0 0 false
-let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
- let feedback_id =
- if Option.is_empty newtip then Edit eid
- else State (Option.get newtip) in
+(* We must parse on top of a state id, it should be something like:
+
+ - get parsing information for that state.
+ - feed the parsable / parser with the right parsing information.
+ - call the parser
+
+ Now, the invariant in ensured by the callers, but this is a bit
+ problematic.
+*)
+let stm_parse ?(indlen_prev=fun() -> 0) s =
let indentation, precise, strlen = indentation_of_string s in
let indentation =
if precise then indentation else indlen_prev () + indentation in
- set_id_for_feedback ?route feedback_id;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
Flags.with_option Flags.we_are_parsing (fun () ->
try
match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
- | None -> raise (Invalid_argument "vernac_parse")
+ | None -> raise (Invalid_argument "stm_parse")
| Some (loc, ast) -> indentation, strlen, loc, ast
with e when CErrors.noncritical e ->
let (e, info) = CErrors.push e in
- let loc = Option.default Loc.ghost (Loc.get_loc info) in
- Hooks.(call parse_error feedback_id loc (iprint (e, info)));
+ (* This is the old error recovery strategy. *)
+ (* let loc = Loc.get_loc info in *)
+ (* feedback (?newtip || eid) (Message(Error, loc, msg)) *)
iraise (e, info))
()
@@ -845,7 +847,7 @@ end = struct (* {{{ *)
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
- feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
+ feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
anomaly (str"defining state "++str str_id++str" twice");
@@ -977,7 +979,7 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
(* The Stm will gain the capability to interpret commmads affecting
the whole document state, such as backtrack, etc... so we start
to design the stm command interpreter now *)
- set_id_for_feedback ?route (State id);
+ set_id_for_feedback ?route id;
Aux_file.record_in_aux_set_at loc;
(* We need to check if a command should be filtered from
* vernac_entries, as it cannot handle it. This should go away in
@@ -1391,7 +1393,7 @@ end = struct (* {{{ *)
Aux_file.record_in_aux_at loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
let p = Proof_global.return_proof ~allow_partial:drop_pt () in
- if drop_pt then feedback ~id:(State id) Complete;
+ if drop_pt then feedback ~id Complete;
p)
let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1935,11 +1937,11 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No r_where;
try
stm_vernac_interp r_for { r_what with verbose = true };
- feedback ~id:(State r_for) Processed
+ feedback ~id:r_for Processed
with e when CErrors.noncritical e ->
let e = CErrors.push e in
let msg = iprint e in
- feedback ~id:(State r_for) (Message (Error, None, msg))
+ feedback ~id:r_for (Message (Error, None, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -2141,7 +2143,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| Valid { proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
- feedback ~id:(State id) Feedback.AddedAxiom;
+ feedback ~id:id Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
Option.iter (fun expr -> stm_vernac_interp id {
verbose = true; loc = Loc.ghost; expr; indentation = 0;
@@ -2289,7 +2291,7 @@ let known_state ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
stm_vernac_interp id ~proof x;
- feedback ~id:(State id) Incomplete
+ feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
@@ -2715,13 +2717,13 @@ let ind_len_of id =
indentation + strlen
| _ -> 0
-let add ~ontop ?newtip ?(check=ignore) verb eid s =
+let add ~ontop ?newtip ?(check=ignore) verb s =
let cur_tip = VCS.cur_tip () in
if not (Stateid.equal ontop cur_tip) then
(* For now, arbitrary edits should be announced with edit_at *)
anomaly(str"Not yet implemented, the GUI should not try this");
let indentation, strlen, loc, ast =
- vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
+ stm_parse ~indlen_prev:(fun () -> ind_len_of ontop) s in
CWarnings.set_current_loc loc;
check(loc,ast);
let clas = classify_vernac ast in
@@ -2742,8 +2744,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
Future.purify (fun s ->
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
- let newtip, route = report_with in
- let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
+ let indentation, strlen, loc, ast = stm_parse s in
CWarnings.set_current_loc loc;
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
@@ -2932,8 +2933,8 @@ let get_all_proof_names () =
(* Export hooks *)
let state_computed_hook = Hooks.state_computed_hook
let state_ready_hook = Hooks.state_ready_hook
-let parse_error_hook = Hooks.parse_error_hook
let forward_feedback_hook = Hooks.forward_feedback_hook
let unreachable_state_hook = Hooks.unreachable_state_hook
let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+
(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index a89062c29..d3e5dde39 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -13,8 +13,8 @@ open Loc
(** state-transaction-machine interface *)
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]
- having edit id [eid]. [check] is called on the AST.
+(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop].
+ [check] is called on the AST.
The [ontop] parameter is just for asserting the GUI is on sync, but
will eventually call edit_at on the fly if needed.
The sentence [s] is parsed in the state [ontop].
@@ -23,7 +23,7 @@ open Loc
val add :
ontop:Stateid.t -> ?newtip:Stateid.t ->
?check:(vernac_expr located -> unit) ->
- bool -> edit_id -> string ->
+ bool -> string ->
Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
(* parses and executes a command at a given state, throws away its side effects
@@ -182,9 +182,8 @@ val register_proof_block_delimiter :
* the name of the Task(s) above) *)
val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
-val parse_error_hook :
- (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
+
(* ready means that master has it at hand *)
val state_ready_hook : (Stateid.t -> unit) Hook.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 14:24:06 +0000