--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Dec 30 21:34:33 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Dec 30 21:57:29 2009 +0100
@@ -85,7 +85,7 @@
val start = buffer.getLineStartOffset(line)
val text = buffer.getSegment(start, caret - start)
- val completion = Isabelle.session.syntax().completion
+ val completion = Isabelle.session.current_syntax.completion
completion.complete(text) match {
case None => null
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Wed Dec 30 21:34:33 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Wed Dec 30 21:57:29 2009 +0100
@@ -147,7 +147,7 @@
while (matcher.find() && invalid_tokens != Nil) {
val kind =
- if (session.syntax().is_command(matcher.group))
+ if (session.current_syntax.is_command(matcher.group))
Token.Kind.COMMAND_START
else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
Token.Kind.COMMENT
--- a/src/Tools/jEdit/src/proofdocument/session.scala Wed Dec 30 21:34:33 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Wed Dec 30 21:57:29 2009 +0100
@@ -49,8 +49,8 @@
/* document state information -- owned by session_actor */
- @volatile private var outer_syntax = new Outer_Syntax(system.symbols)
- def syntax(): Outer_Syntax = outer_syntax
+ @volatile private var syntax = new Outer_Syntax(system.symbols)
+ def current_syntax: Outer_Syntax = syntax
@volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
@@ -120,9 +120,9 @@
elem match {
// command and keyword declarations
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
- outer_syntax += (name, kind)
+ syntax += (name, kind)
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
- outer_syntax += name
+ syntax += name
// process ready (after initialization)
case XML.Elem(Markup.READY, _, _) => prover_ready = true