diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 1 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 11 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 5 |
3 files changed, 12 insertions, 5 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 3522027b9..913f1250d 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -20,6 +20,7 @@ let print_loc loc = if loc = dummy_loc then (str"<unknown>") else + let loc = unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 012019852..36c3ff3dc 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -103,7 +103,8 @@ let dotted_location (b,e) = else (String.make (e-b-1) '.', " ") -let print_highlight_location ib (bp,ep) = +let print_highlight_location ib loc = + let (bp,ep) = unloc loc in let bp = bp - ib.start and ep = ep - ib.start in let highlight_lines = @@ -124,7 +125,7 @@ let print_highlight_location ib (bp,ep) = str sn ++ str dn) in (l1 ++ li ++ ln) in - (str"Toplevel input, characters " ++ Cerrors.print_loc (bp,ep) ++ fnl () ++ + (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) @@ -138,6 +139,7 @@ let print_location_in_file s inlibrary fname (bp,ep) = (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ()) else + let (bp,ep) = unloc (bp,ep) in let ic = open_in fname in let rec line_of_pos lin bol cnt = if cnt < bp then @@ -151,7 +153,7 @@ let print_location_in_file s inlibrary fname (bp,ep) = close_in ic; (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str", line " ++ int line ++ - str", characters " ++ Cerrors.print_loc (bp-bol,ep-bol) ++ fnl ()) + str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ fnl ()) with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ())) let print_command_location ib dloc = @@ -168,7 +170,8 @@ let valid_loc dloc (b,e) = | _ -> true let valid_buffer_loc ib dloc (b,e) = - valid_loc dloc (b,e) & b-ib.start >= 0 & e-ib.start < ib.len & b<=e + valid_loc dloc (b,e) & + let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f339159b4..3cc2ba4f8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -72,6 +72,7 @@ let close_input in_chan (_,verb) = with _ -> () let verbose_phrase verbch loc = + let loc = unloc loc in match verbch with | Some ch -> let len = snd loc - fst loc in @@ -131,6 +132,7 @@ let pre_printing = function let post_printing loc (env,t,f,n) = function | VernacSolve (i,_,deftac) -> + let loc = unloc loc in set_formatter_translator(); let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in (if !translate_file then begin @@ -142,6 +144,7 @@ let post_printing loc (env,t,f,n) = function | _ -> () let pr_new_syntax loc ocom = + let loc = unloc loc in if !translate_file then set_formatter_translator(); let fs = States.freeze () in let com = match ocom with @@ -255,7 +258,7 @@ and read_vernac_file verbosely s = close_input in_chan input; (* we must close the file first *) match real_error e with | End_of_input -> - if do_translate () then pr_new_syntax (max_int,max_int) None + if do_translate () then pr_new_syntax (make_loc (max_int,max_int)) None | _ -> raise_with_file fname e (* raw_do_vernac : char Stream.t -> unit |