From 75f569f35fbbbbab5a4629eaf3385335a3024e0b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 03:16:09 +0100 Subject: [vernac] Move `Quit` and `Drop` to the toplevel layer. This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules. --- stm/stm.ml | 6 ------ stm/vernac_classifier.ml | 1 - 2 files changed, 7 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index ad94b6807..756b93c61 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2734,7 +2734,6 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - if e = CErrors.Drop then Exninfo.iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; @@ -2881,11 +2880,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) rc (* Side effect on all branches *) - | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop -> - let st = Vernacstate.freeze_interp_state `No in - ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); - `Ok - | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f68c8b326..9a8af3a58 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,7 +185,6 @@ let classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) - | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) -- cgit v1.2.3