diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/coqloop.ml | 6 | ||||
-rw-r--r-- | toplevel/vernac.ml | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d76703d98..444bf8a8f 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -155,14 +155,16 @@ let error_info_for_buffer ?loc buf = let fname = loc.Loc.fname in let hl, loc = (* We are in the toplevel *) - if CString.equal fname "" then + match fname with + | Loc.ToplevelInput -> let nloc = adjust_loc_buf buf loc in if valid_buffer_loc buf loc then (fnl () ++ print_highlight_location buf nloc, nloc) (* in the toplevel, but not a valid buffer *) else (mt (), nloc) (* we are in batch mode, don't adjust location *) - else (mt (), loc) + | Loc.InFile _ -> + (mt (), loc) in Topfmt.pr_loc loc ++ hl ) loc diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bfab44770..1602f9c68 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -182,7 +182,7 @@ and load_vernac verbosely sid file = if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in let in_chan = open_utf8_file_in file in let in_echo = if verbosely then Some (open_utf8_file_in file) else None in - let in_pa = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in + let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let rsid = ref sid in try (* we go out of the following infinite loop when a End_of_input is |