diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7991d0e58..feaa8c970 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -13,7 +13,6 @@ open Flags open Cerrors open Vernac open Pcoq -open Compat (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -124,7 +123,7 @@ let blanch_utf8_string s bp ep = String.sub s' 0 !j let print_highlight_location ib loc = - let (bp,ep) = unloc loc in + let (bp,ep) = Loc.unloc loc in let bp = bp - ib.start and ep = ep - ib.start in let highlight_lines = @@ -146,7 +145,7 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in - let loc = make_loc (bp,ep) in + let loc = Loc.make_loc (bp,ep) in (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ highlight_lines ++ fnl ()) @@ -154,7 +153,7 @@ let print_highlight_location ib loc = let print_location_in_file s inlibrary fname loc = let errstrm = str"Error while reading " ++ str s in - if loc = dummy_loc then + if loc = Loc.ghost then hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl () else let errstrm = @@ -163,7 +162,7 @@ let print_location_in_file s inlibrary fname loc = hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++ str"characters " ++ Cerrors.print_loc loc) ++ fnl () else - let (bp,ep) = unloc loc in + let (bp,ep) = Loc.unloc loc in let ic = open_in fname in let rec line_of_pos lin bol cnt = if cnt < bp then @@ -178,7 +177,7 @@ let print_location_in_file s inlibrary fname loc = 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":" ++ + Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () with e -> (close_in ic; @@ -192,15 +191,15 @@ let print_command_location ib dloc = | None -> (mt ()) let valid_loc dloc loc = - loc <> dummy_loc + loc <> Loc.ghost & match dloc with | Some dloc -> - let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed + let (bd,ed) = Loc.unloc dloc in let (b,e) = Loc.unloc loc in bd<=b & e<=ed | _ -> true let valid_buffer_loc ib dloc loc = valid_loc dloc loc & - let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e + let (b,e) = Loc.unloc loc 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 @@ -283,7 +282,7 @@ let print_toplevel_error exc = let (dloc,exc) = match exc with | DuringCommandInterp (loc,ie) -> - if loc = dummy_loc then (None,ie) else (Some loc, ie) + if loc = Loc.ghost then (None,ie) else (Some loc, ie) | _ -> (None, exc) in let (locstrm,exc) = @@ -312,7 +311,7 @@ let print_toplevel_error exc = (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot st = match get_tok (Stream.next st) with + let rec dot st = match Compat.get_tok (Stream.next st) with | Tok.KEYWORD "." -> () | Tok.EOI -> raise End_of_input | _ -> dot st |