aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/texmacspp.ml3
-rw-r--r--intf/vernacexpr.mli23
-rw-r--r--parsing/g_vernac.ml410
-rw-r--r--printing/ppvernac.ml16
-rw-r--r--stm/stm.ml51
-rw-r--r--stm/vernac_classifier.ml22
-rw-r--r--toplevel/vernac.ml3
-rw-r--r--toplevel/vernacentries.ml4
8 files changed, 20 insertions, 112 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 680da7f54..dbcd8630b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,9 +724,6 @@ let rec tmpp v loc =
| VernacComments (cl) ->
xmlComment loc (List.flatten (List.map pp_comment cl))
- (* Stm backdoor *)
- | VernacStm _ as x -> xmlTODO loc x
-
(* Proof management *)
| VernacGoal _ as x -> xmlTODO loc x
| VernacAbort _ as x -> xmlTODO loc x
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 92e4dd618..f77a940a7 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -283,16 +283,6 @@ type bullet =
| Star of int
| Plus of int
-(** {6 Types concerning Stm} *)
-type 'a stm_vernac =
- | JoinDocument
- | Finish
- | Wait
- | PrintDag
- | Observe of Stateid.t
- | Command of 'a (* An out of flow command not to be recorded by Stm *)
- | PGLast of 'a (* To ease the life of PG *)
-
(** {6 Types concerning the module layer} *)
(** Rigid / flexible module signature *)
@@ -451,9 +441,6 @@ type vernac_expr =
| VernacRegister of lident * register_kind
| VernacComments of comment list
- (* Stm backdoor *)
- | VernacStm of vernac_expr stm_vernac
-
(* Proof management *)
| VernacGoal of constr_expr
| VernacAbort of lident option
@@ -508,7 +495,7 @@ type vernac_type =
| VtProofStep of proof_step
| VtProofMode of string
| VtQuery of vernac_part_of_script * report_with
- | VtStm of vernac_control * vernac_part_of_script
+ | VtBack of Stateid.t * vernac_part_of_script
| VtUnknown
and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
@@ -516,14 +503,6 @@ and vernac_start = string * opacity_guarantee * Id.t list
and vernac_sideff_type = Id.t list
and vernac_is_alias = bool
and vernac_part_of_script = bool
-and vernac_control =
- | VtFinish
- | VtWait
- | VtJoinDocument
- | VtPrintDag
- | VtObserve of Stateid.t
- | VtBack of Stateid.t
- | VtPG
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9b52d1bf3..4ba9eeefa 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -64,16 +64,6 @@ GEXTEND Gram
| IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
| IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
- (* Stm backdoor *)
- | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
- | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
- | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait
- | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag
- | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
- VernacStm (Observe (Stateid.of_int (int_of_string id)))
- | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
- | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
-
| v = vernac_poly -> v ]
]
;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3494ad006..a6b1c97f5 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -538,22 +538,6 @@ module Make
| VernacLocal (local, v) ->
return (pr_locality local ++ spc() ++ pr_vernac_body v)
- (* Stm *)
- | VernacStm JoinDocument ->
- return (keyword "Stm JoinDocument")
- | VernacStm PrintDag ->
- return (keyword "Stm PrintDag")
- | VernacStm Finish ->
- return (keyword "Stm Finish")
- | VernacStm Wait ->
- return (keyword "Stm Wait")
- | VernacStm (Observe id) ->
- return (keyword "Stm Observe " ++ str(Stateid.to_string id))
- | VernacStm (Command v) ->
- return (keyword "Stm Command " ++ pr_vernac_body v)
- | VernacStm (PGLast v) ->
- return (keyword "Stm PGLast " ++ pr_vernac_body v)
-
(* Proof management *)
| VernacAbortAll ->
return (keyword "Abort All")
diff --git a/stm/stm.ml b/stm/stm.ml
index e387e6322..0ddaf604a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -989,7 +989,7 @@ end = struct (* {{{ *)
try
match v with
| VernacResetInitial ->
- VtStm (VtBack Stateid.initial, true), VtNow
+ VtBack (Stateid.initial, true), VtNow
| VernacResetName (_,name) ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
@@ -997,20 +997,20 @@ end = struct (* {{{ *)
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- VtStm (VtBack oid, true), VtNow
+ VtBack (oid, true), VtNow
with Not_found ->
- VtStm (VtBack id, true), VtNow)
+ VtBack (id, true), VtNow)
| VernacBack n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
- VtStm (VtBack oid, true), VtNow
+ VtBack (oid, true), VtNow
| VernacUndo n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,tactic,undo) ->
let value = (if tactic then 1 else 0) - undo in
if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
- VtStm (VtBack oid, true), VtLater
+ VtBack (oid, true), VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1027,16 +1027,16 @@ end = struct (* {{{ *)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
- VtStm (VtBack oid, true), VtLater
+ VtBack (oid, true), VtLater
| VernacAbortAll ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
- VtStm (VtBack oid, true), VtLater
+ VtBack (oid, true), VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
+ VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow
| _ -> VtUnknown, VtNow
with
| Not_found ->
@@ -2428,22 +2428,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
prerr_endline (fun () ->
" classified as: " ^ string_of_vernac_classification c);
match c with
- (* PG stuff *)
- | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
- | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
- (* Joining various parts of the document *)
- | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
- | VtStm (VtFinish, b), VtNow -> finish (); `Ok
- | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok
- | VtStm (VtPrintDag, b), VtNow ->
- VCS.print ~now:true (); `Ok
- | VtStm (VtObserve id, b), VtNow -> observe id; `Ok
- | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
- |VtPrintDag |VtWait),_), VtLater ->
- anomaly(str"classifier: join actions cannot be classified as VtLater")
-
(* Back *)
- | VtStm (VtBack oid, true), w ->
+ | VtBack(oid, true), w ->
let id = VCS.new_node ~id:newtip () in
let { mine; others } = Backtrack.branches_of oid in
let valid = VCS.get_branch_pos head in
@@ -2462,12 +2448,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.checkout_shallowest_proof_branch ();
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
- | VtStm (VtBack id, false), VtNow ->
+ | VtBack (id, false), VtNow ->
prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
Backtrack.backto id;
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
- | VtStm (VtBack id, false), VtLater ->
+ | VtBack (id, false), VtLater ->
anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
(* Query *)
@@ -2604,15 +2590,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
| VtUnknown, VtLater ->
anomaly(str"classifier: VtUnknown must imply VtNow")
end in
- (* Proof General *)
- begin match expr with
- | VernacStm (PGLast _) ->
- if not (VCS.Branch.equal head VCS.Branch.master) then
- vernac_interp Stateid.dummy
- { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
- expr = VernacShow (ShowGoal OpenSubgoals) }
- | _ -> ()
- end;
prerr_endline (fun () -> "processed }}}");
VCS.print ();
rc
@@ -2674,8 +2651,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
- | VtStm (w,_), _ ->
- ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
+ | VtBack (w,_), _ ->
+ ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow))
| _ ->
ignore(process_transaction
~tty:false aast (VtQuery (false,report_with), VtNow)))
@@ -2822,7 +2799,7 @@ let interp verb (loc,e) =
let print_goals =
verb && match clas with
| VtQuery _, _ -> false
- | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
+ | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true
| _ -> not !Flags.coqtop_ui in
try finish ~print_goals ()
with e ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index dc5be08a3..f9bf9653f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -33,10 +33,7 @@ let string_of_vernac_type = function
| VtQuery (b,(id,route)) ->
"Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
" route " ^ string_of_int route
- | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
- "Stm " ^ string_of_in_script b
- | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
- | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+ | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b
let string_of_vernac_when = function
| VtLater -> "Later"
@@ -55,7 +52,7 @@ let declare_vernac_classifier
let elide_part_of_script_and_now (a, _) =
match a with
| VtQuery (_,id) -> VtQuery (false,id), VtNow
- | VtStm (x, _) -> VtStm (x, false), VtNow
+ | VtBack (x, _) -> VtBack (x, false), VtNow
| x -> x, VtNow
let make_polymorphic (a, b as x) =
@@ -69,23 +66,12 @@ let set_undo_classifier f = undo_classifier := f
let rec classify_vernac e =
let static_classifier e = match e with
- (* PG compatibility *)
- | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
- | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
- when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
| VernacSetOption (["Universe"; "Polymorphism"],_)
| VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
- (* Stm *)
- | VernacStm Finish -> VtStm (VtFinish, true), VtNow
- | VernacStm Wait -> VtStm (VtWait, true), VtNow
- | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
- | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
- | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
- | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
- | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
+
(* Nested vernac exprs *)
| VernacProgram e -> classify_vernac e
| VernacLocal (_,e) -> classify_vernac e
@@ -98,7 +84,7 @@ let rec classify_vernac e =
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
- | VtStm _ | VtProofMode _ ), _ as x -> x
+ | VtBack _ | VtProofMode _ ), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtNow
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bfdae85d5..ba5bc5506 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,8 +27,7 @@ let rec is_navigation_vernac = function
| VernacResetName _
| VernacBacktrack _
| VernacBackTo _
- | VernacBack _
- | VernacStm _ -> true
+ | VernacBack _ -> true
| VernacRedirect (_, (_,c))
| VernacTime (_,c) ->
is_navigation_vernac c (* Time Back* is harmless *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 230e62607..f0e63aa7c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1941,7 +1941,6 @@ let interp ?proof ~loc locality poly c =
| VernacTime _ -> assert false
| VernacRedirect _ -> assert false
| VernacTimeout _ -> assert false
- | VernacStm _ -> assert false
| VernacError e -> raise e
@@ -2209,9 +2208,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
aux ?locality ~polymorphism:b isprogcmd c
| VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
| VernacLocal _ -> CErrors.error "Locality specified twice"
- | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
- | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
- | VernacStm _ -> assert false (* Done by Stm *)
| VernacFail v ->
with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
| VernacTimeout (n,v) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 16:16:43 +0000