src/Tools/jEdit/src/proofdocument/prover.scala
changeset 34759 bfea7839d9e1
parent 34742 7b8847852aae
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,175 @@
     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 +}