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 /toplevel | |
| parent | d6d7a12eb49c997dd83298477e216349fad74c7f (diff) | |
| parent | 7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa (diff) | |
Merge PR #1051: Using an algebraic type for distinguishing toplevel input from location in file
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 d76703d980..444bf8a8f7 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 bfab447706..1602f9c683 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 |