# HG changeset patch
# User wenzelm
# Date 1285160494 -7200
# Node ID 5b81b8df1ddeb2ebb5f56550e9a2e9811962f438
# Parent  507fcf86e1e0db32bff6f99d2afcdd9f8401fe82
Session_Dockable: basic syslog output;

diff -r 507fcf86e1e0 -r 5b81b8df1dde src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Sep 22 14:53:42 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 22 15:01:34 2010 +0200
@@ -201,7 +201,8 @@
             }
           }
           else if (result.is_exit) prover = null  // FIXME ??
-          else if (!result.is_system && !result.is_stdout) bad_result(result)
+          else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
+            bad_result(result)
         }
     }
     //}}}
@@ -229,6 +230,7 @@
     {
       receiveWithin(timeout) {
         case result: Isabelle_Process.Result if result.is_init =>
+          handle_result(result)
           while (receive {
             case result: Isabelle_Process.Result =>
               handle_result(result); !result.is_ready
@@ -236,6 +238,7 @@
           None
 
         case result: Isabelle_Process.Result if result.is_exit =>
+          handle_result(result)
           Some(startup_error())
 
         case TIMEOUT =>  // FIXME clarify
diff -r 507fcf86e1e0 -r 5b81b8df1dde src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Sep 22 14:53:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Sep 22 15:01:34 2010 +0200
@@ -17,7 +17,7 @@
 
 class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
 {
-  private val text_area = new TextArea("Isabelle session")
+  private val text_area = new TextArea
   text_area.editable = false
   set_content(new ScrollPane(text_area))
 
@@ -27,11 +27,15 @@
   private val main_actor = actor {
     loop {
       react {
+        case result: Isabelle_Process.Result =>
+          if (result.is_init || result.is_exit || result.is_system)
+            Swing_Thread.now { text_area.append(XML.content(result.message).mkString + "\n") }
+
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }
     }
   }
 
-  override def init() { }
-  override def exit() { }
+  override def init() { Isabelle.session.raw_messages += main_actor }
+  override def exit() { Isabelle.session.raw_messages -= main_actor }
 }