diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 42 |
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 -> |