--- a/src/Tools/jEdit/src/prover/Prover.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,204 +1,168 @@
+/*
+ * Higher-level prover communication
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
package isabelle.prover
-import scala.collection.mutable.{ HashMap, HashSet }
import java.util.Properties
-import javax.swing.SwingUtilities
+import scala.collection.mutable.{HashMap, HashSet}
-import isabelle.proofdocument.{ ProofDocument, Text, Token }
-import isabelle.IsabelleProcess.Result
-import isabelle.YXML.parse_failsafe
-import isabelle.XML.{ Elem, Tree }
-import isabelle.Symbol.Interpretation
-import isabelle.IsabelleSyntax.{ encode_properties, encode_string }
+import org.gjt.sp.util.Log
+
+import isabelle.proofdocument.{ProofDocument, Text, Token}
+
-import isabelle.utils.EventSource
-
-import Command.Phase
+class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation)
+{
+ private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
+ private var process: Isar = null
+ private var commands = new HashMap[String, Command]
-class Prover() {
- val converter = new Interpretation()
-
- private var _logic = "HOL"
- private var process = null : IsabelleProcess
- private var commands = new HashMap[String, Command]
-
val command_decls = new HashSet[String]
val keyword_decls = new HashSet[String]
private var initialized = false
-
- val activated = new EventSource[Unit]
- val commandInfo = new EventSource[CommandChangeInfo]
- val outputInfo = new EventSource[String]
- val allInfo = new EventSource[Result]
- var document = null : Document
+
+ val activated = new EventBus[Unit]
+ val command_info = new EventBus[Command]
+ val output_info = new EventBus[String]
+ var document: Document = null
- def fireChange(c : Command) =
- inUIThread(() => commandInfo.fire(new CommandChangeInfo(c)))
+
+ def command_change(c: Command) = Swing.now { command_info.event(c) }
+
+ private def handle_result(r: IsabelleProcess.Result) = {
+ val id = if (r.props != null) r.props.getProperty(Markup.ID) else null
+ val st = if (id != null) commands.getOrElse(id, null) else null
- val worker_thread = new Thread("isabelle.Prover: worker") {
- override def run() : Unit = {
- while (true) {
- val r = process.get_result
-
- val id = if (r.props != null) r.props.getProperty("id") else null
- val st = if (id != null) commands.getOrElse(id, null) else null
-
- if (r.kind == IsabelleProcess.Kind.EXIT)
- return
- else if (r.kind == IsabelleProcess.Kind.STDOUT
- || r.kind == IsabelleProcess.Kind.STDIN)
- inUIThread(() => outputInfo.fire(r.result))
- else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
- initialized = true
- inUIThread(() =>
- if (document != null) {
- document.activate()
- activated.fire(())
- }
- )
+ if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
+ Swing.now { output_info.event(r.result) }
+ else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
+ initialized = true
+ Swing.now {
+ if (document != null) {
+ document.activate()
+ activated.event(())
}
- else {
- val tree = parse_failsafe(converter.decode(r.result))
- if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE))
- tree match {
- //handle all kinds of status messages here
- case Elem("message", List(("class","status")), elems) =>
- elems map (elem => elem match{
+ }
+ }
+ else {
+ val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
+ if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
+ r.kind match {
- // catch command_start and keyword declarations
- case Elem("command_decl", List(("name", name), ("kind", _)), _) =>
- command_decls.addEntry(name)
- case Elem("keyword_decl", List(("name", name)), _) =>
- keyword_decls.addEntry(name)
+ case IsabelleProcess.Kind.STATUS =>
+ //{{{ handle all kinds of status messages here
+ tree match {
+ case XML.Elem(Markup.MESSAGE, _, elems) =>
+ for (elem <- elems) {
+ elem match {
+ //{{{
+ // command status
+ case XML.Elem(Markup.FINISHED, _, _) =>
+ st.status = Command.Status.FINISHED
+ command_change(st)
+ case XML.Elem(Markup.UNPROCESSED, _, _) =>
+ st.status = Command.Status.UNPROCESSED
+ command_change(st)
+ case XML.Elem(Markup.FAILED, _, _) =>
+ st.status = Command.Status.FAILED
+ command_change(st)
+ case XML.Elem(Markup.DISPOSED, _, _) =>
+ document.prover.commands.removeKey(st.id)
+ st.status = Command.Status.REMOVED
+ command_change(st)
- // expecting markups here
- case Elem(kind, List(("offset", offset),
- ("end_offset", end_offset),
- ("id", id)), List()) =>
- val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
- val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
-
- val command =
- // outer syntax: no id in props
- if(st == null) commands.getOrElse(id, null)
- // inner syntax: id from props
- else st
- command.root_node.insert(command.node_from(kind, begin, end))
+ // command and keyword declarations
+ case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) =>
+ command_decls += name
+ case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+ keyword_decls += name
- // Phase changed
- case Elem("finished", _, _) =>
- st.phase = Phase.FINISHED
- fireChange(st)
- case Elem("unprocessed", _, _) =>
- st.phase = Phase.UNPROCESSED
- fireChange(st)
- case Elem("failed", _, _) =>
- st.phase = Phase.FAILED
- fireChange(st)
- case Elem("removed", _, _) =>
- document.prover.commands.removeKey(st.idString)
- st.phase = Phase.REMOVED
- fireChange(st)
- case _ =>
- })
- case _ =>
- if (st != null)
- handleResult(st, r, tree)
- }
+ // other markup
+ case XML.Elem(kind,
+ (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
+ (Markup.ID, markup_id) :: _, _) =>
+ val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
+ val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
+
+ val command =
+ // outer syntax: no id in props
+ if (st == null) commands.getOrElse(markup_id, null)
+ // inner syntax: id from props
+ else st
+ command.root_node.insert(command.node_from(kind, begin, end))
+
+ case _ =>
+ //}}}
+ }
+ }
+ case _ =>
+ }
+ //}}}
+
+ case IsabelleProcess.Kind.ERROR if st != null =>
+ if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)
+ st.status = Command.Status.FAILED
+ st.add_result(tree)
+ command_change(st)
+
+ case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
+ | IsabelleProcess.Kind.WARNING if st != null =>
+ st.add_result(tree)
+ command_change(st)
+
+ case _ =>
}
-
}
}
}
-
- def handleResult(st : Command, r : Result, tree : XML.Tree) {
+
- r.kind match {
- case IsabelleProcess.Kind.ERROR =>
- if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
- st.phase = Phase.FAILED
- st.addResult(tree)
- fireChange(st)
-
- case IsabelleProcess.Kind.WRITELN =>
- st.addResult(tree)
- fireChange(st)
-
- case IsabelleProcess.Kind.PRIORITY =>
- st.addResult(tree)
- fireChange(st)
+ def start(logic: String) {
+ if (logic != null) _logic = logic
- case IsabelleProcess.Kind.WARNING =>
- st.addResult(tree)
- fireChange(st)
-
- case IsabelleProcess.Kind.STATUS =>
- System.err.println("handleResult - Ignored: " + tree)
+ val results = new EventBus[IsabelleProcess.Result]
+ results += handle_result
+ results.logger = Log.log(Log.ERROR, null, _)
- case _ =>
- }
- }
-
- def logic = _logic
-
- def start(logic : String) {
- if (logic != null)
- _logic = logic
- process = new IsabelleProcess("-m", "xsymbols", _logic)
- worker_thread.start
+ process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
}
def stop() {
process.kill
}
-
- private def inUIThread(runnable : () => Unit) {
- SwingUtilities invokeAndWait new Runnable() {
- override def run() { runnable () }
- }
- }
-
- def setDocument(text : Text, path : String) {
+
+ def set_document(text: Text, path: String) {
this.document = new Document(text, this)
- process.ML("ThyLoad.add_path " + encode_string(path))
+ process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
- document.structuralChanges.add(changes => {
+ document.structural_changes += (changes => {
for (cmd <- changes.removedCommands) remove(cmd)
for (cmd <- changes.addedCommands) send(cmd)
})
if (initialized) {
document.activate()
- activated.fire(())
+ activated.event(())
}
}
-
- private def send(cmd : Command) {
- commands.put(cmd.idString, cmd)
-
- val props = new Properties()
- props.setProperty("id", cmd.idString)
- props.setProperty("offset", Integer.toString(1))
+
+ private def send(cmd: Command) {
+ cmd.status = Command.Status.UNPROCESSED
+ commands.put(cmd.id, cmd)
- val content = converter.encode(document.getContent(cmd))
- process.output_sync("Isar.command "
- + encode_properties(props)
- + " "
- + encode_string(content))
-
- process.output_sync("Isar.insert "
- + encode_string(if (cmd.previous == null) ""
- else cmd.previous.idString)
- + " "
- + encode_string(cmd.idString))
-
- cmd.phase = Phase.UNPROCESSED
+ val content = isabelle_symbols.encode(document.getContent(cmd))
+ process.create_command(cmd.id, content)
+ process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id)
}
-
- def remove(cmd : Command) {
- cmd.phase = Phase.REMOVE
- process.output_sync("Isar.remove " + encode_string(cmd.idString))
+ def remove(cmd: Command) {
+ cmd.status = Command.Status.REMOVE
+ process.remove_command(cmd.id)
}
-}
\ No newline at end of file
+}