From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- toplevel/vernac.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'toplevel/vernac.ml') 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() -- cgit v1.2.3