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