discontinued obsolete tty and prompt;

--- 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);

--- 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) =>

--- 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;

--- 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 ($$ "\\<open>") |--
     !!! (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;

--- 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) =

--- 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);

--- 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";

--- 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;