--- a/src/Tools/jEdit/src/prover/Prover.scala Tue Jun 02 22:31:58 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jun 02 23:37:36 2009 +0200
@@ -113,17 +113,16 @@
else (false, null)
}
- if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN)
+ if (result.kind == IsabelleProcess.Kind.STDOUT ||
+ result.kind == IsabelleProcess.Kind.STDIN)
output_info.event(result.toString)
- else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !?
- initialized = true
- Swing.now { this ! ProverEvents.Activate }
- }
else {
result.kind match {
- case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
- | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR =>
+ case IsabelleProcess.Kind.WRITELN
+ | IsabelleProcess.Kind.PRIORITY
+ | IsabelleProcess.Kind.WARNING
+ | IsabelleProcess.Kind.ERROR =>
if (command != null) {
if (result.kind == IsabelleProcess.Kind.ERROR)
command.status = Command.Status.FAILED
@@ -147,6 +146,12 @@
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
keyword_decls += name
+ // process ready (after initialization)
+ case XML.Elem(Markup.READY, _, _)
+ if !initialized =>
+ initialized = true
+ Swing.now { this ! ProverEvents.Activate }
+
// document edits
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
if document_versions.exists(_.id == doc_id) =>