diff options
Diffstat (limited to 'toplevel/protectedtoplevel.ml')
| -rw-r--r-- | toplevel/protectedtoplevel.ml | 21 |
1 files changed, 1 insertions, 20 deletions
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index 7af6dcc894..cc12847188 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -2,6 +2,7 @@ (* $Id$ *) open Pp +open Line_oriented_parser open Vernac (* The toplevel parsing loop we propose here is more robust to printing @@ -60,26 +61,6 @@ let set_start_marker s = let set_end_marker s = end_marker := s -let line_oriented_channel_to_option stop_string input_channel = - let count = ref 0 in - let buff = ref "" in - let current_length = ref 0 in - fun i -> - if (i - !count) >= !current_length then begin - count := !count + !current_length + 1; - buff := input_line input_channel; - if !buff = stop_string then - None - else begin - current_length := String.length !buff; - Some '\n' - end - end else - Some (String.get !buff (i - !count)) - -let flush_until_end_of_stream char_stream = - Stream.iter (function _ -> ()) char_stream - let rec parse_one_command input_channel = let this_line = input_line input_channel in if ((String.length this_line) >= !start_length) then begin |