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