From ec87775425dbe882bd4ce418c6028943d96d6f96 Mon Sep 17 00:00:00 2001 From: filliatr Date: Mon, 8 Dec 2003 09:19:47 +0000 Subject: pas de Goal pendant une preuve pas de Debug On/Off git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5075 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 0de38431a..d8e0a04c2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -97,6 +97,9 @@ let is_in_coq_path f = let is_in_proof_mode () = try ignore (get_pftreestate ()); true with _ -> false +let user_error_loc l s = + raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) + let interp s = prerr_endline "Starting interp..."; prerr_endline s; @@ -104,15 +107,13 @@ let interp s = Pcoq.main_entry (Pcoq.Gram.parsable (Stream.of_string s)) in match pe with - | Some (loc,(VernacDefinition _ | VernacStartTheoremProof _ | VernacBeginSection _ + | Some (loc,( VernacDefinition _ | VernacStartTheoremProof _ + | VernacBeginSection _ | VernacGoal _ | VernacDefineModule _ | VernacDeclareModuleType _)) - when is_in_proof_mode () - -> - raise (Stdpp.Exc_located (loc, - Util.UserError - ("CoqIde", - (str "cannot do that while in proof mode.")) - )) + when is_in_proof_mode () -> + user_error_loc loc (str "cannot do that while in proof mode.") + | Some (loc, VernacDebug _ ) -> + user_error_loc loc (str "cannot do that within CoqIDE") | _ -> Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); match pe with -- cgit v1.2.3