src/Tools/jEdit/src/proofdocument/prover.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34769 826525fc5285
permissions -rw-r--r--
misc modernization of names;
wenzelm@34407
     1
/*
wenzelm@34501
     2
 * Higher-level prover communication: interactive document model
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
wenzelm@34407
     5
 * @author Fabian Immler, TU Munich
wenzelm@34453
     6
 * @author Makarius
wenzelm@34407
     7
 */
wenzelm@34407
     8
wenzelm@34760
     9
package isabelle.proofdocument
wenzelm@34318
    10
wenzelm@34318
    11
wenzelm@34703
    12
import scala.actors.Actor, Actor._
immler@34538
    13
immler@34671
    14
import javax.swing.JTextArea
wenzelm@34456
    15
wenzelm@34501
    16
import isabelle.jedit.Isabelle
wenzelm@34318
    17
wenzelm@34703
    18
wenzelm@34742
    19
class Prover(system: Isabelle_System, logic: String)
wenzelm@34453
    20
{
wenzelm@34724
    21
  /* incoming messages */
wenzelm@34730
    22
wenzelm@34721
    23
  private var prover_ready = false
wenzelm@34721
    24
wenzelm@34742
    25
  private val receiver = new Actor {
wenzelm@34742
    26
    def act() {
wenzelm@34742
    27
      loop {
wenzelm@34742
    28
        react {
wenzelm@34742
    29
          case result: Isabelle_Process.Result => handle_result(result)
wenzelm@34742
    30
          case change: Change if prover_ready => handle_change(change)
wenzelm@34742
    31
          case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
wenzelm@34742
    32
        }
wenzelm@34721
    33
      }
wenzelm@34721
    34
    }
wenzelm@34721
    35
  }
wenzelm@34721
    36
wenzelm@34742
    37
  def input(change: Change) { receiver ! change }
wenzelm@34742
    38
wenzelm@34721
    39
wenzelm@34724
    40
  /* outgoing messages */
wenzelm@34730
    41
wenzelm@34724
    42
  val command_change = new Event_Bus[Command]
wenzelm@34760
    43
  val document_change = new Event_Bus[Proof_Document]
wenzelm@34724
    44
wenzelm@34724
    45
wenzelm@34504
    46
  /* prover process */
wenzelm@34504
    47
wenzelm@34533
    48
  private val process =
wenzelm@34742
    49
    new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
wenzelm@34504
    50
wenzelm@34730
    51
wenzelm@34720
    52
  /* outer syntax keywords and completion */
wenzelm@34720
    53
wenzelm@34723
    54
  @volatile private var _command_decls = Map[String, String]()
wenzelm@34723
    55
  def command_decls() = _command_decls
wenzelm@34723
    56
wenzelm@34720
    57
  @volatile private var _keyword_decls = Set[String]()
wenzelm@34720
    58
  def keyword_decls() = _keyword_decls
wenzelm@34720
    59
wenzelm@34720
    60
  @volatile private var _completion = Isabelle.completion
wenzelm@34720
    61
  def completion() = _completion
wenzelm@34720
    62
wenzelm@34720
    63
wenzelm@34509
    64
  /* document state information */
wenzelm@34509
    65
wenzelm@34721
    66
  @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
wenzelm@34721
    67
  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
immler@34654
    68
  val document_0 =
wenzelm@34760
    69
    Proof_Document.empty.
wenzelm@34740
    70
    set_command_keyword((s: String) => command_decls().contains(s))
wenzelm@34721
    71
  @volatile private var document_versions = List(document_0)
immler@34538
    72
wenzelm@34690
    73
  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
wenzelm@34760
    74
  def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
wenzelm@34740
    75
    document_versions.find(_.id == id)
wenzelm@34730
    76
wenzelm@34489
    77
wenzelm@34721
    78
  /* prover results */
wenzelm@34489
    79
wenzelm@34728
    80
  val output_text_view = new JTextArea    // FIXME separate jEdit component
immler@34671
    81
wenzelm@34615
    82
  private def handle_result(result: Isabelle_Process.Result)
wenzelm@34489
    83
  {
wenzelm@34728
    84
    // FIXME separate jEdit component
wenzelm@34728
    85
    Swing_Thread.later { output_text_view.append(result.toString + "\n") }
wenzelm@34728
    86
wenzelm@34728
    87
    val message = Isabelle_Process.parse_message(system, result)
wenzelm@34728
    88
immler@34676
    89
    val state =
wenzelm@34740
    90
      Position.id_of(result.props) match {
wenzelm@34740
    91
        case None => None
wenzelm@34740
    92
        case Some(id) => commands.get(id) orElse states.get(id) orElse None
wenzelm@34740
    93
      }
wenzelm@34724
    94
    if (state.isDefined) state.get ! (this, message)
wenzelm@34728
    95
    else if (result.kind == Isabelle_Process.Kind.STATUS) {
wenzelm@34728
    96
      //{{{ global status message
wenzelm@34728
    97
      message match {
wenzelm@34728
    98
        case XML.Elem(Markup.MESSAGE, _, elems) =>
wenzelm@34728
    99
          for (elem <- elems) {
wenzelm@34728
   100
            elem match {
wenzelm@34728
   101
              // document edits
wenzelm@34740
   102
              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
wenzelm@34740
   103
                document_versions.find(_.id == doc_id) match {
wenzelm@34740
   104
                  case Some(doc) =>
wenzelm@34740
   105
                    for {
wenzelm@34740
   106
                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
wenzelm@34741
   107
                      <- edits }
wenzelm@34741
   108
                    {
wenzelm@34741
   109
                      commands.get(cmd_id) match {
wenzelm@34741
   110
                        case Some(cmd) =>
wenzelm@34741
   111
                          val state = new Command_State(cmd)
wenzelm@34741
   112
                          states += (state_id -> state)
wenzelm@34741
   113
                          doc.states += (cmd -> state)
wenzelm@34742
   114
                          command_change.event(cmd)   // FIXME really!?
wenzelm@34741
   115
                        case None =>
wenzelm@34741
   116
                      }
wenzelm@34740
   117
                    }
wenzelm@34740
   118
                  case None =>
wenzelm@34728
   119
                }
wenzelm@34730
   120
wenzelm@34741
   121
              // command and keyword declarations
wenzelm@34740
   122
              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
wenzelm@34728
   123
                _command_decls += (name -> kind)
wenzelm@34728
   124
                _completion += name
wenzelm@34728
   125
              case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
wenzelm@34728
   126
                _keyword_decls += name
wenzelm@34728
   127
                _completion += name
wenzelm@34453
   128
wenzelm@34741
   129
              // process ready (after initialization)
wenzelm@34728
   130
              case XML.Elem(Markup.READY, _, _) => prover_ready = true
wenzelm@34728
   131
wenzelm@34728
   132
              case _ =>
immler@34676
   133
            }
wenzelm@34728
   134
          }
wenzelm@34728
   135
        case _ =>
wenzelm@34728
   136
      }
wenzelm@34728
   137
      //}}}
wenzelm@34318
   138
    }
wenzelm@34318
   139
  }
wenzelm@34453
   140
wenzelm@34721
   141
wenzelm@34721
   142
  /* document changes */
wenzelm@34721
   143
wenzelm@34729
   144
  def begin_document(path: String) {
immler@34650
   145
    process.begin_document(document_0.id, path)
wenzelm@34318
   146
  }
wenzelm@34453
   147
wenzelm@34729
   148
  def handle_change(change: Change) {
wenzelm@34729
   149
    val old = document(change.parent.get.id).get
wenzelm@34729
   150
    val (doc, changes) = old.text_changed(change)
wenzelm@34729
   151
    document_versions ::= doc
wenzelm@34729
   152
wenzelm@34709
   153
    val id_changes = changes map { case (c1, c2) =>
wenzelm@34730
   154
        (c1.map(_.id).getOrElse(document_0.id),
wenzelm@34730
   155
         c2 match {
wenzelm@34730
   156
            case None => None
wenzelm@34730
   157
            case Some(command) =>
wenzelm@34730
   158
              commands += (command.id -> command)
wenzelm@34730
   159
              process.define_command(command.id, system.symbols.encode(command.content))
wenzelm@34730
   160
              Some(command.id)
wenzelm@34730
   161
          })
immler@34660
   162
    }
immler@34660
   163
    process.edit_document(old.id, doc.id, id_changes)
wenzelm@34729
   164
wenzelm@34729
   165
    document_change.event(doc)
immler@34650
   166
  }
wenzelm@34742
   167
wenzelm@34742
   168
wenzelm@34742
   169
  /* main controls */
wenzelm@34742
   170
wenzelm@34742
   171
  def start() { receiver.start() }
wenzelm@34742
   172
wenzelm@34742
   173
  def stop() { process.kill() }
wenzelm@34453
   174
}