diff options
| -rw-r--r-- | .depend | 12 | ||||
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | toplevel/line_oriented_parser.ml | 22 | ||||
| -rw-r--r-- | toplevel/line_oriented_parser.mli | 6 | ||||
| -rw-r--r-- | toplevel/protectedtoplevel.ml | 21 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
6 files changed, 40 insertions, 27 deletions
@@ -1049,6 +1049,8 @@ toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx library/global.cmx \ parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx kernel/type_errors.cmx lib/util.cmx \ toplevel/himsg.cmi +toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi +toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \ parsing/extend.cmi library/lib.cmi library/libobject.cmi \ @@ -1069,11 +1071,13 @@ toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \ parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \ kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx -toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \ - lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \ +toplevel/protectedtoplevel.cmo: toplevel/errors.cmi \ + toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \ + toplevel/vernac.cmi toplevel/vernacinterp.cmi \ toplevel/protectedtoplevel.cmi -toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmx \ - lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \ +toplevel/protectedtoplevel.cmx: toplevel/errors.cmx \ + toplevel/line_oriented_parser.cmx parsing/pcoq.cmx lib/pp.cmx \ + toplevel/vernac.cmx toplevel/vernacinterp.cmx \ toplevel/protectedtoplevel.cmi toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ toplevel/command.cmi parsing/coqast.cmi kernel/declarations.cmi \ @@ -110,8 +110,9 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \ toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \ toplevel/record.cmo toplevel/discharge.cmo toplevel/vernacinterp.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \ - toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \ - toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo + toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ + toplevel/toplevel.cmo toplevel/usage.cmo \ + toplevel/coqinit.cmo toplevel/coqtop.cmo HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ tactics/inv.cmo tactics/leminv.cmo tactics/eauto.cmo \ diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml new file mode 100644 index 000000000..780780412 --- /dev/null +++ b/toplevel/line_oriented_parser.ml @@ -0,0 +1,22 @@ + +(* $Id$ *) + +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 diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli new file mode 100644 index 000000000..866cfc3df --- /dev/null +++ b/toplevel/line_oriented_parser.mli @@ -0,0 +1,6 @@ + +(* $Id$ *) + +val line_oriented_channel_to_option: string -> in_channel -> int -> char option + +val flush_until_end_of_stream : 'a Stream.t -> unit diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index 7af6dcc89..cc1284718 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 diff --git a/toplevel/usage.ml b/toplevel/usage.ml index a87e61bc5..d5a5a7aec 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -24,7 +24,6 @@ let print_usage_channel co command = -require f load Coq object file f.vo and import it (Require f.) -opt run the native-code version of Coq or Coq_SearchIsos - -full run the native-code version of Coq with all tactics -image f specify an alternative binary image f -bindir dir specify an alternative directory for the binaries -libdir dir specify an alternative directory for the library |