# HG changeset patch # User wenzelm # Date 1262115608 -3600 # Node ID e462572536e9d868b07d8827c96453af03d196f4 # Parent d71ecec53c61b675730c818409d79f9a310d6575 eliminated global Session.document_0 -- did not work due to hardwired id; more precise Session.begin_document, avoid race on var prover; replaced slightly odd Session.document_versions by Sassion.documents table (cf. src/Pure/Isar/isar_document.ML); simplified edit_document in ML: initial empty command is identified by ""; misc tuning; diff -r d71ecec53c61 -r e462572536e9 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Tue Dec 29 15:33:39 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Tue Dec 29 20:40:08 2009 +0100 @@ -58,8 +58,10 @@ { /* changes vs. edits */ - private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil) // FIXME !? - private var _changes = List(change_0) // owned by Swing/AWT thread + private val document_0 = session.begin_document(buffer.getName) + + private val change_0 = new Change(document_0.id, None, Nil) // FIXME !? + private var _changes = List(change_0) // owned by Swing thread def changes = _changes private var current_change = change_0 diff -r d71ecec53c61 -r e462572536e9 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Dec 29 15:33:39 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Dec 29 20:40:08 2009 +0100 @@ -262,7 +262,7 @@ /* activation */ - def activate() + private def activate() { text_area.addCaretListener(selected_state_controller) text_area.addLeftOfScrollBar(overview) @@ -271,7 +271,7 @@ session.command_change += command_change_actor } - def deactivate() + private def deactivate() { session.command_change -= command_change_actor command_change_actor !? Exit diff -r d71ecec53c61 -r e462572536e9 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 29 15:33:39 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 29 20:40:08 2009 +0100 @@ -101,13 +101,10 @@ def activate_buffer(buffer: Buffer) { + session.start(Isabelle.isabelle_args()) val model = Document_Model.init(session, buffer) for (text_area <- jedit_text_areas(buffer)) Document_View.init(model, text_area) - - session.start(Isabelle.isabelle_args()) - // FIXME theory_view.activate() - session.begin_document(buffer.getName) } def deactivate_buffer(buffer: Buffer) diff -r d71ecec53c61 -r e462572536e9 src/Tools/jEdit/src/proofdocument/proof_document.scala --- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 29 15:33:39 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 29 20:40:08 2009 +0100 @@ -30,7 +30,7 @@ "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" + "[()\\[\\]{}:;]", Pattern.MULTILINE) - def empty(id: String): Proof_Document = + def empty(id: Isar_Document.Document_ID): Proof_Document = new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map()) type StructureChange = List[(Option[Command], Option[Command])] @@ -38,11 +38,11 @@ class Proof_Document( - val id: String, + val id: Isar_Document.Document_ID, val tokens: Linear_Set[Token], // FIXME plain List, inside Command val token_start: Map[Token, Int], // FIXME eliminate val commands: Linear_Set[Command], - var states: Map[Command, Command_State]) // FIXME immutable + var states: Map[Command, Command_State]) // FIXME immutable, eliminate!? { import Proof_Document.StructureChange diff -r d71ecec53c61 -r e462572536e9 src/Tools/jEdit/src/proofdocument/session.scala --- a/src/Tools/jEdit/src/proofdocument/session.scala Tue Dec 29 15:33:39 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Tue Dec 29 20:40:08 2009 +0100 @@ -27,6 +27,7 @@ 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 @@ -48,7 +49,14 @@ if (prover != null) prover.kill prover_ready = false - + + case Begin_Document(path: String) if prover_ready => + val id = create_id() + val doc = Proof_Document.empty(id) + documents += (id -> doc) + prover.begin_document(id, path) + reply(doc) + case change: Change if prover_ready => handle_change(change) @@ -87,38 +95,35 @@ @volatile private var states = Map[Isar_Document.State_ID, Command_State]() @volatile private var commands = Map[Isar_Document.Command_ID, Command]() - val document_0 = Proof_Document.empty(create_id()) // FIXME fresh id (!??) - @volatile private var document_versions = List(document_0) + @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] = - document_versions.find(_.id == id) + def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id) /* document changes */ - def begin_document(path: String) - { - prover.begin_document(document_0.id, path) // FIXME fresh document!?! - } + 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) - document_versions ::= doc val id_changes = changes map { case (c1, c2) => - (c1.map(_.id).getOrElse(document_0.id), + (c1.map(_.id).getOrElse(""), c2 match { case None => None - case Some(command) => + 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) @@ -143,7 +148,8 @@ elem match { // document edits case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => - document_versions.find(_.id == doc_id) match { + document(doc_id) match { + case None => // FIXME clarify case Some(doc) => for { XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) @@ -158,7 +164,6 @@ case None => } } - case None => } // command and keyword declarations