# 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)))