clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
authorwenzelm
Wed, 22 Aug 2012 16:24:52 +0200
changeset 48884 963b50ec6d73
parent 48883 04cd2fddb4d9
child 48885 d5fdaf7dd1f8
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
src/Pure/System/session.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/token_markup.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 =
--- 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 =
   {
--- 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 */
 
--- 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)))