Simon Génier pushed to branch source-object at Stefan / Typer

Commits: e3fb3f5e by Simon Génier at 2021-03-24T19:54:15-04:00 [Source] Do not buffer more than one line.

- - - - -

1 changed file:

- src/source.ml

Changes:

===================================== src/source.ml ===================================== @@ -35,7 +35,11 @@ class virtual t = object (self) method virtual current_offset : int

(* Slices the text, from (and including) a starting offset and to (and - excluding) the curent cursor offset. *) + excluding) the curent cursor offset. + + Note that the source is required only to buffer the last line read and may + raise an Invalid_argument if the slice extends before the start of the + line. *) method virtual slice_from_offset : int -> string

(* Moves the cursor forward one byte *) @@ -53,32 +57,36 @@ class source_file file_name = object (self) inherit t

val in_channel = open_in file_name - val bytes = Bytes.create read_buffer_length - val buffer = Buffer.create 4096 + val mutable end_of_line = false + val mutable line = "" + val mutable line_offset = 0 val mutable offset = 0 - val mutable length = 0

method private peek_char_unchecked = - Some (Buffer.nth buffer offset) + if offset < String.length line + then line.[offset] + else '\n'

method peek_char = - if offset < length - then self#peek_char_unchecked + if offset <= String.length line + then Some self#peek_char_unchecked else - match input in_channel bytes 0 read_buffer_length with - | 0 -> None - | read_length - -> Buffer.add_subbytes buffer bytes 0 read_length; - length <- length + read_length; - self#peek_char_unchecked + try + line_offset <- line_offset + 1 + String.length line; + line <- input_line in_channel; + offset <- 0; + Some self#peek_char_unchecked + with + | End_of_file -> None

method advance = offset <- offset + 1

- method current_offset = offset + method current_offset = line_offset + offset

method slice_from_offset start_offset = - Buffer.sub buffer start_offset (offset - start_offset) + let relative_start_offset = start_offset - line_offset in + String.sub line relative_start_offset (offset - relative_start_offset)

method file_name = file_name end

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e3fb3f5ed2217d547b61829b4422c5d207...