# HG changeset patch
# User wenzelm
# Date 1315336272 -7200
# Node ID deb929f002b886545cbe144da0b4402a48eabc9e
# Parent  8aae881685997da2c0850ff562040d1e6bf2fd25# Parent  03a5ba7213cf4b6cd1ddee9721808d603613821c
merged

diff -r 8aae88168599 -r deb929f002b8 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/General/antiquote.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -12,7 +12,7 @@
     Open of Position.T |
     Close of Position.T
   val is_text: 'a antiquote -> bool
-  val report: ('a -> unit) -> 'a antiquote -> unit
+  val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list
   val check_nesting: 'a antiquote list -> unit
   val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
@@ -35,14 +35,14 @@
   | is_text _ = false;
 
 
-(* report *)
-
-fun report_antiq pos = Position.report pos Markup.antiq;
+(* reports *)
 
-fun report report_text (Text x) = report_text x
-  | report _ (Antiq (_, (pos, _))) = report_antiq pos
-  | report _ (Open pos) = report_antiq pos
-  | report _ (Close pos) = report_antiq pos;
+fun reports_of text =
+  maps
+    (fn Text x => text x
+      | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
+      | Open pos => [(pos, Markup.antiq)]
+      | Close pos => [(pos, Markup.antiq)]);
 
 
 (* check_nesting *)
@@ -97,7 +97,7 @@
 
 fun read (syms, pos) =
   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
-    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+    SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs)
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 end;
diff -r 8aae88168599 -r deb929f002b8 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/General/position.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -35,8 +35,9 @@
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
-  type reports = (T * Markup.T) list
-  val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
+  type report = T * Markup.T
+  val reports: report list -> unit
+  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
   val str_of: T -> string
   type range = T * T
   val no_range: range
@@ -154,10 +155,14 @@
 fun report_text pos markup txt = Output.report (reported_text pos markup txt);
 fun report pos markup = report_text pos markup "";
 
-type reports = (T * Markup.T) list;
+type report = T * Markup.T;
 
-fun reports _ [] _ _ = ()
-  | reports (r: reports Unsynchronized.ref) ps markup x =
+val reports =
+  map (fn (pos, m) => if is_reported pos then Markup.markup_only (markup pos m) else "")
+  #> implode #> Output.report;
+
+fun store_reports _ [] _ _ = ()
+  | store_reports (r: report list Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
 
diff -r 8aae88168599 -r deb929f002b8 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -258,7 +258,7 @@
   let
     val commands = lookup_commands outer_syntax;
     val range_pos = Position.set_range (Token.range toks);
-    val _ = List.app Thy_Syntax.report_token toks;
+    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
   in
     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
       [tr] =>
diff -r 8aae88168599 -r deb929f002b8 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -34,31 +34,31 @@
 
 fun report_parse_tree depth space =
   let
-    val report_text =
+    val reported_text =
       (case Context.thread_data () of
-        SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
-      | _ => Position.report_text);
+        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
+      | _ => Position.reported_text);
 
-    fun report_entity kind loc decl =
-      report_text (position_of loc)
+    fun reported_entity kind loc decl =
+      reported_text (position_of loc)
         (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
 
-    fun report loc (PolyML.PTtype types) =
-          cons (fn () =>
-            PolyML.NameSpace.displayTypeExpression (types, depth, space)
-            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-            |> report_text (position_of loc) Markup.ML_typing)
-      | report loc (PolyML.PTdeclaredAt decl) =
-          cons (fn () => report_entity Markup.ML_defN loc decl)
-      | report loc (PolyML.PTopenedAt decl) =
-          cons (fn () => report_entity Markup.ML_openN loc decl)
-      | report loc (PolyML.PTstructureAt decl) =
-          cons (fn () => report_entity Markup.ML_structN loc decl)
-      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
-      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
-      | report _ _ = I
-    and report_tree (loc, props) = fold (report loc) props;
-  in fn tree => List.app (fn e => e ()) (report_tree tree []) end;
+    fun reported loc (PolyML.PTtype types) =
+          cons
+            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
+              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+              |> reported_text (position_of loc) Markup.ML_typing)
+      | reported loc (PolyML.PTdeclaredAt decl) =
+          cons (reported_entity Markup.ML_defN loc decl)
+      | reported loc (PolyML.PTopenedAt decl) =
+          cons (reported_entity Markup.ML_openN loc decl)
+      | reported loc (PolyML.PTstructureAt decl) =
+          cons (reported_entity Markup.ML_structN loc decl)
+      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
+      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+      | reported _ _ = I
+    and reported_tree (loc, props) = fold (reported loc) props;
+  in fn tree => Output.report (implode (reported_tree tree [])) end;
 
 
 (* eval ML source tokens *)
