# HG changeset patch
# User wenzelm
# Date 1262206649 -3600
# Node ID 86cb7f8e5a0d209730e174554c938f7759b19ba7
# Parent  7df68a8f0e3e89f399e334200825f709e747495d
tuned signature;

diff -r 7df68a8f0e3e -r 86cb7f8e5a0d src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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
diff -r 7df68a8f0e3e -r 86cb7f8e5a0d src/Tools/jEdit/src/proofdocument/proof_document.scala
--- 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
diff -r 7df68a8f0e3e -r 86cb7f8e5a0d src/Tools/jEdit/src/proofdocument/session.scala
--- 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