# HG changeset patch
# User wenzelm
# Date 1392564530 -3600
# Node ID 6d21415e390994cbc1f5eb1488b3203ff5ade5c7
# Parent  75c68e05f9eaf3d758c4794409c553d987d4fbdf
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;

diff -r 75c68e05f9ea -r 6d21415e3909 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Feb 16 15:38:08 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Feb 16 16:28:50 2014 +0100
@@ -148,9 +148,15 @@
 {
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    Swing_Thread.now { Document_Model(buffer) } match {
-      case Some(model) if model.is_theory =>
-        val snapshot = model.snapshot
+    val opt_snapshot =
+      Swing_Thread.now {
+        Document_Model(buffer) match {
+          case Some(model) if model.is_theory => Some(model.snapshot)
+          case _ => None
+        }
+      }
+    opt_snapshot match {
+      case Some(snapshot) =>
         val root = data.root
         for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
           Isabelle_Sidekick.swing_markup_tree(
@@ -172,7 +178,7 @@
               })
         }
         true
-      case _ => false
+      case None => false
     }
   }
 }