diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 8a9ef501..a1acd1d6 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 11317 2008-08-07 15:52:38Z barras $ *) +(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *) open Pp open Util open Flags open Cerrors open Vernac +open Vernacexpr open Pcoq open Protectedtoplevel @@ -262,6 +263,7 @@ let rec is_pervasive_exn = function | Error_in_file (_,_,e) -> is_pervasive_exn e | Stdpp.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e + | DuringSyntaxChecking e -> is_pervasive_exn e | _ -> false (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D @@ -270,7 +272,8 @@ let rec is_pervasive_exn = function let print_toplevel_error exc = let (dloc,exc) = match exc with - | DuringCommandInterp (loc,ie) -> + | DuringCommandInterp (loc,ie) + | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) | _ -> (None, exc) in @@ -321,7 +324,8 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ as e -> e + | DuringCommandInterp _ + | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e | e -> if is_pervasive_exn e then e |