src/Tools/jEdit/src/proofdocument/session.scala
changeset 34819 86cb7f8e5a0d
parent 34818 7df68a8f0e3e
child 34820 a8ba6cde13e9
equal deleted inserted replaced
34818:7df68a8f0e3e 34819:86cb7f8e5a0d
    47   def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
    47   def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
    48 
    48 
    49 
    49 
    50   /* document state information -- owned by session_actor */
    50   /* document state information -- owned by session_actor */
    51 
    51 
    52   @volatile private var outer_syntax = new Outer_Syntax(system.symbols)
    52   @volatile private var syntax = new Outer_Syntax(system.symbols)
    53   def syntax(): Outer_Syntax = outer_syntax
    53   def current_syntax: Outer_Syntax = syntax
    54 
    54 
    55   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    55   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    56   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    56   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    57 
    57 
    58   // FIXME eliminate
    58   // FIXME eliminate
   118         // global status message
   118         // global status message
   119         for (elem <- result.body) {
   119         for (elem <- result.body) {
   120           elem match {
   120           elem match {
   121             // command and keyword declarations
   121             // command and keyword declarations
   122             case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
   122             case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
   123               outer_syntax += (name, kind)
   123               syntax += (name, kind)
   124             case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
   124             case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
   125               outer_syntax += name
   125               syntax += name
   126 
   126 
   127             // process ready (after initialization)
   127             // process ready (after initialization)
   128             case XML.Elem(Markup.READY, _, _) => prover_ready = true
   128             case XML.Elem(Markup.READY, _, _) => prover_ready = true
   129 
   129 
   130           case _ =>
   130           case _ =>