diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 01:35:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 01:35:06 +0200 |
| commit | ce7c528298b045b7363d530a8db034aeb622cd42 (patch) | |
| tree | 97a858abf220c511d1303130323bf5fbfd6d47c8 /stm/vernac_classifier.ml | |
| parent | 8b15eee6125f7f8596f17e9c982fb944a5e3f9be (diff) | |
[stm] More cleanup of "classification is not an interpreter"
We remove meta-information from the query classification and we don't
process `Stm.query` as a transaction anymore, as the right API is
available to it to execute the command directly.
This simplifies pure commands and removes some impossible cases.
Depends on #7138.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index a78323323..eff870715 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -16,8 +16,6 @@ open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] -let string_of_in_script b = if b then " (inside script)" else "" - let string_of_parallel = function | `Yes (solve,abs) -> "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" @@ -34,7 +32,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route + | VtQuery -> "Query" | VtMeta -> "Meta " let string_of_vernac_when = function @@ -70,7 +68,7 @@ let classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater + | VernacCheckMayEval _ -> VtQuery, VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -205,7 +203,7 @@ let classify_vernac e = static_control_classifier ~poly e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier ~poly e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ + | ( VtQuery | VtProofStep _ | VtSideff _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, @@ -214,6 +212,6 @@ let classify_vernac e = in static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e -let classify_as_query = VtQuery (true,Feedback.default_route), VtLater +let classify_as_query = VtQuery, VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater |