# HG changeset patch
# User wenzelm
# Date 1330811604 -3600
# Node ID 3bbc156823dd546bc6d37111283ce12ff4c3d8c0
# Parent  69b10720104062ddb7c20ba0942cc27ffbcfa4b6# Parent  4f298836018b0d64a2df5d9a1b6d0734bad4d3d1
merged;

diff -r 69b107201040 -r 3bbc156823dd src/HOL/SPARK/Tools/fdl_parser.ML
--- a/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -325,7 +325,7 @@
 fun declarations x =
  ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
   (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
-     !!! ($$$ ";")) >> (fn ds => apply ds empty_decls)) --|
+     !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --|
   $$$ "end" --| $$$ ";") x;
 
 fun parse_declarations pos s =
@@ -371,7 +371,7 @@
 
 val rules =
   parse_all (rule >> (apfst o cons) || rule_family >> (apsnd o cons)) >>
-  (fn rls => apply (rev rls) ([], []));
+  (fn rls => fold_rev I rls ([], []));
 
 fun parse_rules pos s =
   s |>
diff -r 69b107201040 -r 3bbc156823dd src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -185,20 +185,21 @@
                         fun undo_imps thm =
                             Thm.equal_elim (Thm.symmetric rew_imp) thm
 
-                        fun add_final (arg as (thy, thm)) =
+                        fun add_final (thm, thy) =
                             if name = ""
-                            then arg |> Library.swap
+                            then (thm, thy)
                             else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
                                   Global_Theory.store_thm (Binding.name name, thm) thy)
                     in
-                        args |> apsnd (remove_alls frees)
-                             |> apsnd undo_imps
-                             |> apsnd Drule.export_without_context
-                             |> Thm.theory_attributes
+                        swap args
+                             |> apfst (remove_alls frees)
+                             |> apfst undo_imps
+                             |> apfst Drule.export_without_context
+                             |-> Thm.theory_attributes
                                 (map (Attrib.attribute thy)
                                   (@{attributes [nitpick_choice_spec]} @ atts))
                              |> add_final
-                             |> Library.swap
+                             |> swap
                     end
 
                 fun process_all [proc_arg] args =
diff -r 69b107201040 -r 3bbc156823dd src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/General/output.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -34,7 +34,7 @@
     val prompt_fn: (output -> unit) Unsynchronized.ref
     val status_fn: (output -> unit) Unsynchronized.ref
     val report_fn: (output -> unit) Unsynchronized.ref
-    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
   val error_msg': serial * string -> unit
@@ -42,7 +42,7 @@
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
-  val raw_message: Properties.T -> string -> unit
+  val protocol_message: Properties.T -> string -> unit
 end;
 
 structure Output: OUTPUT =
@@ -97,8 +97,8 @@
   val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
-  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
-    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
+  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
@@ -110,7 +110,7 @@
 fun prompt s = ! Private_Hooks.prompt_fn (output s);
 fun status s = ! Private_Hooks.status_fn (output s);
 fun report s = ! Private_Hooks.report_fn (output s);
-fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
+fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
 
 end;
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -191,8 +191,7 @@
     Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
       let
         val atts = map (attribute_i thy) srcs;
-        val (context', th') =
-          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
+        val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
       in (context', pick "" [th']) end)
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
@@ -204,8 +203,8 @@
       let
         val ths = Facts.select thmref fact;
         val atts = map (attribute_i thy) srcs;
-        val (context', ths') =
-          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
+        val (ths', context') =
+          fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
       in (context', pick name ths') end)
   end);
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -153,7 +153,7 @@
 
 fun status_message m s =
   Position.setmp_thread_data Position.none
-    (if print_mode_active keyword_statusN then Output.raw_message m else writeln) s;
+    (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
 
 fun keyword_status name =
   status_message (Isabelle_Markup.keyword_decl name)
diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/Isar/method.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -377,13 +377,12 @@
 local
 
 fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
-fun app (f, att) (context, ths) =
-  Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths);
+fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context);
 
 in
 
 fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
-  (fn (m, ths) => Scan.succeed (app m (context, ths))));
+  (fn (m, ths) => Scan.succeed (swap (app m ths context))));
 
 fun sections ss = Scan.repeat (section ss);
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -894,13 +894,12 @@
 
 in
 
-fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
+fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt =>
   let
     val name = full_name ctxt b;
     val facts = Global_Theory.name_thmss false name raw_facts;
-    fun app (th, attrs) x =
-      swap (Library.foldl_map
-        (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
+    fun app (ths, atts) =
+      fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = Global_Theory.name_thms false false name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -415,7 +415,7 @@
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
     |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
         error "Illegal schematic goal statement")
-    |> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt))))
+    |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt))
   end;
 
 in
diff -r 69b107201040 -r 3bbc156823dd src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -302,7 +302,7 @@
 val (badN, bad) = markup_elem "bad";
 
 
-(* raw message functions *)
+(* protocol message functions *)
 
 val functionN = "function"
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -229,7 +229,7 @@
   val TRACING = "tracing"
   val WARNING = "warning"
   val ERROR = "error"
-  val RAW = "raw"
+  val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
@@ -242,7 +242,7 @@
   val BAD = "bad"
 
 
-  /* raw message functions */
+  /* protocol message functions */
 
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
diff -r 69b107201040 -r 3bbc156823dd src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -57,7 +57,7 @@
         val (assignment, state1) = Document.update old_id new_id edits state;
         val _ = Future.join_tasks running;
         val _ =
-          Output.raw_message Isabelle_Markup.assign_execs
+          Output.protocol_message Isabelle_Markup.assign_execs
             ((new_id, assignment) |>
               let open XML.Encode
               in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
@@ -73,7 +73,7 @@
           YXML.parse_body versions_yxml |>
             let open XML.Decode in list int end;
         val state1 = Document.remove_versions versions state;
-        val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
+        val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml;
       in state1 end));
 
 val _ =
diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/System/invoke_scala.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -33,10 +33,10 @@
 fun promise_method name arg =
   let
     val id = new_id ();
-    fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) "";
+    fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
     val promise = Future.promise abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
-    val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg;
+    val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
   in promise end;
 
 fun method name arg = Future.join (promise_method name arg);
diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -109,7 +109,7 @@
     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 true mbox "H";
+    Output.Private_Hooks.protocol_message_fn := message true mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
     message true mbox "A" [] (Session.welcome ())
@@ -185,7 +185,7 @@
 
     val _ = Keyword.status ();
     val _ = Thy_Info.status ();
-    val _ = Output.raw_message Isabelle_Markup.ready "";
+    val _ = Output.protocol_message Isabelle_Markup.ready "";
   in loop channel end));
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -18,7 +18,7 @@
 
 object Isabelle_Process
 {
-  /* results */
+  /* messages */
 
   object Kind
   {
@@ -30,7 +30,7 @@
       ('E' : Int) -> Isabelle_Markup.TRACING,
       ('F' : Int) -> Isabelle_Markup.WARNING,
       ('G' : Int) -> Isabelle_Markup.ERROR,
-      ('H' : Int) -> Isabelle_Markup.RAW)
+      ('H' : Int) -> Isabelle_Markup.PROTOCOL)
   }
 
   sealed abstract class Message
@@ -44,7 +44,7 @@
             XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
   }
 
