--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Mar 02 19:27:06 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) {
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Mar 02 19:27:06 2009 +0100
@@ -211,14 +211,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)
@@ -228,11 +223,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) {
@@ -250,8 +248,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) { }
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Mar 02 19:27:06 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)
}
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Mon Mar 02 19:27:06 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 =
--- a/src/Tools/jEdit/src/prover/Command.scala Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Mon Mar 02 19:27:06 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
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Mar 02 19:27:06 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)
}
}