PR#8611: be more conservative (no assert false), and tweak some comments

master
Armaël Guéneau 2019-09-11 20:04:37 +02:00
parent 03ddf295d5
commit c4109d6051
3 changed files with 13 additions and 9 deletions

View File

@ -604,8 +604,9 @@ let lines_around_from_current_input ~start_pos ~end_pos =
match !input_lexbuf, !input_phrase_buffer, !input_name with
| _, Some pb, "//toplevel//" ->
begin match lines_around_from_phrasebuf pb ~start_pos ~end_pos with
| [] -> (* Couldn't get input from phrase buffer, raise an error *)
assert false
| [] -> (* Could not read the input from the phrase buffer. This is likely
a sign that we were given a buggy location. *)
[]
| lines ->
lines
end

View File

@ -73,10 +73,12 @@ val mkloc : 'a -> t -> 'a loc
val input_name: string ref
val input_lexbuf: Lexing.lexbuf option ref
(* Used by the Error Reporting Code if [!input_name] is
//toplevel// [!input_phrase_buffer] is Some buf
where buf is the last toplevel phrase and otherwise
[!input_phrase_buffer] is None *)
(* This is used for reporting errors coming from the toplevel.
When running a toplevel session (i.e. when [!input_name] is "//toplevel//"),
[!input_phrase_buffer] should be [Some buf] where [buf] contains the last
toplevel phrase. *)
val input_phrase_buffer: Buffer.t option ref

View File

@ -36,7 +36,8 @@ type directive_info = {
doc: string;
}
(* Phase Buffer that Stores the Last Toplevel Phrase *)
(* Phase buffer that stores the last toplevel phrase (see
[Location.input_phrase_buffer]). *)
let phrase_buffer = Buffer.create 1024
(* The table of toplevel value bindings and its accessors *)
@ -450,7 +451,7 @@ let read_input_default prompt buffer len =
if !i >= len then raise Exit;
let c = input_char stdin in
Bytes.set buffer !i c;
(* Populate Phrase Buffer as new characters are added *)
(* Also populate the phrase buffer as new characters are added. *)
Buffer.add_char phrase_buffer c;
incr i;
if c = '\n' then raise Exit;
@ -557,7 +558,7 @@ let loop ppf =
let snap = Btype.snapshot () in
try
Lexing.flush_input lb;
(* Reset the phrase buffer when we flush the lexing buffer *)
(* Reset the phrase buffer when we flush the lexing buffer. *)
Buffer.reset phrase_buffer;
Location.reset();
Warnings.reset_fatal ();