# HG changeset patch # User wenzelm # Date 1414786211 -3600 # Node ID 1bb0ad7827b49d1ad68a7fc6388be68022c3b5e7 # Parent ef7700ecce838841eea74e3697fd8ae04ab289fb discontinued obsolete tty and prompt; diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/General/output.ML Fri Oct 31 21:10:11 2014 +0100 @@ -29,7 +29,6 @@ val error_message': serial * string -> unit val error_message: string -> unit val system_message: string -> unit - val prompt: string -> unit val status: string -> unit val report: string list -> unit val result: Properties.T -> string list -> unit @@ -45,7 +44,6 @@ val warning_fn: (output list -> unit) Unsynchronized.ref val error_message_fn: (serial * output list -> unit) Unsynchronized.ref val system_message_fn: (output list -> unit) Unsynchronized.ref - val prompt_fn: (output -> unit) Unsynchronized.ref val status_fn: (output list -> unit) Unsynchronized.ref val report_fn: (output list -> unit) Unsynchronized.ref val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref @@ -101,7 +99,6 @@ val error_message_fn = Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss))); val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); -val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*) val status_fn = Unsynchronized.ref (fn _: output list => ()); val report_fn = Unsynchronized.ref (fn _: output list => ()); val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ()); @@ -115,7 +112,6 @@ fun error_message' (i, s) = ! error_message_fn (i, [output s]); fun error_message s = error_message' (serial (), s); fun system_message s = ! system_message_fn [output s]; -fun prompt s = ! prompt_fn (output s); fun status s = ! status_fn [output s]; fun report ss = ! report_fn (map output ss); fun result props ss = ! result_fn props (map output ss); diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/General/scan.ML Fri Oct 31 21:10:11 2014 +0100 @@ -38,7 +38,6 @@ signature SCAN = sig include BASIC_SCAN - val prompt: string -> ('a -> 'b) -> 'a -> 'b val permissive: ('a -> 'b) -> 'a -> 'b val error: ('a -> 'b) -> 'a -> 'b val catch: ('a -> 'b) -> 'a -> 'b (*exception Fail*) @@ -76,8 +75,8 @@ -> 'b * 'a list -> 'c * ('d * 'a list) val finite: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list val read: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b option - val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b stopper -> - ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a + val drain: ('a -> 'b list * 'a) -> 'b stopper -> ('c * 'b list -> 'd * ('e * 'b list)) -> + ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a type lexicon val is_literal: lexicon -> string list -> bool val literal: lexicon -> (string * 'a) list -> (string * 'a) list * (string * 'a) list @@ -98,14 +97,13 @@ type message = unit -> string; -exception MORE of string option; (*need more input (prompt)*) -exception FAIL of message option; (*try alternatives (reason of failure)*) -exception ABORT of message; (*dead end*) +exception MORE of unit; (*need more input*) +exception FAIL of message option; (*try alternatives (reason of failure)*) +exception ABORT of message; (*dead end*) fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg)); -fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE; -fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE; -fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str); +fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE; +fun strict scan xs = scan xs handle MORE () => raise FAIL NONE; fun error scan xs = scan xs handle ABORT msg => Library.error (msg ()); fun catch scan xs = scan xs @@ -140,11 +138,11 @@ fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs)); fun succeed y xs = (y, xs); -fun some _ [] = raise MORE NONE +fun some _ [] = raise MORE () | some f (x :: xs) = (case f x of SOME y => (y, xs) | _ => raise FAIL NONE); -fun one _ [] = raise MORE NONE +fun one _ [] = raise MORE () | one pred (x :: xs) = if pred x then (x, xs) else raise FAIL NONE; @@ -154,14 +152,14 @@ fun this ys xs = let fun drop_prefix [] xs = xs - | drop_prefix (_ :: _) [] = raise MORE NONE + | drop_prefix (_ :: _) [] = raise MORE () | drop_prefix (y :: ys) (x :: xs) = if (y: string) = x then drop_prefix ys xs else raise FAIL NONE; in (ys, drop_prefix ys xs) end; fun this_string s = this (raw_explode s) >> K s; (*primitive string -- no symbols here!*) -fun many _ [] = raise MORE NONE +fun many _ [] = raise MORE () | many pred (lst as x :: xs) = if pred x then apfst (cons x) (many pred xs) else ([], lst); @@ -265,11 +263,11 @@ (* infinite scans -- draining state-based source *) -fun drain def_prompt get stopper scan ((state, xs), src) = - (scan (state, xs), src) handle MORE prompt => - (case get (the_default def_prompt prompt) src of +fun drain get stopper scan ((state, xs), src) = + (scan (state, xs), src) handle MORE () => + (case get src of ([], _) => (finite' stopper scan (state, xs), src) - | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src')); + | (xs', src') => drain get stopper scan ((state, xs @ xs'), src')); @@ -292,7 +290,8 @@ let fun finish (SOME (res, rest)) = (rev res, rest) | finish NONE = raise FAIL NONE; - fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE + fun scan _ res (Lexicon tab) [] = + if Symtab.is_empty tab then finish res else raise MORE () | scan path res (Lexicon tab) (c :: cs) = (case Symtab.lookup tab (fst c) of SOME (tip, lex) => diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/General/source.ML Fri Oct 31 21:10:11 2014 +0100 @@ -7,8 +7,6 @@ signature SOURCE = sig type ('a, 'b) source - val default_prompt: string - 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: ('a, 'b) source -> ('a * ('a, 'b) source) option @@ -19,7 +17,6 @@ val exhausted: ('a, 'b) source -> ('a, 'a list) source val of_string: string -> (string, string list) source val of_string_limited: int -> string -> (string, substring) source - val tty: TextIO.instream -> (string, unit) source val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option -> ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source @@ -38,37 +35,24 @@ Source of {buffer: 'a list, info: 'b, - prompt: string, - drain: string -> 'b -> 'a list * 'b}; - -fun make_source buffer info prompt drain = - Source {buffer = buffer, info = info, prompt = prompt, drain = drain}; - + drain: 'b -> 'a list * 'b}; -(* prompt *) - -val default_prompt = "> "; - -fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) = - make_source buffer info prompt drain; +fun make_source buffer info drain = + Source {buffer = buffer, info = info, drain = drain}; (* get / unget *) -fun get (Source {buffer = [], info, prompt, drain}) = - let val (xs, info') = drain prompt info - in (xs, make_source [] info' prompt drain) end - | get (Source {buffer, info, prompt, drain}) = - (buffer, make_source [] info prompt drain); +fun get (Source {buffer = [], info, drain}) = + let val (xs, info') = drain info + in (xs, make_source [] info' drain) end + | get (Source {buffer, info, drain}) = (buffer, make_source [] info drain); -fun unget (xs, Source {buffer, info, prompt, drain}) = - make_source (xs @ buffer) info prompt drain; +fun unget (xs, Source {buffer, info, drain}) = make_source (xs @ buffer) info drain; (* variations on get *) -fun get_prompt prompt src = get (set_prompt prompt src); - fun get_single src = (case get src of ([], _) => NONE @@ -82,16 +66,16 @@ (* (map)filter *) -fun drain_map_filter f prompt src = +fun drain_map_filter f src = let - val (xs, src') = get_prompt prompt src; + val (xs, src') = get src; val xs' = map_filter f xs; in if null xs orelse not (null xs') then (xs', src') - else drain_map_filter f prompt src' + else drain_map_filter f src' end; -fun map_filter f src = make_source [] src default_prompt (drain_map_filter f); +fun map_filter f src = make_source [] src (drain_map_filter f); fun filter pred = map_filter (fn x => if pred x then SOME x else NONE); @@ -100,7 +84,7 @@ (* list source *) -fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, [])); +fun of_list xs = make_source [] xs (fn xs => (xs, [])); fun exhausted src = of_list (exhaust src); @@ -110,44 +94,23 @@ val of_string = of_list o raw_explode; fun of_string_limited limit str = - make_source [] (Substring.full str) default_prompt - (fn _ => fn s => + make_source [] (Substring.full str) + (fn s => let val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit)); val cs = map String.str (Substring.explode s1); in (cs, s2) end); -(* stream source *) - -fun slurp_input instream = - let - fun slurp () = - (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of - NONE => [] - | SOME 0 => [] - | SOME _ => TextIO.input instream :: slurp ()); - in maps raw_explode (slurp ()) end; - -fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () => - let val input = slurp_input in_stream in - if exists (fn c => c = "\n") input then (input, ()) - else - (case (Output.prompt prompt; TextIO.inputLine in_stream) of - SOME line => (input @ raw_explode line, ()) - | NONE => (input, ())) - end); - - (** cascade sources **) (* state-based *) -fun drain_source' stopper scan opt_recover prompt (state, src) = +fun drain_source' stopper scan opt_recover (state, src) = let - val drain = Scan.drain prompt get_prompt stopper; - val (xs, s) = get_prompt prompt src; + val drain = Scan.drain get stopper; + val (xs, s) = get src; val inp = ((state, xs), s); val ((ys, (state', xs')), src') = if null xs then (([], (state, [])), s) @@ -162,17 +125,16 @@ in (ys, (state', unget (xs', src'))) end; fun source' init_state stopper scan recover src = - make_source [] (init_state, src) default_prompt (drain_source' stopper scan recover); + make_source [] (init_state, src) (drain_source' stopper scan recover); (* non state-based *) -fun drain_source stopper scan opt_recover prompt = +fun drain_source stopper scan opt_recover = Scan.unlift (drain_source' stopper (Scan.lift scan) - (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover) prompt); + (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover)); fun source stopper scan recover src = - make_source [] src default_prompt (drain_source stopper scan recover); - + make_source [] src (drain_source stopper scan recover); end; diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/General/symbol_pos.ML Fri Oct 31 21:10:11 2014 +0100 @@ -17,7 +17,6 @@ val is_eof: T -> bool val stopper: T Scan.stopper val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a - val change_prompt: ('a -> 'b) -> 'a -> 'b val scan_pos: T list -> Position.T * T list val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list @@ -88,8 +87,6 @@ (case msg of NONE => "" | SOME m => "\n" ^ m ()); in Scan.!! err scan end; -fun change_prompt scan = Scan.prompt "# " scan; - fun $$ s = Scan.one (fn x => symbol x = s); fun ~$$ s = Scan.one (fn x => symbol x <> s); @@ -120,7 +117,7 @@ Scan.ahead ($$ q) |-- !!! (fn () => err_prefix ^ "unclosed string literal") ((scan_pos --| $$$ q) -- - (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)))); + ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))); fun recover_strs q = $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat); @@ -174,7 +171,7 @@ fun scan_cartouche err_prefix = Scan.ahead ($$ "\\") |-- !!! (fn () => err_prefix ^ "unclosed text cartouche") - (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth)); + (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth); val recover_cartouche = Scan.pass 0 scan_cartouche_depth; @@ -205,19 +202,17 @@ val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat); -val scan_body = change_prompt scan_cmts; - in fun scan_comment err_prefix = Scan.ahead ($$ "(" -- $$ "*") |-- !!! (fn () => err_prefix ^ "unclosed comment") - ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")"); + ($$$ "(" @@@ $$$ "*" @@@ scan_cmts @@@ $$$ "*" @@@ $$$ ")"); fun scan_comment_body err_prefix = Scan.ahead ($$ "(" -- $$ "*") |-- !!! (fn () => err_prefix ^ "unclosed comment") - ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")"); + ($$ "(" |-- $$ "*" |-- scan_cmts --| $$ "*" --| $$ ")"); val recover_comment = $$$ "(" @@@ $$$ "*" @@@ scan_cmts; diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Fri Oct 31 21:10:11 2014 +0100 @@ -35,8 +35,6 @@ val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax -> Position.T -> string -> Toplevel.transition list val parse_spans: Token.T list -> Command_Span.span list - type isar - val isar: TextIO.instream -> bool -> isar val side_comments: Token.T list -> Token.T list val command_reports: outer_syntax -> Token.T -> Position.report_text list val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list @@ -84,7 +82,7 @@ fun body cmd (name, _) = (case cmd name of SOME (Command {int_only, parse, ...}) => - Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only)) + Parse.!!! (Parse.tags |-- parse >> pair int_only) | NONE => Scan.succeed (false, Toplevel.imperative (fn () => error ("Bad parser for outer syntax command " ^ quote name)))); @@ -184,8 +182,6 @@ | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing)) end; -fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax); - fun command (spec, pos) comment parse = add_command spec (new_command comment NONE false parse pos); @@ -240,8 +236,7 @@ let val no_terminator = Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof)); - fun recover int = - (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]); + fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]); in src |> Token.source_proper @@ -303,24 +298,6 @@ end; -(* interactive source of toplevel transformers *) - -type isar = - (Toplevel.transition, (Toplevel.transition option, - (Token.T, (Token.T option, (Token.T, (Token.T, - (Symbol_Pos.T, - Position.T * (Symbol.symbol, (Symbol.symbol, (string, unit) Source.source) Source.source) - Source.source) Source.source) Source.source) Source.source) - Source.source) Source.source) Source.source) Source.source; - -fun isar in_stream term : isar = - Source.tty in_stream - |> Symbol.source - |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*) - |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none - |> toplevel_source term (SOME true) lookup_commands_dynamic; - - (* side-comments *) fun cmts (t1 :: t2 :: toks) = diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/Isar/token.ML Fri Oct 31 21:10:11 2014 +0100 @@ -499,8 +499,7 @@ Scan.ahead ($$ "{" -- $$ "*") |-- !!! "unclosed verbatim text" ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- - Symbol_Pos.change_prompt - ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); + ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); val recover_verbatim = $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Fri Oct 31 21:10:11 2014 +0100 @@ -162,7 +162,6 @@ val systemN: string val protocolN: string val legacyN: string val legacy: T - val promptN: string val prompt: T val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: T @@ -547,7 +546,6 @@ val protocolN = "protocol"; val (legacyN, legacy) = markup_elem "legacy"; -val (promptN, prompt) = markup_elem "prompt"; val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; diff -r ef7700ecce83 -r 1bb0ad7827b4 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Fri Oct 31 18:56:59 2014 +0100 +++ b/src/Pure/System/isabelle_process.ML Fri Oct 31 21:10:11 2014 +0100 @@ -126,7 +126,6 @@ (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Output.system_message_fn := message Markup.systemN []; Output.protocol_message_fn := message Markup.protocolN; - Output.prompt_fn := ignore; message Markup.initN [] [Session.welcome ()]; msg_channel end;