diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
commit | da178a880e3ace820b41d38b191d3785b82991f5 (patch) | |
tree | 6356ab3164a5ad629f4161dc6c44ead74edc2937 /toplevel/toplevel.ml | |
parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) |
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
Diffstat (limited to 'toplevel/toplevel.ml')
-rw-r--r-- | toplevel/toplevel.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index a1acd1d6..9d64f983 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *) open Pp open Util @@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc = try let (line, bol) = line_of_pos 1 0 0 in close_in ic; - hov 0 - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++ - hov 0 (str"line " ++ int line ++ str"," ++ spc() ++ - str"characters " ++ - Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++ + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + str", line " ++ int line ++ str", characters " ++ + Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () with e -> (close_in ic; @@ -316,7 +315,7 @@ let parse_to_dot = let rec discard_to_dot () = try Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,Token.Error _) -> + with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> discard_to_dot() |