From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- toplevel/coqloop.ml | 6 ++---- toplevel/vernac.ml | 42 ++++++++++++++++++++++-------------------- 2 files changed, 24 insertions(+), 24 deletions(-) (limited to 'toplevel') 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"" - 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 -> -- cgit v1.2.3