diff -r 8aae88168599 -r deb929f002b8 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/ML/ml_lex.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -20,7 +20,6 @@
   val content_of: token -> string
   val check_content_of: token -> string
   val flatten: token list -> string
-  val report_token: token -> unit
   val keywords: string list
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
@@ -126,7 +125,7 @@
 
 in
 
-fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
+fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x);
 
 end;
 
@@ -293,7 +292,7 @@
         |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
           (SOME (false, fn msg => recover msg >> map Antiquote.Text))
         |> Source.exhaust
-        |> tap (List.app (Antiquote.report report_token))
+        |> tap (Position.reports o Antiquote.reports_of (single o report_of_token))
         |> tap Antiquote.check_nesting
         |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
       handle ERROR msg =>
diff -r 8aae88168599 -r deb929f002b8 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -44,7 +44,7 @@
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val report_token: Proof.context -> token -> unit
+  val report_of_token: token -> Position.report
   val reported_token_range: Proof.context -> token -> string
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
@@ -203,11 +203,11 @@
   | Comment     => Markup.inner_comment
   | EOF         => Markup.empty;
 
-fun report_token ctxt (Token (kind, s, (pos, _))) =
+fun report_of_token (Token (kind, s, (pos, _))) =
   let val markup =
     if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
     else token_kind_markup kind
-  in Context_Position.report ctxt pos markup end;
+  in (pos, markup) end;
 
 fun reported_token_range ctxt tok =
   if is_proper tok
diff -r 8aae88168599 -r deb929f002b8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -10,7 +10,7 @@
   val term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> term -> typ
   val decode_term: Proof.context ->
-    Position.reports * term Exn.result -> Position.reports * term Exn.result
+    Position.report list * term Exn.result -> Position.report list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
 end
@@ -126,8 +126,8 @@
 
 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   let
-    val reports = Unsynchronized.ref ([]: Position.reports);
-    fun report pos = Position.reports reports [pos];
+    val reports = Unsynchronized.ref ([]: Position.report list);
+    fun report pos = Position.store_reports reports [pos];
 
     fun trans a args =
       (case trf a of
@@ -196,7 +196,7 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
         fun get_const a =
@@ -207,7 +207,7 @@
         val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
 
         val reports = Unsynchronized.ref reports0;
-        fun report ps = Position.reports reports ps;
+        fun report ps = Position.store_reports reports ps;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
@@ -262,12 +262,10 @@
 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
 
-fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
-
 fun report_result ctxt pos results =
   (case (proper_results results, failed_results results) of
-    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
-  | ([(reports, x)], _) => (report ctxt reports; x)
+    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
+  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
   | _ => error (ambiguity_msg pos));
 
 
@@ -279,7 +277,7 @@
     val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
-    val _ = List.app (Lexicon.report_token ctxt) toks;
+    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
 
     val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
diff -r 8aae88168599 -r deb929f002b8 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -66,27 +66,29 @@
 
 fun chunk s = [string_of_int (size s), "\n", s];
 
-fun message mbox ch raw_props body =
+fun message do_flush mbox ch raw_props body =
   let
     val robust_props = map (pairself YXML.embed_controls) raw_props;
     val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
-  in Mailbox.send mbox (chunk header @ chunk body) end;
+  in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
 
 fun standard_message mbox opt_serial ch body =
   if body = "" then ()
   else
-    message mbox ch
+    message false mbox ch
       ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
         (Position.properties_of (Position.thread_data ()))) body;
 
 fun message_output mbox out_stream =
   let
