# HG changeset patch # User wenzelm # Date 1262118677 -3600 # Node ID 0fed930f29927de30037ce3bc1dfca79c13632cf # Parent e462572536e9d868b07d8827c96453af03d196f4 misc tuning; diff -r e462572536e9 -r 0fed930f2992 src/Tools/jEdit/src/proofdocument/session.scala --- a/src/Tools/jEdit/src/proofdocument/session.scala Tue Dec 29 20:40:08 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Tue Dec 29 21:31:17 2009 +0100 @@ -17,26 +17,132 @@ class Session(system: Isabelle_System) { + /* pervasive event buses */ + + val global_settings = new Event_Bus[Session.Global_Settings.type] + val raw_results = new Event_Bus[Isabelle_Process.Result] + val results = new Event_Bus[Command] + + val command_change = new Event_Bus[Command] + val document_change = new Event_Bus[Proof_Document] + + /* unique ids */ private var id_count: BigInt = 0 def create_id(): String = synchronized { id_count += 1; "j" + id_count } - /* main actor */ + /* document state information -- vars belong to session_actor */ + + @volatile private var outer_syntax = new Outer_Syntax(system.symbols) + def syntax(): Outer_Syntax = outer_syntax + + @volatile private var states = Map[Isar_Document.State_ID, Command_State]() + @volatile private var commands = Map[Isar_Document.Command_ID, Command]() + @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]() + + def state(id: Isar_Document.State_ID): Option[Command_State] = states.get(id) + def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) + def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id) + + + /** main actor **/ private case class Start(args: List[String]) private case object Stop private case class Begin_Document(path: String) - @volatile private var _syntax = new Outer_Syntax(system.symbols) - def syntax(): Outer_Syntax = _syntax + private val session_actor = actor { + + var prover: Isabelle_Process with Isar_Document = null + var prover_ready = false + + + /* document changes */ + + def handle_change(change: Change) + { + val old = document(change.parent.get.id).get + val (doc, changes) = old.text_changed(this, change) + + val id_changes = changes map { + case (c1, c2) => + (c1.map(_.id).getOrElse(""), + c2 match { + case None => None + case Some(command) => // FIXME clarify -- may reuse existing commands!?? + commands += (command.id -> command) + prover.define_command(command.id, system.symbols.encode(command.content)) + Some(command.id) + }) + } + documents += (doc.id -> doc) + prover.edit_document(old.id, doc.id, id_changes) + + document_change.event(doc) + } + + + /* prover results */ + + def handle_result(result: Isabelle_Process.Result) + { + raw_results.event(result) - private var prover: Isabelle_Process with Isar_Document = null - private var prover_ready = false + val state = + Position.id_of(result.props) match { + case None => None + case Some(id) => commands.get(id) orElse states.get(id) orElse None + } + if (state.isDefined) state.get ! (this, result.message) + else if (result.kind == Isabelle_Process.Kind.STATUS) { + //{{{ global status message + for (elem <- result.body) { + elem match { + // document edits + case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => + document(doc_id) match { + case None => // FIXME clarify + case Some(doc) => + for { + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) + <- edits } + { + commands.get(cmd_id) match { + case Some(cmd) => + val state = new Command_State(cmd) + states += (state_id -> state) + doc.states += (cmd -> state) + command_change.event(cmd) // FIXME really!? + case None => + } + } + } - private val session_actor = actor { + // command and keyword declarations + case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => + outer_syntax += (name, kind) + case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => + outer_syntax += name + + // process ready (after initialization) + case XML.Elem(Markup.READY, _, _) => prover_ready = true + + case _ => + } + } + //}}} + } + else if (result.kind == Isabelle_Process.Kind.EXIT) + prover = null + } + val xml_cache = new XML.Cache(131071) + + + /* main loop */ + loop { react { case Start(args) => @@ -56,7 +162,7 @@ documents += (id -> doc) prover.begin_document(id, path) reply(doc) - + case change: Change if prover_ready => handle_change(change) @@ -69,118 +175,20 @@ } } + + /* main methods */ + def start(args: List[String]) { session_actor !? Start(args) } def stop() { session_actor ! Stop } def input(change: Change) { session_actor ! change } - - /* pervasive event buses */ - - val global_settings = new Event_Bus[Session.Global_Settings.type] - val raw_results = new Event_Bus[Isabelle_Process.Result] - val results = new Event_Bus[Command] - - val command_change = new Event_Bus[Command] - val document_change = new Event_Bus[Proof_Document] - - - /* selected state */ // FIXME!? races!? - - private var _selected_state: Command = null - def selected_state = _selected_state - def selected_state_=(state: Command) { _selected_state = state; results.event(state) } - - - /* document state information */ - - @volatile private var states = Map[Isar_Document.State_ID, Command_State]() - @volatile private var commands = Map[Isar_Document.Command_ID, Command]() - @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]() - - def state(id: Isar_Document.State_ID): Option[Command_State] = states.get(id) - def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) - def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id) - - - /* document changes */ - def begin_document(path: String): Proof_Document = (session_actor !? Begin_Document(path)).asInstanceOf[Proof_Document] - private def handle_change(change: Change) - { - val old = document(change.parent.get.id).get - val (doc, changes) = old.text_changed(this, change) - val id_changes = changes map { - case (c1, c2) => - (c1.map(_.id).getOrElse(""), - c2 match { - case None => None - case Some(command) => // FIXME clarify -- may reuse existing commands!?? - commands += (command.id -> command) - prover.define_command(command.id, system.symbols.encode(command.content)) - Some(command.id) - }) - } - documents += (doc.id -> doc) - prover.edit_document(old.id, doc.id, id_changes) - - document_change.event(doc) - } - - - /* prover results */ - - private def handle_result(result: Isabelle_Process.Result) - { - raw_results.event(result) + /* selected state */ // FIXME eliminate!?! - val state = - Position.id_of(result.props) match { - case None => None - case Some(id) => commands.get(id) orElse states.get(id) orElse None - } - if (state.isDefined) state.get ! (this, result.message) - else if (result.kind == Isabelle_Process.Kind.STATUS) { - //{{{ global status message - for (elem <- result.body) { - elem match { - // document edits - case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => - document(doc_id) match { - case None => // FIXME clarify - case Some(doc) => - for { - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) - <- edits } - { - commands.get(cmd_id) match { - case Some(cmd) => - val state = new Command_State(cmd) - states += (state_id -> state) - doc.states += (cmd -> state) - command_change.event(cmd) // FIXME really!? - case None => - } - } - } - - // command and keyword declarations - case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => - _syntax += (name, kind) - case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => - _syntax += name - - // process ready (after initialization) - case XML.Elem(Markup.READY, _, _) => prover_ready = true - - case _ => - } - } - //}}} - } - else if (result.kind == Isabelle_Process.Kind.EXIT) - prover = null - } + private var _selected_state: Command = null + def selected_state = _selected_state + def selected_state_=(state: Command) { _selected_state = state; results.event(state) } }