src/Pure/Isar/isar_document.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 36682 3f989067f87d
child 38150 67fc24df3721
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
wenzelm@29553
     1
/*  Title:      Pure/Isar/isar_document.scala
wenzelm@29553
     2
    Author:     Makarius
wenzelm@29553
     3
wenzelm@29553
     4
Interactive Isar documents.
wenzelm@29553
     5
*/
wenzelm@29553
     6
wenzelm@29553
     7
package isabelle
wenzelm@29553
     8
wenzelm@32450
     9
wenzelm@32467
    10
object Isar_Document
wenzelm@32450
    11
{
wenzelm@29553
    12
  /* unique identifiers */
wenzelm@29553
    13
wenzelm@29553
    14
  type State_ID = String
wenzelm@29553
    15
  type Command_ID = String
wenzelm@29553
    16
  type Document_ID = String
wenzelm@36682
    17
wenzelm@36682
    18
wenzelm@36682
    19
  /* reports */
wenzelm@36682
    20
wenzelm@36682
    21
  object Assign {
wenzelm@36682
    22
    def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
wenzelm@36682
    23
      msg match {
wenzelm@36682
    24
        case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
wenzelm@36682
    25
        case _ => None
wenzelm@36682
    26
      }
wenzelm@36682
    27
  }
wenzelm@36682
    28
wenzelm@36682
    29
  object Edit {
wenzelm@36682
    30
    def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
wenzelm@36682
    31
      msg match {
wenzelm@36682
    32
        case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
wenzelm@36682
    33
          Some(cmd_id, state_id)
wenzelm@36682
    34
        case _ => None
wenzelm@36682
    35
      }
wenzelm@36682
    36
  }
wenzelm@29645
    37
}
wenzelm@29645
    38
wenzelm@32450
    39
wenzelm@32467
    40
trait Isar_Document extends Isabelle_Process
wenzelm@29645
    41
{
wenzelm@32467
    42
  import Isar_Document._
wenzelm@29553
    43
wenzelm@29553
    44
wenzelm@29553
    45
  /* commands */
wenzelm@29553
    46
wenzelm@29644
    47
  def define_command(id: Command_ID, text: String) {
wenzelm@32448
    48
    output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
wenzelm@32448
    49
      Isabelle_Syntax.encode_string(text))
wenzelm@29553
    50
  }
wenzelm@29553
    51
wenzelm@29553
    52
wenzelm@29553
    53
  /* documents */
wenzelm@29553
    54
wenzelm@29644
    55
  def begin_document(id: Document_ID, path: String) {
wenzelm@32448
    56
    output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
wenzelm@32448
    57
      Isabelle_Syntax.encode_string(path))
wenzelm@29553
    58
  }
wenzelm@29553
    59
wenzelm@29644
    60
  def end_document(id: Document_ID) {
wenzelm@32448
    61
    output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
wenzelm@29553
    62
  }
wenzelm@29553
    63
wenzelm@29644
    64
  def edit_document(old_id: Document_ID, new_id: Document_ID,
wenzelm@29553
    65
      edits: List[(Command_ID, Option[Command_ID])])
wenzelm@29553
    66
  {
wenzelm@29553
    67
    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
wenzelm@29553
    68
    {
wenzelm@29553
    69
      edit match {
wenzelm@32448
    70
        case (id, None) => Isabelle_Syntax.append_string(id, result)
wenzelm@29553
    71
        case (id, Some(id2)) =>
wenzelm@32448
    72
          Isabelle_Syntax.append_string(id, result)
wenzelm@29553
    73
          result.append(" ")
wenzelm@32448
    74
          Isabelle_Syntax.append_string(id2, result)
wenzelm@29553
    75
      }
wenzelm@29553
    76
    }
wenzelm@29553
    77
wenzelm@29553
    78
    val buf = new StringBuilder(40)
wenzelm@29553
    79
    buf.append("Isar.edit_document ")
wenzelm@32448
    80
    Isabelle_Syntax.append_string(old_id, buf)
wenzelm@29553
    81
    buf.append(" ")
wenzelm@32448
    82
    Isabelle_Syntax.append_string(new_id, buf)
wenzelm@29553
    83
    buf.append(" ")
wenzelm@32448
    84
    Isabelle_Syntax.append_list(append_edit, edits, buf)
wenzelm@29644
    85
    output_sync(buf.toString)
wenzelm@29553
    86
  }
wenzelm@29553
    87
}