-  class Result(val message: XML.Elem) extends Message
+  class Output(val message: XML.Elem) extends Message
   {
     def kind: String = message.markup.name
     def properties: Properties.T = message.markup.properties
@@ -57,14 +57,14 @@
     def is_system = kind == Isabelle_Markup.SYSTEM
     def is_status = kind == Isabelle_Markup.STATUS
     def is_report = kind == Isabelle_Markup.REPORT
-    def is_raw = kind == Isabelle_Markup.RAW
+    def is_protocol = kind == Isabelle_Markup.PROTOCOL
     def is_syslog = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
-        else if (is_raw) "..."
+        else if (is_protocol) "..."
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
@@ -84,29 +84,29 @@
   import Isabelle_Process._
 
 
-  /* results */
+  /* output */
 
-  private def system_result(text: String)
+  private def system_output(text: String)
   {
-    receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
+    receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private val xml_cache = new XML.Cache()
 
-  private def put_result(kind: String, props: Properties.T, body: XML.Body)
+  private def output_message(kind: String, props: Properties.T, body: XML.Body)
   {
     if (kind == Isabelle_Markup.INIT) system_channel.accepted()
-    if (kind == Isabelle_Markup.RAW)
-      receiver(new Result(XML.Elem(Markup(kind, props), body)))
+    if (kind == Isabelle_Markup.PROTOCOL)
+      receiver(new Output(XML.Elem(Markup(kind, props), body)))
     else {
       val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
-      receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
+      receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
     }
   }
 
-  private def put_result(kind: String, text: String)
+  private def output_message(kind: String, text: String)
   {
-    put_result(kind, Nil, List(XML.Text(Symbol.decode(text))))
+    output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
   }
 
 
@@ -147,7 +147,7 @@
   private def terminate_process()
   {
     try { process.terminate }
-    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
+    catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
   }
 
   private val process_manager = Simple_Thread.fork("process_manager")
@@ -169,10 +169,10 @@
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
-    if (startup_errors != "") system_result(startup_errors)
+    if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
-      put_result(Isabelle_Markup.EXIT, "Return code: 127")
+      output_message(Isabelle_Markup.EXIT, "Return code: 127")
       process.stdin.close
       Thread.sleep(300)
       terminate_process()
@@ -182,17 +182,17 @@
       val (command_stream, message_stream) = system_channel.rendezvous()
 
       standard_input = stdin_actor()
-      val stdout = raw_output_actor(false)
-      val stderr = raw_output_actor(true)
+      val stdout = physical_output_actor(false)
+      val stderr = physical_output_actor(true)
       command_input = input_actor(command_stream)
       val message = message_actor(message_stream)
 
       val rc = process_result.join
-      system_result("process terminated")
+      system_output("process terminated")
       for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
         thread.join
-      system_result("process_manager terminated")
-      put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
+      system_output("process_manager terminated")
+      output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
     }
     system_channel.accepted()
   }
@@ -205,7 +205,7 @@
   def terminate()
   {
     close()
-    system_result("Terminating Isabelle process")
+    system_output("Terminating Isabelle process")
     terminate_process()
   }
 
@@ -213,7 +213,7 @@
 
   /** stream actors **/
 
-  /* raw stdin */
+  /* physical stdin */
 
   private def stdin_actor(): (Thread, Actor) =
   {
@@ -235,15 +235,15 @@
           //}}}
         }
       }
-      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
-      system_result(name + " terminated")
+      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+      system_output(name + " terminated")
     }
   }
 
 
-  /* raw output */
+  /* physical output */
 
-  private def raw_output_actor(err: Boolean): (Thread, Actor) =
+  private def physical_output_actor(err: Boolean): (Thread, Actor) =
   {
     val (name, reader, markup) =
       if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
@@ -263,7 +263,7 @@
             else done = true
           }
           if (result.length > 0) {
-            put_result(markup, result.toString)
+            output_message(markup, result.toString)
             result.length = 0
           }
           else {
@@ -273,8 +273,8 @@
           //}}}
         }
       }
-      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
-      system_result(name + " terminated")
+      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+      system_output(name + " terminated")
     }
   }
 
@@ -304,8 +304,8 @@
           //}}}
         }
       }
-      catch { case e: IOException => system_result(name + ": " + e.getMessage) }
-      system_result(name + " terminated")
+      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+      system_output(name + " terminated")
     }
   }
 
@@ -364,8 +364,8 @@
               case List(XML.Elem(Markup(name, props), Nil))
                   if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
                 val kind = Kind.message_markup(name(0))
-                val body = read_chunk(kind != Isabelle_Markup.RAW)
-                put_result(kind, props, body)
+                val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
+                output_message(kind, props, body)
               case _ =>
                 read_chunk(false)
                 throw new Protocol_Error("bad header: " + header.toString)
@@ -376,12 +376,12 @@
         } while (c != -1)
       }
       catch {
-        case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
-        case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
+        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
       stream.close
 
-      system_result(name + " terminated")
+      system_output(name + " terminated")
     }
   }
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/System/session.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -12,6 +12,7 @@
 import java.util.{Timer, TimerTask}
 
 import scala.collection.mutable
