diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
| commit | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch) | |
| tree | b04b45d1a6f42d19b1428c522d647afbad2f9b83 /toplevel/toplevel.ml | |
| parent | 3e96002677226c0cdaa8f355938a76cfb37a722a (diff) | |
Imported Upstream version 8.3pl1upstream/8.3pl1
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9594c988..299214f0 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: toplevel.ml 13668 2010-12-02 17:43:59Z herbelin $ *) open Pp open Util @@ -276,7 +276,6 @@ 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 @@ -285,8 +284,7 @@ let rec is_pervasive_exn = function let print_toplevel_error exc = let (dloc,exc) = match exc with - | DuringCommandInterp (loc,ie) - | DuringSyntaxChecking (loc,ie) -> + | DuringCommandInterp (loc,ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) | _ -> (None, exc) in @@ -335,8 +333,7 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ - | DuringSyntaxChecking _ as e -> e + | DuringCommandInterp _ as e -> e | e -> if is_pervasive_exn e then e |