discontinued obsolete tty and prompt;
authorwenzelm
Fri Oct 31 21:10:11 2014 +0100 (2014-10-31)
changeset 588501bb0ad7827b4
parent 58849 ef7700ecce83
child 58851 897f266c44b3
discontinued obsolete tty and prompt;
src/Pure/General/output.ML
src/Pure/General/scan.ML
src/Pure/General/source.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/markup.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/General/output.ML	Fri Oct 31 18:56:59 2014 +0100
     1.2 +++ b/src/Pure/General/output.ML	Fri Oct 31 21:10:11 2014 +0100
     1.3 @@ -29,7 +29,6 @@
     1.4    val error_message': serial * string -> unit
     1.5    val error_message: string -> unit
     1.6    val system_message: string -> unit
     1.7 -  val prompt: string -> unit
     1.8    val status: string -> unit
     1.9    val report: string list -> unit
    1.10    val result: Properties.T -> string list -> unit
    1.11 @@ -45,7 +44,6 @@
    1.12    val warning_fn: (output list -> unit) Unsynchronized.ref
    1.13    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    1.14    val system_message_fn: (output list -> unit) Unsynchronized.ref
    1.15 -  val prompt_fn: (output -> unit) Unsynchronized.ref
    1.16    val status_fn: (output list -> unit) Unsynchronized.ref
    1.17    val report_fn: (output list -> unit) Unsynchronized.ref
    1.18    val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    1.19 @@ -101,7 +99,6 @@
    1.20  val error_message_fn =
    1.21    Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.22  val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.23 -val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
    1.24  val status_fn = Unsynchronized.ref (fn _: output list => ());
    1.25  val report_fn = Unsynchronized.ref (fn _: output list => ());
    1.26  val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
    1.27 @@ -115,7 +112,6 @@
    1.28  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    1.29  fun error_message s = error_message' (serial (), s);
    1.30  fun system_message s = ! system_message_fn [output s];
    1.31 -fun prompt s = ! prompt_fn (output s);
    1.32  fun status s = ! status_fn [output s];
    1.33  fun report ss = ! report_fn (map output ss);
    1.34  fun result props ss = ! result_fn props (map output ss);
     2.1 --- a/src/Pure/General/scan.ML	Fri Oct 31 18:56:59 2014 +0100
     2.2 +++ b/src/Pure/General/scan.ML	Fri Oct 31 21:10:11 2014 +0100
     2.3 @@ -38,7 +38,6 @@
     2.4  signature SCAN =
     2.5  sig
     2.6    include BASIC_SCAN
     2.7 -  val prompt: string -> ('a -> 'b) -> 'a -> 'b
     2.8    val permissive: ('a -> 'b) -> 'a -> 'b
     2.9    val error: ('a -> 'b) -> 'a -> 'b
    2.10    val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
    2.11 @@ -76,8 +75,8 @@
    2.12      -> 'b * 'a list -> 'c * ('d * 'a list)
    2.13    val finite: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
    2.14    val read: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
    2.15 -  val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b stopper ->
    2.16 -    ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
    2.17 +  val drain: ('a -> 'b list * 'a) -> 'b stopper -> ('c * 'b list -> 'd * ('e * 'b list)) ->
    2.18 +    ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
    2.19    type lexicon
    2.20    val is_literal: lexicon -> string list -> bool
    2.21    val literal: lexicon -> (string * 'a) list -> (string * 'a) list * (string * 'a) list
    2.22 @@ -98,14 +97,13 @@
    2.23  
    2.24  type message = unit -> string;
    2.25  
    2.26 -exception MORE of string option;        (*need more input (prompt)*)
    2.27 -exception FAIL of message option;       (*try alternatives (reason of failure)*)
    2.28 -exception ABORT of message;             (*dead end*)
    2.29 +exception MORE of unit;  (*need more input*)
    2.30 +exception FAIL of message option;  (*try alternatives (reason of failure)*)
    2.31 +exception ABORT of message;  (*dead end*)
    2.32  
    2.33  fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
    2.34 -fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    2.35 -fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
    2.36 -fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
    2.37 +fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    2.38 +fun strict scan xs = scan xs handle MORE () => raise FAIL NONE;
    2.39  fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
    2.40  
    2.41  fun catch scan xs = scan xs
    2.42 @@ -140,11 +138,11 @@
    2.43  fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
    2.44  fun succeed y xs = (y, xs);
    2.45  
    2.46 -fun some _ [] = raise MORE NONE
    2.47 +fun some _ [] = raise MORE ()
    2.48    | some f (x :: xs) =
    2.49        (case f x of SOME y => (y, xs) | _ => raise FAIL NONE);
    2.50  
    2.51 -fun one _ [] = raise MORE NONE
    2.52 +fun one _ [] = raise MORE ()
    2.53    | one pred (x :: xs) =
    2.54        if pred x then (x, xs) else raise FAIL NONE;
    2.55  
    2.56 @@ -154,14 +152,14 @@
    2.57  fun this ys xs =
    2.58    let
    2.59      fun drop_prefix [] xs = xs
    2.60 -      | drop_prefix (_ :: _) [] = raise MORE NONE
    2.61 +      | drop_prefix (_ :: _) [] = raise MORE ()
    2.62        | drop_prefix (y :: ys) (x :: xs) =
    2.63            if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
    2.64    in (ys, drop_prefix ys xs) end;
    2.65  
    2.66  fun this_string s = this (raw_explode s) >> K s;  (*primitive string -- no symbols here!*)
    2.67  
    2.68 -fun many _ [] = raise MORE NONE
    2.69 +fun many _ [] = raise MORE ()
    2.70    | many pred (lst as x :: xs) =
    2.71        if pred x then apfst (cons x) (many pred xs)
    2.72        else ([], lst);
    2.73 @@ -265,11 +263,11 @@
    2.74  
    2.75  (* infinite scans -- draining state-based source *)
    2.76  
    2.77 -fun drain def_prompt get stopper scan ((state, xs), src) =
    2.78 -  (scan (state, xs), src) handle MORE prompt =>
    2.79 -    (case get (the_default def_prompt prompt) src of
    2.80 +fun drain get stopper scan ((state, xs), src) =
    2.81 +  (scan (state, xs), src) handle MORE () =>
    2.82 +    (case get src of
    2.83        ([], _) => (finite' stopper scan (state, xs), src)
    2.84 -    | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src'));
    2.85 +    | (xs', src') => drain get stopper scan ((state, xs @ xs'), src'));
    2.86  
    2.87  
    2.88  
    2.89 @@ -292,7 +290,8 @@
    2.90    let
    2.91      fun finish (SOME (res, rest)) = (rev res, rest)
    2.92        | finish NONE = raise FAIL NONE;
    2.93 -    fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE
    2.94 +    fun scan _ res (Lexicon tab) [] =
    2.95 +          if Symtab.is_empty tab then finish res else raise MORE ()
    2.96        | scan path res (Lexicon tab) (c :: cs) =
    2.97            (case Symtab.lookup tab (fst c) of
    2.98              SOME (tip, lex) =>
     3.1 --- a/src/Pure/General/source.ML	Fri Oct 31 18:56:59 2014 +0100
     3.2 +++ b/src/Pure/General/source.ML	Fri Oct 31 21:10:11 2014 +0100
     3.3 @@ -7,8 +7,6 @@
     3.4  signature SOURCE =
     3.5  sig
     3.6    type ('a, 'b) source
     3.7 -  val default_prompt: string
     3.8 -  val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
     3.9    val get: ('a, 'b) source -> 'a list * ('a, 'b) source
    3.10    val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
    3.11    val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
    3.12 @@ -19,7 +17,6 @@
    3.13    val exhausted: ('a, 'b) source -> ('a, 'a list) source
    3.14    val of_string: string -> (string, string list) source
    3.15    val of_string_limited: int -> string -> (string, substring) source
    3.16 -  val tty: TextIO.instream -> (string, unit) source
    3.17    val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    3.18      (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
    3.19      ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
    3.20 @@ -38,37 +35,24 @@
    3.21    Source of
    3.22     {buffer: 'a list,
    3.23      info: 'b,
    3.24 -    prompt: string,
    3.25 -    drain: string -> 'b -> 'a list * 'b};
    3.26 -
    3.27 -fun make_source buffer info prompt drain =
    3.28 -  Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
    3.29 -
    3.30 +    drain: 'b -> 'a list * 'b};
    3.31  
    3.32 -(* prompt *)
    3.33 -
    3.34 -val default_prompt = "> ";
    3.35 -
    3.36 -fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
    3.37 -  make_source buffer info prompt drain;
    3.38 +fun make_source buffer info drain =
    3.39 +  Source {buffer = buffer, info = info, drain = drain};
    3.40  
    3.41  
    3.42  (* get / unget *)
    3.43  
    3.44 -fun get (Source {buffer = [], info, prompt, drain}) =
    3.45 -      let val (xs, info') = drain prompt info
    3.46 -      in (xs, make_source [] info' prompt drain) end
    3.47 -  | get (Source {buffer, info, prompt, drain}) =
    3.48 -      (buffer, make_source [] info prompt drain);
    3.49 +fun get (Source {buffer = [], info, drain}) =
    3.50 +      let val (xs, info') = drain info
    3.51 +      in (xs, make_source [] info' drain) end
    3.52 +  | get (Source {buffer, info, drain}) = (buffer, make_source [] info drain);
    3.53  
    3.54 -fun unget (xs, Source {buffer, info, prompt, drain}) =
    3.55 -  make_source (xs @ buffer) info prompt drain;
    3.56 +fun unget (xs, Source {buffer, info, drain}) = make_source (xs @ buffer) info drain;
    3.57  
    3.58  
    3.59  (* variations on get *)
    3.60  
    3.61 -fun get_prompt prompt src = get (set_prompt prompt src);
    3.62 -
    3.63  fun get_single src =
    3.64    (case get src of
    3.65      ([], _) => NONE
    3.66 @@ -82,16 +66,16 @@
    3.67  
    3.68  (* (map)filter *)
    3.69  
    3.70 -fun drain_map_filter f prompt src =
    3.71 +fun drain_map_filter f src =
    3.72    let
    3.73 -    val (xs, src') = get_prompt prompt src;
    3.74 +    val (xs, src') = get src;
    3.75      val xs' = map_filter f xs;
    3.76    in
    3.77      if null xs orelse not (null xs') then (xs', src')
    3.78 -    else drain_map_filter f prompt src'
    3.79 +    else drain_map_filter f src'
    3.80    end;
    3.81  
    3.82 -fun map_filter f src = make_source [] src default_prompt (drain_map_filter f);
    3.83 +fun map_filter f src = make_source [] src (drain_map_filter f);
    3.84  fun filter pred = map_filter (fn x => if pred x then SOME x else NONE);
    3.85  
    3.86  
    3.87 @@ -100,7 +84,7 @@
    3.88  
    3.89  (* list source *)
    3.90  
    3.91 -fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
    3.92 +fun of_list xs = make_source [] xs (fn xs => (xs, []));
    3.93  
    3.94  fun exhausted src = of_list (exhaust src);
    3.95  
    3.96 @@ -110,44 +94,23 @@
    3.97  val of_string = of_list o raw_explode;
    3.98  
    3.99  fun of_string_limited limit str =
   3.100 -  make_source [] (Substring.full str) default_prompt
   3.101 -    (fn _ => fn s =>
   3.102 +  make_source [] (Substring.full str)
   3.103 +    (fn s =>
   3.104        let
   3.105          val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
   3.106          val cs = map String.str (Substring.explode s1);
   3.107        in (cs, s2) end);
   3.108  
   3.109  
   3.110 -(* stream source *)
   3.111 -
   3.112 -fun slurp_input instream =
   3.113 -  let
   3.114 -    fun slurp () =
   3.115 -      (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
   3.116 -        NONE => []
   3.117 -      | SOME 0 => []
   3.118 -      | SOME _ => TextIO.input instream :: slurp ());
   3.119 -  in maps raw_explode (slurp ()) end;
   3.120 -
   3.121 -fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
   3.122 -  let val input = slurp_input in_stream in
   3.123 -    if exists (fn c => c = "\n") input then (input, ())
   3.124 -    else
   3.125 -      (case (Output.prompt prompt; TextIO.inputLine in_stream) of
   3.126 -        SOME line => (input @ raw_explode line, ())
   3.127 -      | NONE => (input, ()))
   3.128 -  end);
   3.129 -
   3.130 -
   3.131  
   3.132  (** cascade sources **)
   3.133  
   3.134  (* state-based *)
   3.135  
   3.136 -fun drain_source' stopper scan opt_recover prompt (state, src) =
   3.137 +fun drain_source' stopper scan opt_recover (state, src) =
   3.138    let
   3.139 -    val drain = Scan.drain prompt get_prompt stopper;
   3.140 -    val (xs, s) = get_prompt prompt src;
   3.141 +    val drain = Scan.drain get stopper;
   3.142 +    val (xs, s) = get src;
   3.143      val inp = ((state, xs), s);
   3.144      val ((ys, (state', xs')), src') =
   3.145        if null xs then (([], (state, [])), s)
   3.146 @@ -162,17 +125,16 @@
   3.147    in (ys, (state', unget (xs', src'))) end;
   3.148  
   3.149  fun source' init_state stopper scan recover src =
   3.150 -  make_source [] (init_state, src) default_prompt (drain_source' stopper scan recover);
   3.151 +  make_source [] (init_state, src) (drain_source' stopper scan recover);
   3.152  
   3.153  
   3.154  (* non state-based *)
   3.155  
   3.156 -fun drain_source stopper scan opt_recover prompt =
   3.157 +fun drain_source stopper scan opt_recover =
   3.158    Scan.unlift (drain_source' stopper (Scan.lift scan)
   3.159 -    (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover) prompt);
   3.160 +    (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover));
   3.161  
   3.162  fun source stopper scan recover src =
   3.163 -  make_source [] src default_prompt (drain_source stopper scan recover);
   3.164 -
   3.165 +  make_source [] src (drain_source stopper scan recover);
   3.166  
   3.167  end;
     4.1 --- a/src/Pure/General/symbol_pos.ML	Fri Oct 31 18:56:59 2014 +0100
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Oct 31 21:10:11 2014 +0100
     4.3 @@ -17,7 +17,6 @@
     4.4    val is_eof: T -> bool
     4.5    val stopper: T Scan.stopper
     4.6    val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
     4.7 -  val change_prompt: ('a -> 'b) -> 'a -> 'b
     4.8    val scan_pos: T list -> Position.T * T list
     4.9    val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list
    4.10    val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list
    4.11 @@ -88,8 +87,6 @@
    4.12        (case msg of NONE => "" | SOME m => "\n" ^ m ());
    4.13    in Scan.!! err scan end;
    4.14  
    4.15 -fun change_prompt scan = Scan.prompt "# " scan;
    4.16 -
    4.17  fun $$ s = Scan.one (fn x => symbol x = s);
    4.18  fun ~$$ s = Scan.one (fn x => symbol x <> s);
    4.19  
    4.20 @@ -120,7 +117,7 @@
    4.21    Scan.ahead ($$ q) |--
    4.22      !!! (fn () => err_prefix ^ "unclosed string literal")
    4.23        ((scan_pos --| $$$ q) --
    4.24 -        (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))));
    4.25 +        ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
    4.26  
    4.27  fun recover_strs q =
    4.28    $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
    4.29 @@ -174,7 +171,7 @@
    4.30  fun scan_cartouche err_prefix =
    4.31    Scan.ahead ($$ "\\<open>") |--
    4.32      !!! (fn () => err_prefix ^ "unclosed text cartouche")
    4.33 -      (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
    4.34 +      (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth);
    4.35  
    4.36  val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
    4.37  
    4.38 @@ -205,19 +202,17 @@
    4.39  
    4.40  val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
    4.41  
    4.42 -val scan_body = change_prompt scan_cmts;
    4.43 -
    4.44  in
    4.45  
    4.46  fun scan_comment err_prefix =
    4.47    Scan.ahead ($$ "(" -- $$ "*") |--
    4.48      !!! (fn () => err_prefix ^ "unclosed comment")
    4.49 -      ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
    4.50 +      ($$$ "(" @@@ $$$ "*" @@@ scan_cmts @@@ $$$ "*" @@@ $$$ ")");
    4.51  
    4.52  fun scan_comment_body err_prefix =
    4.53    Scan.ahead ($$ "(" -- $$ "*") |--
    4.54      !!! (fn () => err_prefix ^ "unclosed comment")
    4.55 -      ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
    4.56 +      ($$ "(" |-- $$ "*" |-- scan_cmts --| $$ "*" --| $$ ")");
    4.57  
    4.58  val recover_comment =
    4.59    $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 31 18:56:59 2014 +0100
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 31 21:10:11 2014 +0100
     5.3 @@ -35,8 +35,6 @@
     5.4    val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax ->
     5.5      Position.T -> string -> Toplevel.transition list
     5.6    val parse_spans: Token.T list -> Command_Span.span list
     5.7 -  type isar
     5.8 -  val isar: TextIO.instream -> bool -> isar
     5.9    val side_comments: Token.T list -> Token.T list
    5.10    val command_reports: outer_syntax -> Token.T -> Position.report_text list
    5.11    val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
    5.12 @@ -84,7 +82,7 @@
    5.13  fun body cmd (name, _) =
    5.14    (case cmd name of
    5.15      SOME (Command {int_only, parse, ...}) =>
    5.16 -      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    5.17 +      Parse.!!! (Parse.tags |-- parse >> pair int_only)
    5.18    | NONE =>
    5.19        Scan.succeed (false, Toplevel.imperative (fn () =>
    5.20          error ("Bad parser for outer syntax command " ^ quote name))));
    5.21 @@ -184,8 +182,6 @@
    5.22      | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
    5.23    end;
    5.24  
    5.25 -fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
    5.26 -
    5.27  fun command (spec, pos) comment parse =
    5.28    add_command spec (new_command comment NONE false parse pos);
    5.29  
    5.30 @@ -240,8 +236,7 @@
    5.31    let
    5.32      val no_terminator =
    5.33        Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
    5.34 -    fun recover int =
    5.35 -      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
    5.36 +    fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]);
    5.37    in
    5.38      src
    5.39      |> Token.source_proper
    5.40 @@ -303,24 +298,6 @@
    5.41  end;
    5.42  
    5.43  
    5.44 -(* interactive source of toplevel transformers *)
    5.45 -
    5.46 -type isar =
    5.47 -  (Toplevel.transition, (Toplevel.transition option,
    5.48 -    (Token.T, (Token.T option, (Token.T, (Token.T,
    5.49 -      (Symbol_Pos.T,
    5.50 -        Position.T * (Symbol.symbol, (Symbol.symbol, (string, unit) Source.source) Source.source)
    5.51 -  Source.source) Source.source) Source.source) Source.source)
    5.52 -  Source.source) Source.source) Source.source) Source.source;
    5.53 -
    5.54 -fun isar in_stream term : isar =
    5.55 -  Source.tty in_stream
    5.56 -  |> Symbol.source
    5.57 -  |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
    5.58 -  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
    5.59 -  |> toplevel_source term (SOME true) lookup_commands_dynamic;
    5.60 -
    5.61 -
    5.62  (* side-comments *)
    5.63  
    5.64  fun cmts (t1 :: t2 :: toks) =
     6.1 --- a/src/Pure/Isar/token.ML	Fri Oct 31 18:56:59 2014 +0100
     6.2 +++ b/src/Pure/Isar/token.ML	Fri Oct 31 21:10:11 2014 +0100
     6.3 @@ -499,8 +499,7 @@
     6.4    Scan.ahead ($$ "{" -- $$ "*") |--
     6.5      !!! "unclosed verbatim text"
     6.6        ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
     6.7 -        Symbol_Pos.change_prompt
     6.8 -          ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
     6.9 +        ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
    6.10  
    6.11  val recover_verbatim =
    6.12    $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
     7.1 --- a/src/Pure/PIDE/markup.ML	Fri Oct 31 18:56:59 2014 +0100
     7.2 +++ b/src/Pure/PIDE/markup.ML	Fri Oct 31 21:10:11 2014 +0100
     7.3 @@ -162,7 +162,6 @@
     7.4    val systemN: string
     7.5    val protocolN: string
     7.6    val legacyN: string val legacy: T
     7.7 -  val promptN: string val prompt: T
     7.8    val reportN: string val report: T
     7.9    val no_reportN: string val no_report: T
    7.10    val badN: string val bad: T
    7.11 @@ -547,7 +546,6 @@
    7.12  val protocolN = "protocol";
    7.13  
    7.14  val (legacyN, legacy) = markup_elem "legacy";
    7.15 -val (promptN, prompt) = markup_elem "prompt";
    7.16  
    7.17  val (reportN, report) = markup_elem "report";
    7.18  val (no_reportN, no_report) = markup_elem "no_report";
     8.1 --- a/src/Pure/System/isabelle_process.ML	Fri Oct 31 18:56:59 2014 +0100
     8.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Oct 31 21:10:11 2014 +0100
     8.3 @@ -126,7 +126,6 @@
     8.4        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     8.5      Output.system_message_fn := message Markup.systemN [];
     8.6      Output.protocol_message_fn := message Markup.protocolN;
     8.7 -    Output.prompt_fn := ignore;
     8.8      message Markup.initN [] [Session.welcome ()];
     8.9      msg_channel
    8.10    end;