diff options
| author | Maxime Dénès | 2016-11-18 08:38:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-18 08:38:30 +0100 |
| commit | bdcf5b040b975a179fe9b2889fea0d38ae4689df (patch) | |
| tree | 1f35be33dcc6ca7117bb85db4415d6f728b80641 /intf | |
| parent | 954f1697fb750eecf4612bbb191a91c3a4bafb7c (diff) | |
Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.
It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f77a940a7e..92e4dd618e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,6 +283,16 @@ 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 *) @@ -441,6 +451,9 @@ 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 @@ -495,7 +508,7 @@ type vernac_type = | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with - | VtBack of Stateid.t * vernac_part_of_script + | VtStm of vernac_control * 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 *) @@ -503,6 +516,14 @@ 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].*) |