diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /toplevel/toplevel.ml | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
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 |