diff options
| author | Maxime Dénès | 2017-09-15 10:42:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-15 10:42:13 +0200 |
| commit | 9e6b192adcaadcdb1935a68f39ce5ea877562188 (patch) | |
| tree | c0b66a5665b1068c694466e8c64ec57c748530fb /vernac | |
| parent | d6d7a12eb49c997dd83298477e216349fad74c7f (diff) | |
| parent | 7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa (diff) | |
Merge PR #1051: Using an algebraic type for distinguishing toplevel input from location in file
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/topfmt.ml | 5 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e7b14309d1..6a10eb43a2 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -292,10 +292,11 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in - if CString.equal fname "" then + match fname with + | Loc.ToplevelInput -> Loc.(str"Toplevel input, characters " ++ int loc.bp ++ str"-" ++ int loc.ep ++ str":") - else + | Loc.InFile fname -> Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ str", line " ++ int loc.line_nb ++ str", characters " ++ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d2ba9eb1cc..22306ac5bf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1902,7 +1902,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in + Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in try while true do interp (snd (parse_sentence input)) done with End_of_input -> () |