+    fun flush () = ignore (try TextIO.flushOut out_stream);
     fun loop receive =
       (case receive mbox of
-        SOME msg =>
+        SOME (msg, do_flush) =>
          (List.app (fn s => TextIO.output (out_stream, s)) msg;
+          if do_flush then flush () else ();
           loop (Mailbox.receive_timeout (seconds 0.02)))
-      | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
+      | NONE => (flush (); loop (SOME o Mailbox.receive)));
   in fn () => loop (SOME o Mailbox.receive) end;
 
 in
@@ -100,7 +102,7 @@
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
 
-    val mbox = Mailbox.create () : string list Mailbox.T;
+    val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
     val _ = Simple_Thread.fork false (message_output mbox out_stream);
   in
     Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
@@ -109,10 +111,10 @@
     Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
     Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
     Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
-    Output.Private_Hooks.raw_message_fn := message mbox "H";
+    Output.Private_Hooks.raw_message_fn := message true mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
-    message mbox "A" [] (Session.welcome ());
+    message true mbox "A" [] (Session.welcome ());
     in_stream
   end;
 
diff -r 8aae88168599 -r deb929f002b8 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala	Tue Sep 06 21:11:12 2011 +0200
@@ -33,7 +33,7 @@
       ('H' : Int) -> Markup.RAW)
   }
 
-  abstract class Message
+  sealed abstract class Message
 
   class Input(name: String, args: List[String]) extends Message
   {
@@ -75,22 +75,21 @@
 }
 
 
-class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
+class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
 {
   import Isabelle_Process._
 
 
   /* demo constructor */
 
-  def this(args: String*) =
-    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
+  def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
 
 
   /* results */
 
   private def system_result(text: String)
   {
-    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
+    receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private val xml_cache = new XML.Cache()
@@ -99,10 +98,10 @@
   {
     if (kind == Markup.INIT) rm_fifos()
     if (kind == Markup.RAW)
-      receiver ! new Result(XML.Elem(Markup(kind, props), body))
+      receiver(new Result(XML.Elem(Markup(kind, props), body)))
     else {
       val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
-      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
+      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
     }
   }
 
@@ -399,7 +398,7 @@
 
   def input(name: String, args: String*): Unit =
   {
-    receiver ! new Input(name, args.toList)
+    receiver(new Input(name, args.toList))
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
   }
 
diff -r 8aae88168599 -r deb929f002b8 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/System/session.scala	Tue Sep 06 21:11:12 2011 +0200
@@ -7,8 +7,11 @@
 
 package isabelle
 
+
 import java.lang.System
+import java.util.{Timer, TimerTask}
 
+import scala.collection.mutable
 import scala.actors.TIMEOUT
 import scala.actors.Actor._
 
@@ -37,6 +40,7 @@
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
+  val message_delay = Time.seconds(0.01)  // prover messages
   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
   val update_delay = Time.seconds(0.5)  // GUI layout updates
@@ -52,7 +56,9 @@
   val assignments = new Event_Bus[Session.Assignment.type]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val phase_changed = new Event_Bus[Session.Phase]
-  val raw_messages = new Event_Bus[Isabelle_Process.Message]
+  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
+  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
+  val raw_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
 
 
 
@@ -141,15 +147,45 @@
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
+  private case class Messages(msgs: List[Isabelle_Process.Message])
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
     val this_actor = self
-    var prover: Option[Isabelle_Process with Isar_Document] = None
 
     var prune_next = System.currentTimeMillis() + prune_delay.ms
 
 
+    /* buffered prover messages */
+
+    object receiver
+    {
+      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+
+      def flush(): Unit = synchronized {
+        if (!buffer.isEmpty) {
+          val msgs = buffer.toList
+          this_actor ! Messages(msgs)
+          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+        }
+      }
+      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
+        buffer += msg
+        msg match {
+          case result: Isabelle_Process.Result if result.is_raw => flush()
+          case _ =>
+        }
+      }
+
+      private val timer = new Timer("session_actor.receiver", true)
+      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
+
+      def cancel() { timer.cancel() }
+    }
+
+    var prover: Option[Isabelle_Process with Isar_Document] = None
+
+
     /* delayed command changes */
 
     object commands_changed_delay
@@ -371,7 +407,8 @@
         case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
+            prover =
+              Some(new Isabelle_Process(timeout, receiver.invoke _, args:_*) with Isar_Document)
           }
 
         case Stop =>
