From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Dec 2016 18:14:58 +0100 Subject: [stm] Break stm/toplevel dependency loop. Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. --- proofs/proof_global.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a2ee622215..120cde5e55 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -317,7 +317,10 @@ let constrain_variables init uctx = let cstrs = UState.constrain_variables levels uctx in Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) -let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context + +let close_proof ~keep_body_ucst_separate ?feedback_id ~now + (fpl : closed_proof_output Future.computation) = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in @@ -395,8 +398,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = universes = (universes, binders) }, fun pr_ending -> CEphemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context - let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin -- cgit v1.2.3 From 6d520f47e907010f556ef4ba24715607390460ef Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 24 Feb 2017 20:13:57 +0100 Subject: Remove a dead exception catching code. The code was assuming that Proofview.tclFOCUS could raise a CList.IndexOutOfRange exception but this isn't the case. The focusing functions already catch this exception and raises an algebraic exception within the tactic mechanism. --- proofs/pfedit.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'proofs') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 80bea0c3b1..b06ea43bdd 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -143,12 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) with - | Proof_global.NoCurrentProof -> CErrors.error "No focused proof" - | CList.IndexOutOfRange -> - match gi with - | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - CErrors.user_err msg - | _ -> assert false + Proof_global.NoCurrentProof -> CErrors.error "No focused proof" let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) -- cgit v1.2.3 From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- proofs/proof_global.ml | 4 ++-- proofs/proof_using.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 120cde5e55..ca7330fdb6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -195,9 +195,9 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - CErrors.error (Pp.string_of_ppcmds + CErrors.user_err (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).")) + str"Use \"Abort All\" first or complete proof(s).") end let discard_gen id = diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a125fb10db..f51586c739 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = prerr_endline (string_of_ppcmds x) in + let print x = Feedback.msg_error x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" -- cgit v1.2.3