diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
| commit | 20d03a28285c430740d0b675583fe5c4d13ffecc (patch) | |
| tree | 36bd87c5c42d948291605fc35b4b7cf573fc8113 /toplevel/toplevel.ml | |
| parent | c0a92523eaa76afabcbaf06ac4a7e8f7930ee4a3 (diff) | |
| parent | 50dc9067e98ca001ad2e875011abab5da6fdb621 (diff) | |
Merge commit 'upstream/8.3.pl1+dfsg' into experimental/master
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 |