+import scala.collection.immutable.Queue
 import scala.actors.TIMEOUT
 import scala.actors.Actor._
 
@@ -37,7 +38,7 @@
 
 class Session(thy_load: Thy_Load = new Thy_Load)
 {
-  /* real time parameters */  // FIXME properties or settings (!?)
+  /* tuning 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)
@@ -46,6 +47,7 @@
   val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
   val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
   val prune_size = 0  // size of retained history
+  val syslog_limit = 100
 
 
   /* pervasive event buses */
@@ -54,9 +56,9 @@
   val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val phase_changed = new Event_Bus[Session.Phase]
-  val syslog_messages = new Event_Bus[Isabelle_Process.Result]
-  val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
-  val protocol_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
+  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
+  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
+  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
 
 
 
@@ -119,8 +121,8 @@
   @volatile private var syntax = Outer_Syntax.init()
   def current_syntax(): Outer_Syntax = syntax
 
-  @volatile private var reverse_syslog = List[XML.Elem]()
-  def syslog(): String = cat_lines(reverse_syslog.reverse.map(msg => XML.content(msg).mkString))
+  private val syslog = Volatile(Queue.empty[XML.Elem])
+  def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
 
   @volatile private var _phase: Session.Phase = Session.Inactive
   private def phase_=(new_phase: Session.Phase)
@@ -191,7 +193,14 @@
       def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
         buffer += msg
         msg match {
-          case result: Isabelle_Process.Result if result.is_raw => flush()
+          case output: Isabelle_Process.Output =>
+            if (output.is_syslog)
+              syslog >> (queue =>
+                {
+                  val queue1 = queue.enqueue(output.message)
+                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
+                })
+            if (output.is_protocol) flush()
           case _ =>
         }
       }
@@ -334,34 +343,34 @@
     //}}}
 
 
-    /* prover results */
+    /* prover output */
 
-    def handle_result(result: Isabelle_Process.Result)
+    def handle_output(output: Isabelle_Process.Output)
     //{{{
     {
-      def bad_result(result: Isabelle_Process.Result)
+      def bad_output(output: Isabelle_Process.Output)
       {
         if (verbose)
-          System.err.println("Ignoring prover result: " + result.message.toString)
+          System.err.println("Ignoring prover output: " + output.message.toString)
       }
 
-      result.properties match {
+      output.properties match {
 
-        case Position.Id(state_id) if !result.is_raw =>
+        case Position.Id(state_id) if !output.is_protocol =>
           try {
-            val st = global_state >>> (_.accumulate(state_id, result.message))
+            val st = global_state >>> (_.accumulate(state_id, output.message))
             delay_commands_changed.invoke(st.command)
           }
           catch {
-            case _: Document.State.Fail => bad_result(result)
+            case _: Document.State.Fail => bad_output(output)
           }
 
-        case Isabelle_Markup.Assign_Execs if result.is_raw =>
-          XML.content(result.body).mkString match {
+        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
+          XML.content(output.body).mkString match {
             case Protocol.Assign(id, assign) =>
               try { handle_assign(id, assign) }
-              catch { case _: Document.State.Fail => bad_result(result) }
-            case _ => bad_result(result)
+              catch { case _: Document.State.Fail => bad_output(output) }
+            case _ => bad_output(output)
           }
           // FIXME separate timeout event/message!?
           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
@@ -370,47 +379,44 @@
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
 
-        case Isabelle_Markup.Removed_Versions if result.is_raw =>
-          XML.content(result.body).mkString match {
+        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
+          XML.content(output.body).mkString match {
             case Protocol.Removed(removed) =>
               try { handle_removed(removed) }
-              catch { case _: Document.State.Fail => bad_result(result) }
-            case _ => bad_result(result)
+              catch { case _: Document.State.Fail => bad_output(output) }
+            case _ => bad_output(output)
           }
 
-        case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
+        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
           Future.fork {
-            val arg = XML.content(result.body).mkString
+            val arg = XML.content(output.body).mkString
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
 
-        case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
+        case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
 
-        case Isabelle_Markup.Ready if result.is_raw =>
+        case Isabelle_Markup.Ready if output.is_protocol =>
             // FIXME move to ML side (!?)
             syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
             syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
             phase = Session.Ready
 
-        case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
+        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
           thy_load.register_thy(name)
 
-        case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
+        case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
           syntax += (name, kind)
 
-        case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
+        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
           syntax += name
 
         case _ =>
-          if (result.is_syslog) {
-            reverse_syslog ::= result.message
-            if (result.is_exit && phase == Session.Startup) phase = Session.Failed
-            else if (result.is_exit) phase = Session.Inactive
-          }
-          else if (result.is_stdout) { }
-          else bad_result(result)
+          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
+          else if (output.is_exit) phase = Session.Inactive
+          else if (output.is_stdout) { }
+          else bad_output(output)
       }
     }
     //}}}
@@ -465,13 +471,13 @@
         case Messages(msgs) =>
           msgs foreach {
             case input: Isabelle_Process.Input =>
-              protocol_messages.event(input)
+              all_messages.event(input)
 
-            case result: Isabelle_Process.Result =>
-              handle_result(result)
-              if (result.is_syslog) syslog_messages.event(result)
-              if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
-              protocol_messages.event(result)
+            case output: Isabelle_Process.Output =>
+              handle_output(output)
+              if (output.is_syslog) syslog_messages.event(output)
+              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+              all_messages.event(output)
           }
 
         case change: Change_Node
diff -r 69b107201040 -r 3bbc156823dd src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -89,7 +89,8 @@
 fun get_names () = Graph.topological_order (get_thys ());
 
 fun status () =
-  List.app (fn name => Output.raw_message (Isabelle_Markup.loaded_theory name) "") (get_names ());
+  List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "")
+    (get_names ());
 
 
 (* access thy *)
diff -r 69b107201040 -r 3bbc156823dd src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/global_theory.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -80,7 +80,7 @@
 
 (* forked proofs *)
 
-fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (add_proofs thms))) thy, thms);
+fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
 
 val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
 val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
