diff options
author | 2010-10-14 17:58:31 +0200 | |
---|---|---|
committer | 2010-10-14 17:58:31 +0200 | |
commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /toplevel/vernac.ml | |
parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'toplevel/vernac.ml')
-rw-r--r-- | toplevel/vernac.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7f8bcb9e..a00efc5c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *) (* Parsing of vernacular. *) @@ -44,7 +44,7 @@ let raise_with_file file exc = ((b, f, loc), e) | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) - | _ -> ((false,file,cmdloc), re) + | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e) in raise (Error_in_file (file, inner, disable_drop inex)) @@ -198,7 +198,10 @@ let rec vernac_com interpfun (loc,com) = with e -> stop(); raise e end - | v -> if not !just_parsing then interpfun v + | v -> + if not !just_parsing then + States.with_heavy_rollback interpfun + Cerrors.process_vernac_interp_error v in try @@ -239,7 +242,7 @@ and read_vernac_file verbosely s = * backtracking. *) let raw_do_vernac po = - vernac (States.with_heavy_rollback Vernacentries.interp) (po,None); + vernac Vernacentries.interp (po,None); Lib.add_frozen_state(); Lib.mark_end_of_command() |