aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqloop.ml6
-rw-r--r--toplevel/vernac.ml42
2 files changed, 24 insertions, 24 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4641a2bc8..ab360f98d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -146,13 +146,10 @@ let print_highlight_location ib loc =
highlight_lines
let valid_buffer_loc ib loc =
- not (Loc.is_ghost loc) &&
let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
(* This is specific to the toplevel *)
-let pr_loc loc =
- if Loc.is_ghost loc then str"<unknown>"
- else
+let pr_loc ?loc = Option.default (fun loc ->
let fname = loc.Loc.fname in
if CString.equal fname "" then
Loc.(str"Toplevel input, characters " ++ int loc.bp ++
@@ -162,6 +159,7 @@ let pr_loc loc =
str", line " ++ int loc.line_nb ++ str", characters " ++
int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
str":")
+ ) loc
(* Toplevel error explanation. *)
let error_info_for_buffer ?loc buf =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d6bcd2f15..3a67f4cbf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -21,11 +21,12 @@ open Vernacprop
let checknav_simple (loc, cmd) =
if is_navigation_vernac cmd && not (is_reset cmd) then
- CErrors.user_err ~loc (str "Navigation commands forbidden in files.")
+ CErrors.user_err ?loc (str "Navigation commands forbidden in files.")
let checknav_deep (loc, ast) =
if is_deep_navigation_vernac ast then
- CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.")
+ CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
+
let disable_drop = function
| Drop -> CErrors.error "Drop is forbidden."
@@ -33,10 +34,12 @@ let disable_drop = function
(* Echo from a buffer based on position.
XXX: Should move to utility file. *)
-let vernac_echo loc in_chan = let open Loc in
- let len = loc.ep - loc.bp in
- seek_in in_chan loc.bp;
- Feedback.msg_notice @@ str @@ really_input_string in_chan len
+let vernac_echo ?loc in_chan = let open Loc in
+ Option.iter (fun loc ->
+ let len = loc.ep - loc.bp in
+ seek_in in_chan loc.bp;
+ Feedback.msg_notice @@ str @@ really_input_string in_chan len
+ ) loc
(* vernac parses the given stream, executes interpfun on the syntax tree it
* parses, and is verbose on "primitives" commands if verbosely is true *)
@@ -49,8 +52,8 @@ let set_formatter_translator ch =
Format.set_formatter_output_functions out (fun () -> flush ch);
Format.set_max_boxes max_int
-let pr_new_syntax_in_context loc chan_beautify ocom =
- let loc = Loc.unloc loc in
+let pr_new_syntax_in_context ?loc chan_beautify ocom =
+ let loc = Option.cata Loc.unloc (0,0) loc in
if !beautify_file then set_formatter_translator chan_beautify;
let fs = States.freeze ~marshallable:`No in
(* The content of this is not supposed to fail, but if ever *)
@@ -72,14 +75,14 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
States.unfreeze fs;
Format.set_formatter_out_channel stdout
-let pr_new_syntax po loc chan_beautify ocom =
+let pr_new_syntax ?loc po chan_beautify ocom =
(* Reinstall the context of parsing which includes the bindings of comments to locations *)
- Pcoq.Gram.with_parsable po (pr_new_syntax_in_context chan_beautify loc) ocom
+ Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc chan_beautify) ocom
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
-let pp_cmd_header loc com =
+let pp_cmd_header ?loc com =
let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
let noblank s = String.map (fun c ->
match c with
@@ -87,7 +90,7 @@ let pp_cmd_header loc com =
| x -> x
) s
in
- let (start,stop) = Loc.unloc loc in
+ let (start,stop) = Option.cata Loc.unloc (0,0) loc in
let safe_pr_vernac x =
try Ppvernac.pr_vernac x
with e -> str (Printexc.to_string e) in
@@ -98,9 +101,8 @@ let pp_cmd_header loc com =
(* This is a special case where we assume we are in console batch mode
and take control of the console.
*)
-(* FIXME *)
-let print_cmd_header loc com =
- Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
+let print_cmd_header ?loc com =
+ Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com);
Format.pp_print_flush !Topfmt.std_ft ()
let pr_open_cur_subgoals () =
@@ -141,14 +143,14 @@ let rec interp_vernac sid po (loc,com) =
try
(* The -time option is only supported from console-based
clients due to the way it prints. *)
- if !Flags.time then print_cmd_header loc com;
+ if !Flags.time then print_cmd_header ?loc com;
let com = if !Flags.time then VernacTime (loc,com) else com in
interp com
with reraise ->
let (reraise, info) = CErrors.push reraise in
let info = begin
match Loc.get_loc info with
- | None -> Loc.add_loc info loc
+ | None -> Option.cata (Loc.add_loc info) info loc
| Some _ -> info
end in iraise (reraise, info)
@@ -177,8 +179,8 @@ and load_vernac verbosely sid file =
in
(* Printing of vernacs *)
- if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast);
- Option.iter (vernac_echo loc) in_echo;
+ if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
+ Option.iter (vernac_echo ?loc) in_echo;
checknav_simple (loc, ast);
let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in
@@ -193,7 +195,7 @@ and load_vernac verbosely sid file =
| Stm.End_of_input ->
(* Is this called so comments at EOF are printed? *)
if !beautify then
- pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None;
+ pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None;
if !Flags.beautify_file then close_out chan_beautify;
!rsid
| reraise ->