diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 8 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 12 |
3 files changed, 15 insertions, 13 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 86057b4b..095f50c6 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: cerrors.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Pp open Util @@ -81,7 +81,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Syntax error: Undefined token.") | Lexer.Error (Bad_token s) -> hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") - | Stdpp.Exc_located (loc,exc) -> + | Compat.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn_default_aux anomaly_string report_fn exc) @@ -156,8 +156,8 @@ let rec process_vernac_interp_error = function | Proof_type.LtacLocated (s,exc) -> EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), Some (process_vernac_interp_error exc)) - | Stdpp.Exc_located (loc,exc) -> - Stdpp.Exc_located (loc,process_vernac_interp_error exc) + | Compat.Exc_located (loc,exc) -> + Compat.Exc_located (loc,process_vernac_interp_error exc) | exc -> exc diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9954ff56..551e5574 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: toplevel.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Pp open Util @@ -274,7 +274,7 @@ let set_prompt prompt = let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e - | Stdpp.Exc_located (_,e) -> is_pervasive_exn e + | Compat.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e | _ -> false @@ -290,7 +290,7 @@ let print_toplevel_error exc = in let (locstrm,exc) = match exc with - | Stdpp.Exc_located (loc, ie) -> + | Compat.Exc_located (loc, ie) -> if valid_buffer_loc top_buffer dloc loc then (print_highlight_location top_buffer loc, ie) else @@ -325,7 +325,7 @@ let parse_to_dot = let rec discard_to_dot () = try Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> + with Compat.Exc_located(_,(Token.Error _|Lexer.Error _)) -> discard_to_dot() diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a7aef93f..de732618 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: vernac.ml 15025 2012-03-09 14:27:07Z glondu $ *) (* Parsing of vernacular. *) @@ -41,14 +41,14 @@ let raise_with_file file exc = match re with | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc -> ((b, f, loc), e) - | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> + | Compat.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) - | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e) + | Compat.Exc_located (_, e) | e -> ((false,file,cmdloc), e) in raise (Error_in_file (file, inner, disable_drop inex)) let real_error = function - | Stdpp.Exc_located (_, e) -> e + | Compat.Exc_located (_, e) -> e | Error_in_file (_, _, e) -> e | e -> e @@ -206,7 +206,9 @@ let rec vernac_com interpfun (loc,com) = | VernacFail v -> if not !just_parsing then begin try - interp v; raise HasNotFailed + (* If the command actually works, ignore its effects on the state *) + States.with_state_protection + (fun v -> interp v; raise HasNotFailed) v with e -> match real_error e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") |