--- a/src/Tools/jEdit/src/prover/Prover.scala Tue Dec 08 14:29:29 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,175 +0,0 @@
-/*
- * Higher-level prover communication: interactive document model
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.prover
-
-
-import scala.actors.Actor, Actor._
-
-import javax.swing.JTextArea
-
-import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{ProofDocument, Change, Token}
-
-
-class Prover(system: Isabelle_System, logic: String)
-{
- /* incoming messages */
-
- private var prover_ready = false
-
- private val receiver = new Actor {
- def act() {
- loop {
- react {
- case result: Isabelle_Process.Result => handle_result(result)
- case change: Change if prover_ready => handle_change(change)
- case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
- }
- }
- }
- }
-
- def input(change: Change) { receiver ! change }
-
-
- /* outgoing messages */
-
- val command_change = new Event_Bus[Command]
- val document_change = new Event_Bus[ProofDocument]
-
-
- /* prover process */
-
- private val process =
- new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
-
-
- /* outer syntax keywords and completion */
-
- @volatile private var _command_decls = Map[String, String]()
- def command_decls() = _command_decls
-
- @volatile private var _keyword_decls = Set[String]()
- def keyword_decls() = _keyword_decls
-
- @volatile private var _completion = Isabelle.completion
- def completion() = _completion
-
-
- /* document state information */
-
- @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
- @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
- val document_0 =
- ProofDocument.empty.
- set_command_keyword((s: String) => command_decls().contains(s))
- @volatile private var document_versions = List(document_0)
-
- def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
- def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
- document_versions.find(_.id == id)
-
-
- /* prover results */
-
- val output_text_view = new JTextArea // FIXME separate jEdit component
-
- private def handle_result(result: Isabelle_Process.Result)
- {
- // FIXME separate jEdit component
- Swing_Thread.later { output_text_view.append(result.toString + "\n") }
-
- val message = Isabelle_Process.parse_message(system, result)
-
- val state =
- Position.id_of(result.props) match {
- case None => None
- case Some(id) => commands.get(id) orElse states.get(id) orElse None
- }
- if (state.isDefined) state.get ! (this, message)
- else if (result.kind == Isabelle_Process.Kind.STATUS) {
- //{{{ global status message
- message match {
- case XML.Elem(Markup.MESSAGE, _, elems) =>
- for (elem <- elems) {
- elem match {
- // document edits
- case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
- document_versions.find(_.id == doc_id) match {
- case Some(doc) =>
- for {
- XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
- <- edits }
- {
- commands.get(cmd_id) match {
- case Some(cmd) =>
- val state = new Command_State(cmd)
- states += (state_id -> state)
- doc.states += (cmd -> state)
- command_change.event(cmd) // FIXME really!?
- case None =>
- }
- }
- case None =>
- }
-
- // command and keyword declarations
- case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
- _command_decls += (name -> kind)
- _completion += name
- case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
- _keyword_decls += name
- _completion += name
-
- // process ready (after initialization)
- case XML.Elem(Markup.READY, _, _) => prover_ready = true
-
- case _ =>
- }
- }
- case _ =>
- }
- //}}}
- }
- }
-
-
- /* document changes */
-
- def begin_document(path: String) {
- process.begin_document(document_0.id, path)
- }
-
- def handle_change(change: Change) {
- val old = document(change.parent.get.id).get
- val (doc, changes) = old.text_changed(change)
- document_versions ::= doc
-
- val id_changes = changes map { case (c1, c2) =>
- (c1.map(_.id).getOrElse(document_0.id),
- c2 match {
- case None => None
- case Some(command) =>
- commands += (command.id -> command)
- process.define_command(command.id, system.symbols.encode(command.content))
- Some(command.id)
- })
- }
- process.edit_document(old.id, doc.id, id_changes)
-
- document_change.event(doc)
- }
-
-
- /* main controls */
-
- def start() { receiver.start() }
-
- def stop() { process.kill() }
-}