# HG changeset patch # User wenzelm # Date 1260566728 -3600 # Node ID 8eccd35e975e054a346105a2084e8016f1b4b40b # Parent 91d6089cef88bb971cede4a399bc599710b5a1b5 removed unused Session.prover_logic; slightly more robust Session.start/stop; added Session.create_id (formerly in Isabelle_System); Change/Command/Proof_Document: uniform id value, not implicity creation; eliminated Proof_Document.is_command_keyword -- plain method via explicit session; diff -r 91d6089cef88 -r 8eccd35e975e src/Tools/jEdit/src/proofdocument/command.scala --- a/src/Tools/jEdit/src/proofdocument/command.scala Thu Dec 10 22:15:19 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/command.scala Fri Dec 11 22:25:28 2009 +0100 @@ -51,12 +51,12 @@ class Command( + val id: String, val tokens: List[Token], val starts: Map[Token, Int]) extends Accumulator { require(!tokens.isEmpty) - val id = Isabelle.system.id() override def hashCode = id.hashCode diff -r 91d6089cef88 -r 8eccd35e975e src/Tools/jEdit/src/proofdocument/proof_document.scala --- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Thu Dec 10 22:15:19 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Fri Dec 11 22:25:28 2009 +0100 @@ -32,44 +32,39 @@ "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" + "[()\\[\\]{}:;]", Pattern.MULTILINE) - val empty = - new Proof_Document(isabelle.jedit.Isabelle.system.id(), - Linear_Set(), Map(), Linear_Set(), Map(), _ => false) + def empty(id: String): Proof_Document = + new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map()) type StructureChange = List[(Option[Command], Option[Command])] +} -} class Proof_Document( val id: String, val tokens: Linear_Set[Token], val token_start: Map[Token, Int], val commands: Linear_Set[Command], - var states: Map[Command, Command_State], // FIXME immutable - is_command_keyword: String => Boolean) + var states: Map[Command, Command_State]) // FIXME immutable { import Proof_Document.StructureChange - def set_command_keyword(f: String => Boolean): Proof_Document = - new Proof_Document(id, tokens, token_start, commands, states, f) - def content = Token.string_from_tokens(Nil ++ tokens, token_start) /** token view **/ - def text_changed(change: Change): (Proof_Document, StructureChange) = + def text_changed(session: Session, change: Change): (Proof_Document, StructureChange) = { def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = { val (doc, chgs) = doc_chgs - val (new_doc, chg) = doc.text_edit(edit, change.id) + val (new_doc, chg) = doc.text_edit(session, edit, change.id) (new_doc, chgs ++ chg) } ((this, Nil: StructureChange) /: change.edits)(edit_doc) } - def text_edit(e: Edit, id: String): (Proof_Document, StructureChange) = + def text_edit(session: Session, e: Edit, id: String): (Proof_Document, StructureChange) = { case class TextChange(start: Int, added: String, removed: String) val change = e match { @@ -119,7 +114,7 @@ while (matcher.find() && invalid_tokens != Nil) { val kind = - if (is_command_keyword(matcher.group)) + if (session.is_command_keyword(matcher.group)) Token.Kind.COMMAND_START else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*") Token.Kind.COMMENT @@ -143,7 +138,7 @@ } val insert = new_tokens.reverse val new_token_list = begin ::: insert ::: old_suffix - token_changed(id, begin.lastOption, insert, + token_changed(session, id, begin.lastOption, insert, old_suffix.firstOption, new_token_list, start) } @@ -151,6 +146,7 @@ /** command view **/ private def token_changed( + session: Session, new_id: String, before_change: Option[Token], inserted_tokens: List[Token], @@ -192,7 +188,7 @@ case t :: ts => val (cmd, rest) = ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT) - new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest) + new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest) } } @@ -236,7 +232,7 @@ val doc = new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset, - states -- removed_commands, is_command_keyword) + states -- removed_commands) val removes = for (cmd <- removed_commands) yield (cmd_before_change -> None) diff -r 91d6089cef88 -r 8eccd35e975e src/Tools/jEdit/src/proofdocument/session.scala --- a/src/Tools/jEdit/src/proofdocument/session.scala Thu Dec 10 22:15:19 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Fri Dec 11 22:25:28 2009 +0100 @@ -12,13 +12,18 @@ class Session(system: Isabelle_System) { + /* unique ids */ + + private var id_count: BigInt = 0 + def create_id(): String = synchronized { id_count += 1; "j" + id_count } + + /* main actor */ private case class Start(logic: String) private case object Stop private var prover: Isabelle_Process with Isar_Document = null - private var prover_logic = "" private var prover_ready = false private val session_actor = actor { @@ -26,20 +31,17 @@ react { case Start(logic) => if (prover == null) { - // FIXME only once - prover = // FIXME rebust error handling (via results) - new Isabelle_Process(system, self, // FIXME improve options + prover = + new Isabelle_Process(system, self, // FIXME avoid hardwired options "-m", "xsymbols", "-m", "no_brackets", "-m", "no_type_brackets", logic) with Isar_Document - prover_logic = logic reply(()) } case Stop => if (prover != null) prover.kill - prover = null // FIXME later (via results)!? - prover_ready = false // FIXME !?? + prover_ready = false case change: Change if prover_ready => handle_change(change) @@ -86,14 +88,14 @@ @volatile private var _completion = new Completion + system.symbols def completion() = _completion + def is_command_keyword(s: String): Boolean = command_decls().contains(s) + /* document state information */ @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. - set_command_keyword((s: String) => command_decls().contains(s)) // FIXME !? + val document_0 = Proof_Document.empty(create_id()) // FIXME fresh id (!??) @volatile private var document_versions = List(document_0) def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) @@ -105,13 +107,13 @@ def begin_document(path: String) { - prover.begin_document(document_0.id, path) // FIXME fresh id!?! + prover.begin_document(document_0.id, path) // FIXME fresh document!?! } def handle_change(change: Change) { val old = document(change.parent.get.id).get - val (doc, changes) = old.text_changed(change) + val (doc, changes) = old.text_changed(this, change) document_versions ::= doc val id_changes = changes map { @@ -181,12 +183,14 @@ // process ready (after initialization) case XML.Elem(Markup.READY, _, _) => prover_ready = true - case _ => + case _ => } } case _ => } //}}} } + else if (result.kind == Isabelle_Process.Kind.EXIT) + prover = null } } diff -r 91d6089cef88 -r 8eccd35e975e src/Tools/jEdit/src/proofdocument/theory_view.scala --- a/src/Tools/jEdit/src/proofdocument/theory_view.scala Thu Dec 10 22:15:19 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala Fri Dec 11 22:25:28 2009 +0100 @@ -67,7 +67,7 @@ private val edits_delay = Swing_Thread.delay_last(300) { if (!edits.isEmpty) { - val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList) + val change = new Change(session.create_id(), Some(current_change), edits.toList) _changes ::= change session.input(change) current_change = change