@@ -153,13 +153,12 @@
 
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
-  then swap (register_proofs (app_att (thy, thms)))
+  then app_att thms thy |-> register_proofs
   else
     let
       val naming = Sign.naming_of thy;
       val name = Name_Space.full_name naming b;
-      val (thy', thms') =
-        register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+      val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
       val thms'' = map (Thm.transfer thy') thms';
       val thy'' = thy'
         |> (Data.map o apfst)
@@ -170,19 +169,18 @@
 (* store_thm(s) *)
 
 fun store_thms (b, thms) =
-  enter_thms (name_thms true true) (name_thms false true) I (b, thms);
+  enter_thms (name_thms true true) (name_thms false true) pair (b, thms);
 
 fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
 
 fun store_thm_open (b, th) =
-  enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
+  enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single;
 
 
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((b, thms), atts) =
-  enter_thms pre_name (name_thms false true)
-    (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
+  enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
@@ -204,13 +202,14 @@
 
 (* note_thmss *)
 
-fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
+fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy =>
   let
     val name = Sign.full_name thy b;
-    fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
-    val (thms, thy') = thy |> enter_thms
-      (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
-      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
+    fun app (ths, atts) =
+      fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
+    val (thms, thy') =
+      enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app)
+        (b, facts) thy;
   in ((name, thms), thy') end);
 
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/library.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -62,7 +62,6 @@
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
   val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c
-  val apply: ('a -> 'a) list -> 'a -> 'a
   val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
   val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
   val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
@@ -229,7 +228,6 @@
   include BASIC_LIBRARY
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
-  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
 end;
 
 structure Library: LIBRARY =
@@ -334,9 +332,6 @@
 
 fun yield_singleton f x = f [x] #>> the_single;
 
-fun apply [] x = x
-  | apply (f :: fs) x = apply fs (f x);
-
 fun perhaps_apply funs arg =
   let
     fun app [] res = res
@@ -386,16 +381,6 @@
             | itr (x::l) = f(x, itr l)
       in  itr l  end;
 
-fun foldl_map f =
-  let
-    fun fold_aux (x, []) = (x, [])
-      | fold_aux (x, y :: ys) =
-          let
-            val (x', y') = f (x, y);
-            val (x'', ys') = fold_aux (x', ys);
-          in (x'', y' :: ys') end;
-  in fold_aux end;
-
 
 (* basic list functions *)
 
diff -r 69b107201040 -r 3bbc156823dd src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -73,10 +73,10 @@
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
-  val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm
+  val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
   val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
-  val theory_attributes: attribute list -> theory * thm -> theory * thm
-  val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
+  val theory_attributes: attribute list -> thm -> theory -> thm * theory
+  val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
   val tag_rule: Properties.entry -> thm -> thm
@@ -403,16 +403,16 @@
 fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
-fun apply_attribute (att: attribute) (x, th) =
+fun apply_attribute (att: attribute) th x =
   let val (x', th') = att (x, th)
-  in (the_default x x', the_default th th') end;
+  in (the_default th th', the_default x x') end;
 
-fun attribute_declaration att th x = #1 (apply_attribute att (x, th));
+fun attribute_declaration att th x = #2 (apply_attribute att th x);
 
 fun apply_attributes mk dest =
   let
-    fun app [] = I
-      | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts;
+    fun app [] th x = (th, x)
+      | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
   in app end;
 
 val theory_attributes = apply_attributes Context.Theory Context.the_theory;
diff -r 69b107201040 -r 3bbc156823dd src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Pure/simplifier.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -315,7 +315,7 @@
   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
     Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
   >> (fn atts => Thm.declaration_attribute (fn th =>
-        Library.apply (map (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)));
+        fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));
 
 end;
 
diff -r 69b107201040 -r 3bbc156823dd src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Tools/IsaPlanner/isand.ML	Sat Mar 03 22:53:24 2012 +0100
@@ -270,7 +270,7 @@
 
 (* make free vars into schematic vars with index zero *)
  fun unfix_frees frees = 
-     apply (map (K (Thm.forall_elim_var 0)) frees) 
+     fold (K (Thm.forall_elim_var 0)) frees
      o Drule.forall_intr_list frees;
 
 (* fix term and type variables *)
diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -387,7 +387,7 @@
           phase match {
             case Session.Failed =>
               Swing_Thread.now {
-                val text = new scala.swing.TextArea(Isabelle.session.syslog())
+                val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
                 text.editable = false
                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
               }
diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -31,14 +31,14 @@
         case input: Isabelle_Process.Input =>
           Swing_Thread.now { text_area.append(input.toString + "\n") }
 
-        case result: Isabelle_Process.Result =>
-          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
+        case output: Isabelle_Process.Output =>
+          Swing_Thread.now { text_area.append(output.message.toString + "\n") }
 
         case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def init() { Isabelle.session.protocol_messages += main_actor }
-  override def exit() { Isabelle.session.protocol_messages -= main_actor }
+  override def init() { Isabelle.session.all_messages += main_actor }
+  override def exit() { Isabelle.session.all_messages -= main_actor }
 }
diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -29,9 +29,9 @@
   private val main_actor = actor {
     loop {
       react {
-        case result: Isabelle_Process.Result =>
-          if (result.is_stdout || result.is_stderr)
-            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
+        case output: Isabelle_Process.Output =>
+          if (output.is_stdout || output.is_stderr)
+            Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
       }
diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 22:46:34 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 22:53:24 2012 +0100
@@ -43,7 +43,7 @@
   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   status.selection.intervalMode = ListView.IntervalMode.Single
 
-  private val syslog = new TextArea(Isabelle.session.syslog())
+  private val syslog = new TextArea(Isabelle.session.current_syslog())
 
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))
@@ -173,13 +173,11 @@
   private val main_actor = actor {
     loop {
       react {
-        case result: Isabelle_Process.Result =>
-          if (result.is_syslog)
+        case output: Isabelle_Process.Output =>
+          if (output.is_syslog)
             Swing_Thread.now {
-              val text = Isabelle.session.syslog()
-              if (text != syslog.text) {
-                syslog.text = text
-              }
+              val text = Isabelle.session.current_syslog()
+              if (text != syslog.text) syslog.text = text
             }
 
         case phase: Session.Phase =>