# HG changeset patch
# User wenzelm
# Date 1345645492 -7200
# Node ID 963b50ec6d73267a2c3e8de1abe2d3d8c2dc3a98
# Parent  04cd2fddb4d98cef570d50021e38e5122fa93803
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;

diff -r 04cd2fddb4d9 -r 963b50ec6d73 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Aug 22 16:10:23 2012 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 22 16:24:52 2012 +0200
@@ -146,9 +146,6 @@
     if (version.is_init) thy_load.base_syntax
     else version.syntax
   }
-  def get_recent_syntax(): Option[Outer_Syntax] =
-    if (is_ready) Some(recent_syntax)
-    else None
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
diff -r 04cd2fddb4d9 -r 963b50ec6d73 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Aug 22 16:10:23 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Aug 22 16:24:52 2012 +0200
@@ -177,7 +177,7 @@
 
 
 class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
-  "isabelle", Isabelle.session.get_recent_syntax, Isabelle.buffer_node_name)
+  "isabelle", Isabelle.get_recent_syntax, Isabelle.buffer_node_name)
 
 
 class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
@@ -189,7 +189,7 @@
 
 
 class Isabelle_Sidekick_Raw
-  extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
+  extends Isabelle_Sidekick("isabelle-raw", Isabelle.get_recent_syntax)
 {
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
diff -r 04cd2fddb4d9 -r 963b50ec6d73 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 22 16:10:23 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 22 16:24:52 2012 +0200
@@ -40,6 +40,13 @@
   def thy_load(): JEdit_Thy_Load =
     session.thy_load.asInstanceOf[JEdit_Thy_Load]
 
+  def get_recent_syntax(): Option[Outer_Syntax] =
+  {
+    val current_session = session
+    if (current_session != null) Some(current_session.recent_syntax)
+    else None
+  }
+
 
   /* properties */
 
diff -r 04cd2fddb4d9 -r 963b50ec6d73 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Aug 22 16:10:23 2012 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Aug 22 16:24:52 2012 +0200
@@ -224,7 +224,7 @@
   /* mode provider */
 
   private val markers = Map(
-    "isabelle" -> new Token_Markup.Marker(true, Isabelle.session.get_recent_syntax()),
+    "isabelle" -> new Token_Markup.Marker(true, Isabelle.get_recent_syntax()),
     "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
     "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))