# HG changeset patch # User wenzelm # Date 1236017840 -3600 # Node ID 35308320713a58b761a2915ea1d108d0d8284c54 # Parent 839d1f0b2dd1a72ffa83846ab32b2bd3ed7ab681 preliminary/failed attempt to use the new IsarDocument access model to the prover; misc tuning; diff -r 839d1f0b2dd1 -r 35308320713a src/Tools/jEdit/src/jedit/ProverSetup.scala --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Mar 02 19:17:20 2009 +0100 @@ -37,17 +37,17 @@ prover = new Prover(Isabelle.system, Isabelle.default_logic) val buffer = view.getBuffer - val dir = buffer.getDirectory + val path = buffer.getPath theory_view = new TheoryView(view.getTextArea) prover.set_document(theory_view, - if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir) + 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 839d1f0b2dd1 -r 35308320713a src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Mar 02 19:17:20 2009 +0100 @@ -242,14 +242,9 @@ override def contentInserted(buffer: JEditBuffer, - start_line: Int, offset: Int, num_lines: Int, length: Int) { } - - override def contentRemoved(buffer: JEditBuffer, - start_line: Int, offset: Int, num_lines: Int, length: Int) { } - - override def preContentInserted(buffer: JEditBuffer, - start_line: Int, offset: Int, num_lines: Int, length: Int) = + start_line: Int, offset: Int, num_lines: Int, length: Int) { +/* if (col == null) col = new Text.Changed(offset, length, 0) else if (col.start <= offset && offset <= col.start + col.added) @@ -259,11 +254,14 @@ col = new Text.Changed(offset, length, 0) } delay_commit() +*/ + changes.event(new Text.Changed(offset, length, 0)) } override def preContentRemoved(buffer: JEditBuffer, start_line: Int, start: Int, num_lines: Int, removed: Int) = { +/* if (col == null) col = new Text.Changed(start, 0, removed) else if (col.start > start + removed || start > col.start + col.added) { @@ -281,8 +279,14 @@ col = new Text.Changed(start min col.start, added, col.removed - add_removed) } delay_commit() +*/ + changes.event(new Text.Changed(start, 0, removed)) } + override def contentRemoved(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) { } + override def preContentInserted(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) { } override def bufferLoaded(buffer: JEditBuffer) { } override def foldHandlerChanged(buffer: JEditBuffer) { } override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { } diff -r 839d1f0b2dd1 -r 35308320713a src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Mar 02 19:17:20 2009 +0100 @@ -219,7 +219,8 @@ else if (after_change != null) after_change.prev = before_change } - + + System.err.println("token_changed: " + before_change + " " + after_change + " " + first_removed) token_changed(before_change, after_change, first_removed) } diff -r 839d1f0b2dd1 -r 35308320713a src/Tools/jEdit/src/proofdocument/Token.scala --- a/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Mon Mar 02 19:17:20 2009 +0100 @@ -45,7 +45,8 @@ start = bottom_clamp max (start + offset) stop = bottom_clamp max (stop + offset) } - + + override def toString: String = "[" + start + ":" + stop + "]" override def hashCode: Int = (31 + start) * 31 + stop override def equals(obj: Any): Boolean = diff -r 839d1f0b2dd1 -r 35308320713a src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Command.scala Mon Mar 02 19:17:20 2009 +0100 @@ -72,6 +72,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 @@ -85,7 +86,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 839d1f0b2dd1 -r 35308320713a src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Mar 02 19:17:20 2009 +0100 @@ -15,7 +15,7 @@ import org.gjt.sp.util.Log import isabelle.jedit.Isabelle -import isabelle.proofdocument.{ProofDocument, Text, Token} +import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token} import isabelle.IsarDocument @@ -23,12 +23,11 @@ { /* prover process */ - private var process: Isar = 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) + new IsabelleProcess(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument } def stop() { process.kill } @@ -36,10 +35,13 @@ /* 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 val document_versions = new mutable.HashSet[IsarDocument.Document_ID] + document0 + 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_id = document_id0 + private var document_versions = Set(document_id) private var initialized = false @@ -48,13 +50,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) @@ -84,10 +88,9 @@ var document: ProofDocument = null - def command_change(c: Command) = Swing.now { command_info.event(c) } - - private def handle_result(result: IsabelleProcess.Result) + private def handle_result(result: IsabelleProcess.Result): Unit = Swing.now { + def command_change(c: Command) = command_info.event(c) val (running, command) = result.props.find(p => p._1 == Markup.ID) match { case None => (false, null) @@ -98,14 +101,12 @@ } 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 { - if (document != null) { - document.activate() - activated.event(()) - } + if (document != null) { + document.activate() + activated.event(()) } } else { @@ -136,30 +137,35 @@ // 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)) } { - val cmd = commands(cmd_id) - if (cmd.state_id != null) states -= cmd.state_id - states(cmd_id) = cmd - cmd.state_id = state_id - cmd.status = Command.Status.UNPROCESSED - command_change(cmd) + if (commands.contains(cmd_id)) { + val cmd = commands(cmd_id) + if (cmd.state_id != null) states -= cmd.state_id + states(state_id) = cmd + cmd.state_id = state_id + cmd.status = Command.Status.UNPROCESSED + 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) @@ -191,32 +197,37 @@ } } - def set_document(text: Text, path: String) { - this.document = new ProofDocument(text, command_decls.contains(_)) - process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path)) - - document.structural_changes += (changes => { - for (cmd <- changes.removed_commands) remove(cmd) - for (cmd <- changes.added_commands) send(cmd) - }) + def set_document(text: Text, path: String): Unit = Swing.now + { + document = new ProofDocument(text, command_decls.contains(_)) + process.ML("()") // FIXME force initial writeln + process.begin_document(document_id0, path) + document.structural_changes += edit_document + // FIXME !? if (initialized) { document.activate() activated.event(()) } } - private def send(cmd: Command) { - cmd.status = Command.Status.UNPROCESSED - commands.put(cmd.id, cmd) + private def edit_document(changes: StructureChange) = Swing.now + { + val old_id = document_id + document_id = Isabelle.plugin.id() + document_versions += document_id - val content = isabelle_system.symbols.encode(cmd.content) - process.create_command(cmd.id, content) - process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id) - } - - def remove(cmd: Command) { - commands -= cmd.id - if (cmd.state_id != null) states -= cmd.state_id - process.remove_command(cmd.id) + val removes = + for (cmd <- changes.removed_commands) yield { + commands -= cmd.id + if (cmd.state_id != null) states -= cmd.state_id + (if (cmd.prev == null) document_id0 else cmd.prev.id) -> None + } + val inserts = + for (cmd <- changes.added_commands) yield { + commands += (cmd.id -> cmd) + process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) + (if (cmd.prev == null) document_id0 else cmd.prev.id) -> Some(cmd.id) + } + process.edit_document(old_id, document_id, removes.reverse ++ inserts) } }