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);
--- 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)
}
//}}}