--- 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)
}