# HG changeset patch # User wenzelm # Date 895590978 -7200 # Node ID d8e5c6e31854db7fd49d465ead0e780ae4d802d8 # Parent d8c809afafb8d0ef2b9c213b918aad528eff4e9c prompt made part of source; diff -r d8c809afafb8 -r d8e5c6e31854 src/Pure/Syntax/source.ML --- a/src/Pure/Syntax/source.ML Tue May 19 17:15:30 1998 +0200 +++ b/src/Pure/Syntax/source.ML Tue May 19 17:16:18 1998 +0200 @@ -3,23 +3,19 @@ Author: Markus Wenzel, TU Muenchen Co-algebraic data sources. - -TODO: - - proper handling of interrupts (?); - - recovery from scan errors (?); - - make prompt part of source (?); *) signature SOURCE = sig type ('a, 'b) source - val get: string -> ('a, 'b) source -> 'a list * ('a, 'b) source + val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source + val get: ('a, 'b) source -> 'a list * ('a, 'b) source val unget: 'a list * ('a, 'b) source -> ('a, 'b) source - val get_single: string -> ('a, 'b) source -> 'a * ('a, 'b) source - val exhaust: string -> ('a, 'b) source -> 'a list + val get_single: ('a, 'b) source -> 'a * ('a, 'b) source + val exhaust: ('a, 'b) source -> 'a list val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source - val of_list: int option -> 'a list -> ('a, 'a list) source - val of_string: int option -> string -> (string, string list) source + val of_list: 'a list -> ('a, 'a list) source + val of_string: string -> (string, string list) source val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source val tty: (string, unit) source val state_source: 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) @@ -39,40 +35,53 @@ Source of {buffer: 'a list, info: 'b, + prompt: string option, drain: string -> 'b -> 'a list * 'b}; -fun make_source buffer info drain = - Source {buffer = buffer, info = info, drain = drain}; +fun make_source buffer info prompt drain = + Source {buffer = buffer, info = info, prompt = prompt, drain = drain}; + + +(* prompt *) + +val default_prompt = "> "; + +fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) = + make_source buffer info (Some prompt) drain; (* get / unget *) -fun get prompt (Source {buffer = [], info, drain}) = - let val (xs, info') = drain prompt info - in (xs, make_source [] info' drain) end - | get _ (Source {buffer, info, drain}) = - (buffer, make_source [] info drain); +fun get (Source {buffer = [], info, prompt, drain}) = + let val (xs, info') = drain (if_none prompt default_prompt) info + in (xs, make_source [] info' prompt drain) end + | get (Source {buffer, info, prompt, drain}) = + (buffer, make_source [] info prompt drain); -fun unget (xs, Source {buffer, info, drain}) = - make_source (xs @ buffer) info drain; +fun unget (xs, Source {buffer, info, prompt, drain}) = + make_source (xs @ buffer) info prompt drain; -fun get_single prompt src = - (case get prompt src of +(* variations on get *) + +fun get_prompt prompt src = get (set_prompt prompt src); + +fun get_single src = + (case get src of ([], _) => error "Input source exhausted!" | (x :: xs, src') => (x, unget (xs, src'))); -fun exhaust prompt src = - (case get prompt src of +fun exhaust src = + (case get src of ([], _) => [] - | (xs, src') => xs @ exhaust prompt src'); + | (xs, src') => xs @ exhaust src'); (* filter *) fun drain_filter pred prompt src = let - val (xs, src') = get prompt src; + val (xs, src') = get src; val xs' = Library.filter pred xs; in if null xs then (xs, src') @@ -80,7 +89,7 @@ else (xs', src') end; -fun filter pred src = make_source [] src (drain_filter pred); +fun filter pred src = make_source [] src None (drain_filter pred); @@ -88,13 +97,13 @@ (* list source *) -fun drain_list _ xs = (xs, []); -fun drain_list_limit n _ xs = (take (n, xs), drop (n, xs)); +(*limiting the master input buffer considerably improves performance*) +val limit = 4000; -fun of_list None xs = make_source [] xs drain_list - | of_list (Some n) xs = make_source [] xs (drain_list_limit (Int.max (n, 1))); +fun drain_list _ xs = (take (limit, xs), drop (limit, xs)); -fun of_string limit str = of_list limit (explode str); +fun of_list xs = make_source [] xs None drain_list; +fun of_string str = of_list (explode str); (* stream source *) @@ -105,7 +114,7 @@ (explode (TextIO.inputLine instream), ())); fun of_stream instream outstream = - make_source [] () (drain_stream instream outstream); + make_source [] () None (drain_stream instream outstream); val tty = of_stream TextIO.stdIn TextIO.stdOut; @@ -116,26 +125,26 @@ (* make state-based *) fun drain_state_source stopper scan prompt state_src = - Scan.source prompt get unget stopper scan state_src; + Scan.source prompt get_prompt unget stopper scan state_src; fun state_source init_state stopper scan src = - make_source [] (init_state, src) (drain_state_source stopper scan); + make_source [] (init_state, src) None (drain_state_source stopper scan); (* not state-based *) fun drain_source stopper scan prompt src = - apsnd snd (Scan.source prompt get unget stopper (Scan.lift scan) ((), src)); + apsnd snd (Scan.source prompt get_prompt unget stopper (Scan.lift scan) ((), src)); fun source stopper scan src = - make_source [] src (drain_source stopper scan); + make_source [] src None (drain_source stopper scan); (** test source interactively **) fun test str_of src = - (case get ">> " src handle Interrupt => ([], src) of + (case get src handle Interrupt => ([], src) of ([], _) => writeln "Terminated." | (xs, src') => (seq writeln (map str_of xs); test str_of src'));