@@ -383,6 +420,7 @@
             phase = Session.Inactive
           }
           finished = true
+          receiver.cancel()
           reply(())
 
         case Interrupt if prover.isDefined =>
@@ -408,12 +446,17 @@
         case change: Change_Node if prover.isDefined =>
           handle_change(change)
 
-        case input: Isabelle_Process.Input =>
-          raw_messages.event(input)
+        case Messages(msgs) =>
+          msgs foreach {
+            case input: Isabelle_Process.Input =>
+              raw_messages.event(input)
 
-        case result: Isabelle_Process.Result =>
-          handle_result(result)
-          raw_messages.event(result)
+            case result: Isabelle_Process.Result =>
+              handle_result(result)
+              if (result.is_syslog) syslog_messages.event(result)
+              if (result.is_stdout) raw_output_messages.event(result)
+              raw_messages.event(result)
+          }
 
         case bad => System.err.println("session_actor: ignoring bad message " + bad)
       }
diff -r 8aae88168599 -r deb929f002b8 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -11,7 +11,7 @@
       Source.source) Source.source) Source.source) Source.source
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
   val present_token: Token.T -> Output.output
-  val report_token: Token.T -> unit
+  val reports_of_token: Token.T -> Position.report list
   datatype span_kind = Command of string | Ignored | Malformed
   type span
   val span_kind: span -> span_kind
@@ -74,17 +74,17 @@
         else I;
     in props (token_kind_markup kind) end;
 
-fun report_symbol (sym, pos) =
-  if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
+fun reports_of_symbol (sym, pos) =
+  if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
 
 in
 
 fun present_token tok =
   Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
 
-fun report_token tok =
- (Position.report (Token.position_of tok) (token_markup tok);
-  List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
+fun reports_of_token tok =
+  (Token.position_of tok, token_markup tok) ::
+    maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok));
 
 end;
 
diff -r 8aae88168599 -r deb929f002b8 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/context_position.ML	Tue Sep 06 21:11:12 2011 +0200
@@ -14,6 +14,7 @@
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   val report: Proof.context -> Position.T -> Markup.T -> unit
+  val reports: Proof.context -> Position.report list -> unit
 end;
 
 structure Context_Position: CONTEXT_POSITION =
@@ -35,4 +36,6 @@
 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
 fun report ctxt pos markup = report_text ctxt pos markup "";
 
+fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
+
 end;
diff -r 8aae88168599 -r deb929f002b8 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 06 21:11:12 2011 +0200
@@ -29,8 +29,6 @@
   private val main_actor = actor {
     loop {
       react {
-        case input: Isabelle_Process.Input =>
-
         case result: Isabelle_Process.Result =>
           if (result.is_stdout)
             Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
@@ -40,6 +38,6 @@
     }
   }
 
-  override def init() { Isabelle.session.raw_messages += main_actor }
-  override def exit() { Isabelle.session.raw_messages -= main_actor }
+  override def init() { Isabelle.session.raw_output_messages += main_actor }
+  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
 }
diff -r 8aae88168599 -r deb929f002b8 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 21:11:12 2011 +0200
@@ -105,8 +105,6 @@
   private val main_actor = actor {
     loop {
       react {
-        case input: Isabelle_Process.Input =>
-
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {
@@ -127,13 +125,13 @@
   }
 
   override def init() {
-    Isabelle.session.raw_messages += main_actor
+    Isabelle.session.syslog_messages += main_actor
     Isabelle.session.phase_changed += main_actor
     Isabelle.session.commands_changed += main_actor
   }
 
   override def exit() {
-    Isabelle.session.raw_messages -= main_actor
+    Isabelle.session.syslog_messages -= main_actor
     Isabelle.session.phase_changed -= main_actor
     Isabelle.session.commands_changed -= main_actor
   }