# HG changeset patch
# User wenzelm
# Date 1289917741 -3600
# Node ID 36d4f2757f4fcfdc642731ed282e3adb1b8ee9ec
# Parent  40cefa372680aaaf05d7e928b8049d0b5e7f12d4
post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);

diff -r 40cefa372680 -r 36d4f2757f4f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Nov 16 15:23:26 2010 +0100
+++ b/src/Pure/System/session.scala	Tue Nov 16 15:29:01 2010 +0100
@@ -196,8 +196,6 @@
     def handle_result(result: Isabelle_Process.Result)
     //{{{
     {
-      raw_messages.event(result)
-
       result.properties match {
         case Position.Id(state_id) =>
           try {
@@ -234,6 +232,8 @@
           }
           else bad_result(result)
         }
+
+      raw_messages.event(result)
     }
     //}}}