merged
authorwenzelm
Tue Sep 06 21:11:12 2011 +0200 (2011-09-06)
changeset 44758deb929f002b8
parent 44757 8aae88168599
parent 44737 03a5ba7213cf
child 44759 9572b6be1aab
child 44835 ff6b9eb9c5ef
merged
     1.1 --- a/src/Pure/General/antiquote.ML	Tue Sep 06 10:30:33 2011 -0700
     1.2 +++ b/src/Pure/General/antiquote.ML	Tue Sep 06 21:11:12 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4      Open of Position.T |
     1.5      Close of Position.T
     1.6    val is_text: 'a antiquote -> bool
     1.7 -  val report: ('a -> unit) -> 'a antiquote -> unit
     1.8 +  val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list
     1.9    val check_nesting: 'a antiquote list -> unit
    1.10    val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
    1.11    val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    1.12 @@ -35,14 +35,14 @@
    1.13    | is_text _ = false;
    1.14  
    1.15  
    1.16 -(* report *)
    1.17 -
    1.18 -fun report_antiq pos = Position.report pos Markup.antiq;
    1.19 +(* reports *)
    1.20  
    1.21 -fun report report_text (Text x) = report_text x
    1.22 -  | report _ (Antiq (_, (pos, _))) = report_antiq pos
    1.23 -  | report _ (Open pos) = report_antiq pos
    1.24 -  | report _ (Close pos) = report_antiq pos;
    1.25 +fun reports_of text =
    1.26 +  maps
    1.27 +    (fn Text x => text x
    1.28 +      | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
    1.29 +      | Open pos => [(pos, Markup.antiq)]
    1.30 +      | Close pos => [(pos, Markup.antiq)]);
    1.31  
    1.32  
    1.33  (* check_nesting *)
    1.34 @@ -97,7 +97,7 @@
    1.35  
    1.36  fun read (syms, pos) =
    1.37    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
    1.38 -    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
    1.39 +    SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs)
    1.40    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    1.41  
    1.42  end;
     2.1 --- a/src/Pure/General/position.ML	Tue Sep 06 10:30:33 2011 -0700
     2.2 +++ b/src/Pure/General/position.ML	Tue Sep 06 21:11:12 2011 +0200
     2.3 @@ -35,8 +35,9 @@
     2.4    val reported_text: T -> Markup.T -> string -> string
     2.5    val report_text: T -> Markup.T -> string -> unit
     2.6    val report: T -> Markup.T -> unit
     2.7 -  type reports = (T * Markup.T) list
     2.8 -  val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
     2.9 +  type report = T * Markup.T
    2.10 +  val reports: report list -> unit
    2.11 +  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
    2.12    val str_of: T -> string
    2.13    type range = T * T
    2.14    val no_range: range
    2.15 @@ -154,10 +155,14 @@
    2.16  fun report_text pos markup txt = Output.report (reported_text pos markup txt);
    2.17  fun report pos markup = report_text pos markup "";
    2.18  
    2.19 -type reports = (T * Markup.T) list;
    2.20 +type report = T * Markup.T;
    2.21  
    2.22 -fun reports _ [] _ _ = ()
    2.23 -  | reports (r: reports Unsynchronized.ref) ps markup x =
    2.24 +val reports =
    2.25 +  map (fn (pos, m) => if is_reported pos then Markup.markup_only (markup pos m) else "")
    2.26 +  #> implode #> Output.report;
    2.27 +
    2.28 +fun store_reports _ [] _ _ = ()
    2.29 +  | store_reports (r: report list Unsynchronized.ref) ps markup x =
    2.30        let val ms = markup x
    2.31        in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
    2.32  
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 10:30:33 2011 -0700
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 21:11:12 2011 +0200
     3.3 @@ -258,7 +258,7 @@
     3.4    let
     3.5      val commands = lookup_commands outer_syntax;
     3.6      val range_pos = Position.set_range (Token.range toks);
     3.7 -    val _ = List.app Thy_Syntax.report_token toks;
     3.8 +    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
     3.9    in
    3.10      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    3.11        [tr] =>
     4.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 06 10:30:33 2011 -0700
     4.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 06 21:11:12 2011 +0200
     4.3 @@ -34,31 +34,31 @@
     4.4  
     4.5  fun report_parse_tree depth space =
     4.6    let
     4.7 -    val report_text =
     4.8 +    val reported_text =
     4.9        (case Context.thread_data () of
    4.10 -        SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
    4.11 -      | _ => Position.report_text);
    4.12 +        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
    4.13 +      | _ => Position.reported_text);
    4.14  
    4.15 -    fun report_entity kind loc decl =
    4.16 -      report_text (position_of loc)
    4.17 +    fun reported_entity kind loc decl =
    4.18 +      reported_text (position_of loc)
    4.19          (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
    4.20  
    4.21 -    fun report loc (PolyML.PTtype types) =
    4.22 -          cons (fn () =>
    4.23 -            PolyML.NameSpace.displayTypeExpression (types, depth, space)
    4.24 -            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    4.25 -            |> report_text (position_of loc) Markup.ML_typing)
    4.26 -      | report loc (PolyML.PTdeclaredAt decl) =
    4.27 -          cons (fn () => report_entity Markup.ML_defN loc decl)
    4.28 -      | report loc (PolyML.PTopenedAt decl) =
    4.29 -          cons (fn () => report_entity Markup.ML_openN loc decl)
    4.30 -      | report loc (PolyML.PTstructureAt decl) =
    4.31 -          cons (fn () => report_entity Markup.ML_structN loc decl)
    4.32 -      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
    4.33 -      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
    4.34 -      | report _ _ = I
    4.35 -    and report_tree (loc, props) = fold (report loc) props;
    4.36 -  in fn tree => List.app (fn e => e ()) (report_tree tree []) end;
    4.37 +    fun reported loc (PolyML.PTtype types) =
    4.38 +          cons
    4.39 +            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
    4.40 +              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    4.41 +              |> reported_text (position_of loc) Markup.ML_typing)
    4.42 +      | reported loc (PolyML.PTdeclaredAt decl) =
    4.43 +          cons (reported_entity Markup.ML_defN loc decl)
    4.44 +      | reported loc (PolyML.PTopenedAt decl) =
    4.45 +          cons (reported_entity Markup.ML_openN loc decl)
    4.46 +      | reported loc (PolyML.PTstructureAt decl) =
    4.47 +          cons (reported_entity Markup.ML_structN loc decl)
    4.48 +      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    4.49 +      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    4.50 +      | reported _ _ = I
    4.51 +    and reported_tree (loc, props) = fold (reported loc) props;
    4.52 +  in fn tree => Output.report (implode (reported_tree tree [])) end;
    4.53  
    4.54  
    4.55  (* eval ML source tokens *)
     5.1 --- a/src/Pure/ML/ml_lex.ML	Tue Sep 06 10:30:33 2011 -0700
     5.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Sep 06 21:11:12 2011 +0200
     5.3 @@ -20,7 +20,6 @@
     5.4    val content_of: token -> string
     5.5    val check_content_of: token -> string
     5.6    val flatten: token list -> string
     5.7 -  val report_token: token -> unit
     5.8    val keywords: string list
     5.9    val source: (Symbol.symbol, 'a) Source.source ->
    5.10      (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
    5.11 @@ -126,7 +125,7 @@
    5.12  
    5.13  in
    5.14  
    5.15 -fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
    5.16 +fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x);
    5.17  
    5.18  end;
    5.19  
    5.20 @@ -293,7 +292,7 @@
    5.21          |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    5.22            (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    5.23          |> Source.exhaust
    5.24 -        |> tap (List.app (Antiquote.report report_token))
    5.25 +        |> tap (Position.reports o Antiquote.reports_of (single o report_of_token))
    5.26          |> tap Antiquote.check_nesting
    5.27          |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
    5.28        handle ERROR msg =>
     6.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Sep 06 10:30:33 2011 -0700
     6.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 06 21:11:12 2011 +0200
     6.3 @@ -44,7 +44,7 @@
     6.4    val tvarT: typ
     6.5    val terminals: string list
     6.6    val is_terminal: string -> bool
     6.7 -  val report_token: Proof.context -> token -> unit
     6.8 +  val report_of_token: token -> Position.report
     6.9    val reported_token_range: Proof.context -> token -> string
    6.10    val matching_tokens: token * token -> bool
    6.11    val valued_token: token -> bool
    6.12 @@ -203,11 +203,11 @@
    6.13    | Comment     => Markup.inner_comment
    6.14    | EOF         => Markup.empty;
    6.15  
    6.16 -fun report_token ctxt (Token (kind, s, (pos, _))) =
    6.17 +fun report_of_token (Token (kind, s, (pos, _))) =
    6.18    let val markup =
    6.19      if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
    6.20      else token_kind_markup kind
    6.21 -  in Context_Position.report ctxt pos markup end;
    6.22 +  in (pos, markup) end;
    6.23  
    6.24  fun reported_token_range ctxt tok =
    6.25    if is_proper tok
     7.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 10:30:33 2011 -0700
     7.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 21:11:12 2011 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4    val term_sorts: term -> (indexname * sort) list
     7.5    val typ_of_term: (indexname -> sort) -> term -> typ
     7.6    val decode_term: Proof.context ->
     7.7 -    Position.reports * term Exn.result -> Position.reports * term Exn.result
     7.8 +    Position.report list * term Exn.result -> Position.report list * term Exn.result
     7.9    val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    7.10    val term_of_typ: Proof.context -> typ -> term
    7.11  end
    7.12 @@ -126,8 +126,8 @@
    7.13  
    7.14  fun parsetree_to_ast ctxt constrain_pos trf parsetree =
    7.15    let
    7.16 -    val reports = Unsynchronized.ref ([]: Position.reports);
    7.17 -    fun report pos = Position.reports reports [pos];
    7.18 +    val reports = Unsynchronized.ref ([]: Position.report list);
    7.19 +    fun report pos = Position.store_reports reports [pos];
    7.20  
    7.21      fun trans a args =
    7.22        (case trf a of
    7.23 @@ -196,7 +196,7 @@
    7.24  
    7.25  (* decode_term -- transform parse tree into raw term *)
    7.26  
    7.27 -fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
    7.28 +fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
    7.29    | decode_term ctxt (reports0, Exn.Res tm) =
    7.30        let
    7.31          fun get_const a =
    7.32 @@ -207,7 +207,7 @@
    7.33          val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
    7.34  
    7.35          val reports = Unsynchronized.ref reports0;
    7.36 -        fun report ps = Position.reports reports ps;
    7.37 +        fun report ps = Position.store_reports reports ps;
    7.38  
    7.39          fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
    7.40                (case Term_Position.decode_position typ of
    7.41 @@ -262,12 +262,10 @@
    7.42  fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
    7.43  fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
    7.44  
    7.45 -fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
    7.46 -
    7.47  fun report_result ctxt pos results =
    7.48    (case (proper_results results, failed_results results) of
    7.49 -    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
    7.50 -  | ([(reports, x)], _) => (report ctxt reports; x)
    7.51 +    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
    7.52 +  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
    7.53    | _ => error (ambiguity_msg pos));
    7.54  
    7.55  
    7.56 @@ -279,7 +277,7 @@
    7.57      val ast_tr = Syntax.parse_ast_translation syn;
    7.58  
    7.59      val toks = Syntax.tokenize syn raw syms;
    7.60 -    val _ = List.app (Lexicon.report_token ctxt) toks;
    7.61 +    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
    7.62  
    7.63      val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
    7.64        handle ERROR msg =>
     8.1 --- a/src/Pure/System/isabelle_process.ML	Tue Sep 06 10:30:33 2011 -0700
     8.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Sep 06 21:11:12 2011 +0200
     8.3 @@ -66,27 +66,29 @@
     8.4  
     8.5  fun chunk s = [string_of_int (size s), "\n", s];
     8.6  
     8.7 -fun message mbox ch raw_props body =
     8.8 +fun message do_flush mbox ch raw_props body =
     8.9    let
    8.10      val robust_props = map (pairself YXML.embed_controls) raw_props;
    8.11      val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    8.12 -  in Mailbox.send mbox (chunk header @ chunk body) end;
    8.13 +  in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
    8.14  
    8.15  fun standard_message mbox opt_serial ch body =
    8.16    if body = "" then ()
    8.17    else
    8.18 -    message mbox ch
    8.19 +    message false mbox ch
    8.20        ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    8.21          (Position.properties_of (Position.thread_data ()))) body;
    8.22  
    8.23  fun message_output mbox out_stream =
    8.24    let
    8.25 +    fun flush () = ignore (try TextIO.flushOut out_stream);
    8.26      fun loop receive =
    8.27        (case receive mbox of
    8.28 -        SOME msg =>
    8.29 +        SOME (msg, do_flush) =>
    8.30           (List.app (fn s => TextIO.output (out_stream, s)) msg;
    8.31 +          if do_flush then flush () else ();
    8.32            loop (Mailbox.receive_timeout (seconds 0.02)))
    8.33 -      | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
    8.34 +      | NONE => (flush (); loop (SOME o Mailbox.receive)));
    8.35    in fn () => loop (SOME o Mailbox.receive) end;
    8.36  
    8.37  in
    8.38 @@ -100,7 +102,7 @@
    8.39      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    8.40      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    8.41  
    8.42 -    val mbox = Mailbox.create () : string list Mailbox.T;
    8.43 +    val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
    8.44      val _ = Simple_Thread.fork false (message_output mbox out_stream);
    8.45    in
    8.46      Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    8.47 @@ -109,10 +111,10 @@
    8.48      Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
    8.49      Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    8.50      Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    8.51 -    Output.Private_Hooks.raw_message_fn := message mbox "H";
    8.52 +    Output.Private_Hooks.raw_message_fn := message true mbox "H";
    8.53      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    8.54      Output.Private_Hooks.prompt_fn := ignore;
    8.55 -    message mbox "A" [] (Session.welcome ());
    8.56 +    message true mbox "A" [] (Session.welcome ());
    8.57      in_stream
    8.58    end;
    8.59  
     9.1 --- a/src/Pure/System/isabelle_process.scala	Tue Sep 06 10:30:33 2011 -0700
     9.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Sep 06 21:11:12 2011 +0200
     9.3 @@ -33,7 +33,7 @@
     9.4        ('H' : Int) -> Markup.RAW)
     9.5    }
     9.6  
     9.7 -  abstract class Message
     9.8 +  sealed abstract class Message
     9.9  
    9.10    class Input(name: String, args: List[String]) extends Message
    9.11    {
    9.12 @@ -75,22 +75,21 @@
    9.13  }
    9.14  
    9.15  
    9.16 -class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
    9.17 +class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
    9.18  {
    9.19    import Isabelle_Process._
    9.20  
    9.21  
    9.22    /* demo constructor */
    9.23  
    9.24 -  def this(args: String*) =
    9.25 -    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
    9.26 +  def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
    9.27  
    9.28  
    9.29    /* results */
    9.30  
    9.31    private def system_result(text: String)
    9.32    {
    9.33 -    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    9.34 +    receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    9.35    }
    9.36  
    9.37    private val xml_cache = new XML.Cache()
    9.38 @@ -99,10 +98,10 @@
    9.39    {
    9.40      if (kind == Markup.INIT) rm_fifos()
    9.41      if (kind == Markup.RAW)
    9.42 -      receiver ! new Result(XML.Elem(Markup(kind, props), body))
    9.43 +      receiver(new Result(XML.Elem(Markup(kind, props), body)))
    9.44      else {
    9.45        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    9.46 -      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
    9.47 +      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
    9.48      }
    9.49    }
    9.50  
    9.51 @@ -399,7 +398,7 @@
    9.52  
    9.53    def input(name: String, args: String*): Unit =
    9.54    {
    9.55 -    receiver ! new Input(name, args.toList)
    9.56 +    receiver(new Input(name, args.toList))
    9.57      input_bytes(name, args.map(Standard_System.string_bytes): _*)
    9.58    }
    9.59  
    10.1 --- a/src/Pure/System/session.scala	Tue Sep 06 10:30:33 2011 -0700
    10.2 +++ b/src/Pure/System/session.scala	Tue Sep 06 21:11:12 2011 +0200
    10.3 @@ -7,8 +7,11 @@
    10.4  
    10.5  package isabelle
    10.6  
    10.7 +
    10.8  import java.lang.System
    10.9 +import java.util.{Timer, TimerTask}
   10.10  
   10.11 +import scala.collection.mutable
   10.12  import scala.actors.TIMEOUT
   10.13  import scala.actors.Actor._
   10.14  
   10.15 @@ -37,6 +40,7 @@
   10.16  {
   10.17    /* real time parameters */  // FIXME properties or settings (!?)
   10.18  
   10.19 +  val message_delay = Time.seconds(0.01)  // prover messages
   10.20    val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
   10.21    val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
   10.22    val update_delay = Time.seconds(0.5)  // GUI layout updates
   10.23 @@ -52,7 +56,9 @@
   10.24    val assignments = new Event_Bus[Session.Assignment.type]
   10.25    val commands_changed = new Event_Bus[Session.Commands_Changed]
   10.26    val phase_changed = new Event_Bus[Session.Phase]
   10.27 -  val raw_messages = new Event_Bus[Isabelle_Process.Message]
   10.28 +  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
   10.29 +  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
   10.30 +  val raw_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
   10.31  
   10.32  
   10.33  
   10.34 @@ -141,15 +147,45 @@
   10.35      doc_edits: List[Document.Edit_Command],
   10.36      previous: Document.Version,
   10.37      version: Document.Version)
   10.38 +  private case class Messages(msgs: List[Isabelle_Process.Message])
   10.39  
   10.40    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   10.41    {
   10.42      val this_actor = self
   10.43 -    var prover: Option[Isabelle_Process with Isar_Document] = None
   10.44  
   10.45      var prune_next = System.currentTimeMillis() + prune_delay.ms
   10.46  
   10.47  
   10.48 +    /* buffered prover messages */
   10.49 +
   10.50 +    object receiver
   10.51 +    {
   10.52 +      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   10.53 +
   10.54 +      def flush(): Unit = synchronized {
   10.55 +        if (!buffer.isEmpty) {
   10.56 +          val msgs = buffer.toList
   10.57 +          this_actor ! Messages(msgs)
   10.58 +          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   10.59 +        }
   10.60 +      }
   10.61 +      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
   10.62 +        buffer += msg
   10.63 +        msg match {
   10.64 +          case result: Isabelle_Process.Result if result.is_raw => flush()
   10.65 +          case _ =>
   10.66 +        }
   10.67 +      }
   10.68 +
   10.69 +      private val timer = new Timer("session_actor.receiver", true)
   10.70 +      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
   10.71 +
   10.72 +      def cancel() { timer.cancel() }
   10.73 +    }
   10.74 +
   10.75 +    var prover: Option[Isabelle_Process with Isar_Document] = None
   10.76 +
   10.77 +
   10.78      /* delayed command changes */
   10.79  
   10.80      object commands_changed_delay
   10.81 @@ -371,7 +407,8 @@
   10.82          case Start(timeout, args) if prover.isEmpty =>
   10.83            if (phase == Session.Inactive || phase == Session.Failed) {
   10.84              phase = Session.Startup
   10.85 -            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
   10.86 +            prover =
   10.87 +              Some(new Isabelle_Process(timeout, receiver.invoke _, args:_*) with Isar_Document)
   10.88            }
   10.89  
   10.90          case Stop =>
   10.91 @@ -383,6 +420,7 @@
   10.92              phase = Session.Inactive
   10.93            }
   10.94            finished = true
   10.95 +          receiver.cancel()
   10.96            reply(())
   10.97  
   10.98          case Interrupt if prover.isDefined =>
   10.99 @@ -408,12 +446,17 @@
  10.100          case change: Change_Node if prover.isDefined =>
  10.101            handle_change(change)
  10.102  
  10.103 -        case input: Isabelle_Process.Input =>
  10.104 -          raw_messages.event(input)
  10.105 +        case Messages(msgs) =>
  10.106 +          msgs foreach {
  10.107 +            case input: Isabelle_Process.Input =>
  10.108 +              raw_messages.event(input)
  10.109  
  10.110 -        case result: Isabelle_Process.Result =>
  10.111 -          handle_result(result)
  10.112 -          raw_messages.event(result)
  10.113 +            case result: Isabelle_Process.Result =>
  10.114 +              handle_result(result)
  10.115 +              if (result.is_syslog) syslog_messages.event(result)
  10.116 +              if (result.is_stdout) raw_output_messages.event(result)
  10.117 +              raw_messages.event(result)
  10.118 +          }
  10.119  
  10.120          case bad => System.err.println("session_actor: ignoring bad message " + bad)
  10.121        }
    11.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 10:30:33 2011 -0700
    11.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 21:11:12 2011 +0200
    11.3 @@ -11,7 +11,7 @@
    11.4        Source.source) Source.source) Source.source) Source.source
    11.5    val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
    11.6    val present_token: Token.T -> Output.output
    11.7 -  val report_token: Token.T -> unit
    11.8 +  val reports_of_token: Token.T -> Position.report list
    11.9    datatype span_kind = Command of string | Ignored | Malformed
   11.10    type span
   11.11    val span_kind: span -> span_kind
   11.12 @@ -74,17 +74,17 @@
   11.13          else I;
   11.14      in props (token_kind_markup kind) end;
   11.15  
   11.16 -fun report_symbol (sym, pos) =
   11.17 -  if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
   11.18 +fun reports_of_symbol (sym, pos) =
   11.19 +  if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
   11.20  
   11.21  in
   11.22  
   11.23  fun present_token tok =
   11.24    Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
   11.25  
   11.26 -fun report_token tok =
   11.27 - (Position.report (Token.position_of tok) (token_markup tok);
   11.28 -  List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
   11.29 +fun reports_of_token tok =
   11.30 +  (Token.position_of tok, token_markup tok) ::
   11.31 +    maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok));
   11.32  
   11.33  end;
   11.34  
    12.1 --- a/src/Pure/context_position.ML	Tue Sep 06 10:30:33 2011 -0700
    12.2 +++ b/src/Pure/context_position.ML	Tue Sep 06 21:11:12 2011 +0200
    12.3 @@ -14,6 +14,7 @@
    12.4    val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
    12.5    val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
    12.6    val report: Proof.context -> Position.T -> Markup.T -> unit
    12.7 +  val reports: Proof.context -> Position.report list -> unit
    12.8  end;
    12.9  
   12.10  structure Context_Position: CONTEXT_POSITION =
   12.11 @@ -35,4 +36,6 @@
   12.12  fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
   12.13  fun report ctxt pos markup = report_text ctxt pos markup "";
   12.14  
   12.15 +fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
   12.16 +
   12.17  end;
    13.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 10:30:33 2011 -0700
    13.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 21:11:12 2011 +0200
    13.3 @@ -29,8 +29,6 @@
    13.4    private val main_actor = actor {
    13.5      loop {
    13.6        react {
    13.7 -        case input: Isabelle_Process.Input =>
    13.8 -
    13.9          case result: Isabelle_Process.Result =>
   13.10            if (result.is_stdout)
   13.11              Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
   13.12 @@ -40,6 +38,6 @@
   13.13      }
   13.14    }
   13.15  
   13.16 -  override def init() { Isabelle.session.raw_messages += main_actor }
   13.17 -  override def exit() { Isabelle.session.raw_messages -= main_actor }
   13.18 +  override def init() { Isabelle.session.raw_output_messages += main_actor }
   13.19 +  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
   13.20  }
    14.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 10:30:33 2011 -0700
    14.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 21:11:12 2011 +0200
    14.3 @@ -105,8 +105,6 @@
    14.4    private val main_actor = actor {
    14.5      loop {
    14.6        react {
    14.7 -        case input: Isabelle_Process.Input =>
    14.8 -
    14.9          case result: Isabelle_Process.Result =>
   14.10            if (result.is_syslog)
   14.11              Swing_Thread.now {
   14.12 @@ -127,13 +125,13 @@
   14.13    }
   14.14  
   14.15    override def init() {
   14.16 -    Isabelle.session.raw_messages += main_actor
   14.17 +    Isabelle.session.syslog_messages += main_actor
   14.18      Isabelle.session.phase_changed += main_actor
   14.19      Isabelle.session.commands_changed += main_actor
   14.20    }
   14.21  
   14.22    override def exit() {
   14.23 -    Isabelle.session.raw_messages -= main_actor
   14.24 +    Isabelle.session.syslog_messages -= main_actor
   14.25      Isabelle.session.phase_changed -= main_actor
   14.26      Isabelle.session.commands_changed -= main_actor
   14.27    }