summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:43:43 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:45:11 +0200
commit6e34b272d789455a9be589e27ad3a998cf25496b (patch)
tree57b74c7cbafd705a1ebce7d16cdaec02b704fb44 /toplevel
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent2bdcd093b357adb2185518dabbafd1a0b9279044 (diff)
Remove non-DFSG contentsupstream/8.3.pl4+dfsg
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml8
-rw-r--r--toplevel/toplevel.ml8
-rw-r--r--toplevel/vernac.ml12
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 !")