diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-05 13:10:03 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-05 13:10:03 +0000 |
| commit | 2e59cf3c09a8ee2c7b0dc97551f3c26497f4b67d (patch) | |
| tree | 5aa0b84090ec3e29bf13789caa053a6121234f52 /toplevel | |
| parent | ee9fb9cf68d9741eda95995ff59fee94c82f527a (diff) | |
More emacs-friendly error messages.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10882 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/toplevel.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index f5044f1dc..1ae876633 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -134,7 +134,7 @@ let print_highlight_location ib loc = (l1 ++ li ++ ln) in let loc = make_loc (bp,ep) in - (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++ + (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) @@ -162,7 +162,7 @@ let print_location_in_file s inlibrary fname loc = close_in ic; (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str", line " ++ int line ++ - str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ fnl ()) + str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ str":" ++ fnl ()) with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ())) let print_command_location ib dloc = |