src/Tools/jEdit/src/proofdocument/session.scala
changeset 34851 304a86164dd2
parent 34848 77ac13833972
child 34853 32b49207ca20
equal deleted inserted replaced
34850:fdd560e80264 34851:304a86164dd2
    28     def consume(session: Session, message: XML.Tree): Unit
    28     def consume(session: Session, message: XML.Tree): Unit
    29   }
    29   }
    30 }
    30 }
    31 
    31 
    32 
    32 
    33 class Session(val isabelle_system: Isabelle_System)
    33 class Session(system: Isabelle_System)
    34 {
    34 {
    35   /* pervasive event buses */
    35   /* pervasive event buses */
    36 
    36 
    37   val global_settings = new Event_Bus[Session.Global_Settings.type]
    37   val global_settings = new Event_Bus[Session.Global_Settings.type]
    38   val raw_results = new Event_Bus[Isabelle_Process.Result]
    38   val raw_results = new Event_Bus[Isabelle_Process.Result]
    48 
    48 
    49 
    49 
    50 
    50 
    51   /** main actor **/
    51   /** main actor **/
    52 
    52 
    53   @volatile private var syntax = new Outer_Syntax(isabelle_system.symbols)
    53   @volatile private var syntax = new Outer_Syntax(system.symbols)
    54   def current_syntax: Outer_Syntax = syntax
    54   def current_syntax: Outer_Syntax = syntax
    55 
    55 
    56   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    56   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    57   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    57   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    58   def lookup_command(id: Session.Entity_ID): Option[Command] =
    58   def lookup_command(id: Session.Entity_ID): Option[Command] =
    88            c2 match {
    88            c2 match {
    89               case None => None
    89               case None => None
    90               case Some(command) =>
    90               case Some(command) =>
    91                 if (!lookup_command(command.id).isDefined) {
    91                 if (!lookup_command(command.id).isDefined) {
    92                   register(command)
    92                   register(command)
    93                   prover.define_command(command.id, isabelle_system.symbols.encode(command.content))
    93                   prover.define_command(command.id, system.symbols.encode(command.content))
    94                 }
    94                 }
    95                 Some(command.id)
    95                 Some(command.id)
    96             })
    96             })
    97       }
    97       }
    98       register_document(doc)
    98       register_document(doc)
   201 
   201 
   202     loop {
   202     loop {
   203       react {
   203       react {
   204         case Start(timeout, args) =>
   204         case Start(timeout, args) =>
   205           if (prover == null) {
   205           if (prover == null) {
   206             prover = new Isabelle_Process(isabelle_system, self, args:_*) with Isar_Document
   206             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   207             val origin = sender
   207             val origin = sender
   208             val opt_err = prover_startup(timeout)
   208             val opt_err = prover_startup(timeout)
   209             if (opt_err.isDefined) prover = null
   209             if (opt_err.isDefined) prover = null
   210             origin ! opt_err
   210             origin ! opt_err
   211           }
   211           }