clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
--- 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)))