src/Tools/jEdit/src/prover/Prover.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,175 +0,0 @@
     1.4 -/*
     1.5 - * Higher-level prover communication: interactive document model
     1.6 - *
     1.7 - * @author Johannes Hölzl, TU Munich
     1.8 - * @author Fabian Immler, TU Munich
     1.9 - * @author Makarius
    1.10 - */
    1.11 -
    1.12 -package isabelle.prover
    1.13 -
    1.14 -
    1.15 -import scala.actors.Actor, Actor._
    1.16 -
    1.17 -import javax.swing.JTextArea
    1.18 -
    1.19 -import isabelle.jedit.Isabelle
    1.20 -import isabelle.proofdocument.{ProofDocument, Change, Token}
    1.21 -
    1.22 -
    1.23 -class Prover(system: Isabelle_System, logic: String)
    1.24 -{
    1.25 -  /* incoming messages */
    1.26 -
    1.27 -  private var prover_ready = false
    1.28 -
    1.29 -  private val receiver = new Actor {
    1.30 -    def act() {
    1.31 -      loop {
    1.32 -        react {
    1.33 -          case result: Isabelle_Process.Result => handle_result(result)
    1.34 -          case change: Change if prover_ready => handle_change(change)
    1.35 -          case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
    1.36 -        }
    1.37 -      }
    1.38 -    }
    1.39 -  }
    1.40 -
    1.41 -  def input(change: Change) { receiver ! change }
    1.42 -
    1.43 -
    1.44 -  /* outgoing messages */
    1.45 -
    1.46 -  val command_change = new Event_Bus[Command]
    1.47 -  val document_change = new Event_Bus[ProofDocument]
    1.48 -
    1.49 -
    1.50 -  /* prover process */
    1.51 -
    1.52 -  private val process =
    1.53 -    new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
    1.54 -
    1.55 -
    1.56 -  /* outer syntax keywords and completion */
    1.57 -
    1.58 -  @volatile private var _command_decls = Map[String, String]()
    1.59 -  def command_decls() = _command_decls
    1.60 -
    1.61 -  @volatile private var _keyword_decls = Set[String]()
    1.62 -  def keyword_decls() = _keyword_decls
    1.63 -
    1.64 -  @volatile private var _completion = Isabelle.completion
    1.65 -  def completion() = _completion
    1.66 -
    1.67 -
    1.68 -  /* document state information */
    1.69 -
    1.70 -  @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
    1.71 -  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
    1.72 -  val document_0 =
    1.73 -    ProofDocument.empty.
    1.74 -    set_command_keyword((s: String) => command_decls().contains(s))
    1.75 -  @volatile private var document_versions = List(document_0)
    1.76 -
    1.77 -  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
    1.78 -  def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
    1.79 -    document_versions.find(_.id == id)
    1.80 -
    1.81 -
    1.82 -  /* prover results */
    1.83 -
    1.84 -  val output_text_view = new JTextArea    // FIXME separate jEdit component
    1.85 -
    1.86 -  private def handle_result(result: Isabelle_Process.Result)
    1.87 -  {
    1.88 -    // FIXME separate jEdit component
    1.89 -    Swing_Thread.later { output_text_view.append(result.toString + "\n") }
    1.90 -
    1.91 -    val message = Isabelle_Process.parse_message(system, result)
    1.92 -
    1.93 -    val state =
    1.94 -      Position.id_of(result.props) match {
    1.95 -        case None => None
    1.96 -        case Some(id) => commands.get(id) orElse states.get(id) orElse None
    1.97 -      }
    1.98 -    if (state.isDefined) state.get ! (this, message)
    1.99 -    else if (result.kind == Isabelle_Process.Kind.STATUS) {
   1.100 -      //{{{ global status message
   1.101 -      message match {
   1.102 -        case XML.Elem(Markup.MESSAGE, _, elems) =>
   1.103 -          for (elem <- elems) {
   1.104 -            elem match {
   1.105 -              // document edits
   1.106 -              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
   1.107 -                document_versions.find(_.id == doc_id) match {
   1.108 -                  case Some(doc) =>
   1.109 -                    for {
   1.110 -                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
   1.111 -                      <- edits }
   1.112 -                    {
   1.113 -                      commands.get(cmd_id) match {
   1.114 -                        case Some(cmd) =>
   1.115 -                          val state = new Command_State(cmd)
   1.116 -                          states += (state_id -> state)
   1.117 -                          doc.states += (cmd -> state)
   1.118 -                          command_change.event(cmd)   // FIXME really!?
   1.119 -                        case None =>
   1.120 -                      }
   1.121 -                    }
   1.122 -                  case None =>
   1.123 -                }
   1.124 -
   1.125 -              // command and keyword declarations
   1.126 -              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
   1.127 -                _command_decls += (name -> kind)
   1.128 -                _completion += name
   1.129 -              case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
   1.130 -                _keyword_decls += name
   1.131 -                _completion += name
   1.132 -
   1.133 -              // process ready (after initialization)
   1.134 -              case XML.Elem(Markup.READY, _, _) => prover_ready = true
   1.135 -
   1.136 -              case _ =>
   1.137 -            }
   1.138 -          }
   1.139 -        case _ =>
   1.140 -      }
   1.141 -      //}}}
   1.142 -    }
   1.143 -  }
   1.144 -
   1.145 -
   1.146 -  /* document changes */
   1.147 -
   1.148 -  def begin_document(path: String) {
   1.149 -    process.begin_document(document_0.id, path)
   1.150 -  }
   1.151 -
   1.152 -  def handle_change(change: Change) {
   1.153 -    val old = document(change.parent.get.id).get
   1.154 -    val (doc, changes) = old.text_changed(change)
   1.155 -    document_versions ::= doc
   1.156 -
   1.157 -    val id_changes = changes map { case (c1, c2) =>
   1.158 -        (c1.map(_.id).getOrElse(document_0.id),
   1.159 -         c2 match {
   1.160 -            case None => None
   1.161 -            case Some(command) =>
   1.162 -              commands += (command.id -> command)
   1.163 -              process.define_command(command.id, system.symbols.encode(command.content))
   1.164 -              Some(command.id)
   1.165 -          })
   1.166 -    }
   1.167 -    process.edit_document(old.id, doc.id, id_changes)
   1.168 -
   1.169 -    document_change.event(doc)
   1.170 -  }
   1.171 -
   1.172 -
   1.173 -  /* main controls */
   1.174 -
   1.175 -  def start() { receiver.start() }
   1.176 -
   1.177 -  def stop() { process.kill() }
   1.178 -}