recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
--- 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
}
}
}