# HG changeset patch # User immler@in.tum.de # Date 1237477709 -3600 # Node ID 5d88e0681d443909a7ae348c9c2dc30f27381a19 # Parent 20bfcca24658d1e81cf2dae00899bad93699a88e# Parent b06946a1d4cbd0aafbe1c6f5100cb68d814ad0f4 merged; resolved conflicts (kept own versions) diff -r 20bfcca24658 -r 5d88e0681d44 src/Tools/jEdit/src/jedit/ProverSetup.scala --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Mar 19 16:18:57 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Mar 19 16:48:29 2009 +0100 @@ -40,13 +40,13 @@ theory_view = new TheoryView(view.getTextArea, prover) prover.set_document(theory_view.change_receiver, - if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) + if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) theory_view.activate //register output-view prover.output_info += (text => { - output_text_view.append(text) + output_text_view.append(text + "\n") val dockable = view.getDockableWindowManager.getDockable("isabelle-output") //link process output if dockable is active if (dockable != null) { diff -r 20bfcca24658 -r 5d88e0681d44 src/Tools/jEdit/src/jedit/TheoryView.scala diff -r 20bfcca24658 -r 5d88e0681d44 src/Tools/jEdit/src/proofdocument/ProofDocument.scala diff -r 20bfcca24658 -r 5d88e0681d44 src/Tools/jEdit/src/proofdocument/Token.scala --- a/src/Tools/jEdit/src/proofdocument/Token.scala Thu Mar 19 16:18:57 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Thu Mar 19 16:48:29 2009 +0100 @@ -42,5 +42,6 @@ val length = content.length val stop = start + length override def toString = content + "(" + kind + ")" + override def hashCode: Int = (31 + start) * 31 + stop def shift(i: Int) = new Token(start + i, content, kind) } diff -r 20bfcca24658 -r 5d88e0681d44 src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Thu Mar 19 16:18:57 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Command.scala Thu Mar 19 16:48:29 2009 +0100 @@ -51,6 +51,7 @@ def status = _status def status_=(st: Command.Status.Value) { if (st == Command.Status.UNPROCESSED) { + state_results.clear // delete markup for (child <- root_node.children) { child.children = Nil @@ -64,7 +65,7 @@ private val results = new mutable.ListBuffer[XML.Tree] private val state_results = new mutable.ListBuffer[XML.Tree] - def add_result(running: Boolean, tree: XML.Tree) { + def add_result(running: Boolean, tree: XML.Tree) = synchronized { (if (running) state_results else results) += tree } diff -r 20bfcca24658 -r 5d88e0681d44 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 19 16:18:57 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 19 16:48:29 2009 +0100 @@ -31,12 +31,12 @@ { /* prover process */ - private var process: Isar with IsarDocument= null + private val process = { val results = new EventBus[IsabelleProcess.Result] + handle_result results.logger = Log.log(Log.ERROR, null, _) - process = new Isar(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument + new IsabelleProcess(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument } def stop() { process.kill } @@ -44,12 +44,14 @@ /* document state information */ - private val states = new mutable.HashMap[IsarDocument.State_ID, Command] - private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] - private val document0 = Isabelle.plugin.id() - private var document_versions = List((document0, ProofDocument.empty)) + private val states = new mutable.HashMap[IsarDocument.State_ID, Command] with + mutable.SynchronizedMap[IsarDocument.State_ID, Command] + private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with + mutable.SynchronizedMap[IsarDocument.Command_ID, Command] + private val document_id0 = Isabelle.plugin.id() + private var document_versions = List((document_id0, ProofDocument.empty)) - def get_id = document_versions.head._1 + def document_id = document_versions.head._1 def document = document_versions.head._2 private var initialized = false @@ -59,13 +61,15 @@ val decl_info = new EventBus[(String, String)] - private val keyword_decls = new mutable.HashSet[String] { + private val keyword_decls = + new mutable.HashSet[String] with mutable.SynchronizedSet[String] { override def +=(name: String) = { decl_info.event(name, OuterKeyword.MINOR) super.+=(name) } } - private val command_decls = new mutable.HashMap[String, String] { + private val command_decls = + new mutable.HashMap[String, String] with mutable.SynchronizedMap[String, String] { override def +=(entry: (String, String)) = { decl_info.event(entry) super.+=(entry) @@ -93,10 +97,9 @@ val output_info = new EventBus[String] var change_receiver = null: Actor - def command_change(c: Command) = this ! c - private def handle_result(result: IsabelleProcess.Result) { + def command_change(c: Command) = this ! c val (running, command) = result.props.find(p => p._1 == Markup.ID) match { case None => (false, null) @@ -107,7 +110,7 @@ } if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN) - Swing.now { output_info.event(result.result) } + output_info.event(result.toString) else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !? initialized = true Swing.now { this ! ProverEvents.Activate } @@ -143,11 +146,12 @@ // document edits case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) if document_versions.contains(doc_id) => + output_info.event(result.toString) for { XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits - if (commands.contains(cmd_id)) } { + if (commands.contains(cmd_id)) { val cmd = commands(cmd_id) if (cmd.state_id != null) states -= cmd.state_id states(cmd_id) = cmd @@ -156,17 +160,21 @@ command_change(cmd) } + } // command status case XML.Elem(Markup.UNPROCESSED, _, _) if command != null => + output_info.event(result.toString) command.status = Command.Status.UNPROCESSED command_change(command) case XML.Elem(Markup.FINISHED, _, _) if command != null => + output_info.event(result.toString) command.status = Command.Status.FINISHED command_change(command) case XML.Elem(Markup.FAILED, _, _) if command != null => + output_info.event(result.toString) command.status = Command.Status.FAILED command_change(command) @@ -205,20 +213,20 @@ react { case Activate => { val (doc, structure_change) = document.activate - val old_id = get_id + val old_id = document_id val doc_id = Isabelle.plugin.id() document_versions ::= (doc_id, doc) edit_document(old_id, doc_id, structure_change) } case SetIsCommandKeyword(f) => { - val old_id = get_id + val old_id = document_id val doc_id = Isabelle.plugin.id() document_versions ::= (doc_id, document.set_command_keyword(f)) edit_document(old_id, doc_id, StructureChange(None, Nil, Nil)) } case change: Text.Change => { val (doc, structure_change) = document.text_changed(change) - val old_id = get_id + val old_id = document_id val doc_id = Isabelle.plugin.id() document_versions ::= (doc_id, doc) edit_document(old_id, doc_id, structure_change) @@ -235,7 +243,7 @@ this.change_receiver = change_receiver this ! ProverEvents.SetIsCommandKeyword(command_decls.contains) process.ML("()") // FIXME force initial writeln - process.begin_document(document0, path) + process.begin_document(document_id0, path) } private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now @@ -244,13 +252,13 @@ for (cmd <- changes.removed_commands) yield { commands -= cmd.id if (cmd.state_id != null) states -= cmd.state_id - (document.commands.prev(cmd).map(_.id).getOrElse(document0)) -> None + (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None } val inserts = for (cmd <- changes.added_commands) yield { commands += (cmd.id -> cmd) process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) - (document.commands.prev(cmd).map(_.id).getOrElse(document0)) -> Some(cmd.id) + (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id) } process.edit_document(old_id, document_id, removes.reverse ++ inserts) }