src/Tools/jEdit/src/proofdocument/session.scala
changeset 34819 86cb7f8e5a0d
parent 34818 7df68a8f0e3e
child 34820 a8ba6cde13e9
--- 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