src/Pure/Isar/isar_document.scala
author wenzelm
Thu Jun 25 13:25:35 2009 +0200 (2009-06-25 ago)
changeset 31797 203d5e61e3bc
parent 31237 5c1aca930404
child 32448 a89f876731c5
permissions -rw-r--r--
renamed IsabelleProcess to Isabelle_Process;
renamed IsabelleSystem to Isabelle_System;
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@29645
     9
object IsarDocument {
wenzelm@29553
    10
  /* unique identifiers */
wenzelm@29553
    11
wenzelm@29553
    12
  type State_ID = String
wenzelm@29553
    13
  type Command_ID = String
wenzelm@29553
    14
  type Document_ID = String
wenzelm@29645
    15
}
wenzelm@29645
    16
wenzelm@31797
    17
trait IsarDocument extends Isabelle_Process
wenzelm@29645
    18
{
wenzelm@29645
    19
  import IsarDocument._
wenzelm@29553
    20
wenzelm@29553
    21
wenzelm@29553
    22
  /* commands */
wenzelm@29553
    23
wenzelm@29644
    24
  def define_command(id: Command_ID, text: String) {
wenzelm@29644
    25
    output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
wenzelm@29553
    26
      IsabelleSyntax.encode_string(text))
wenzelm@29553
    27
  }
wenzelm@29553
    28
wenzelm@29553
    29
wenzelm@29553
    30
  /* documents */
wenzelm@29553
    31
wenzelm@29644
    32
  def begin_document(id: Document_ID, path: String) {
wenzelm@29644
    33
    output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
wenzelm@31237
    34
      IsabelleSyntax.encode_string(path))
wenzelm@29553
    35
  }
wenzelm@29553
    36
wenzelm@29644
    37
  def end_document(id: Document_ID) {
wenzelm@29644
    38
    output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
wenzelm@29553
    39
  }
wenzelm@29553
    40
wenzelm@29644
    41
  def edit_document(old_id: Document_ID, new_id: Document_ID,
wenzelm@29553
    42
      edits: List[(Command_ID, Option[Command_ID])])
wenzelm@29553
    43
  {
wenzelm@29553
    44
    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
wenzelm@29553
    45
    {
wenzelm@29553
    46
      edit match {
wenzelm@29553
    47
        case (id, None) => IsabelleSyntax.append_string(id, result)
wenzelm@29553
    48
        case (id, Some(id2)) =>
wenzelm@29553
    49
          IsabelleSyntax.append_string(id, result)
wenzelm@29553
    50
          result.append(" ")
wenzelm@29553
    51
          IsabelleSyntax.append_string(id2, result)
wenzelm@29553
    52
      }
wenzelm@29553
    53
    }
wenzelm@29553
    54
wenzelm@29553
    55
    val buf = new StringBuilder(40)
wenzelm@29553
    56
    buf.append("Isar.edit_document ")
wenzelm@29553
    57
    IsabelleSyntax.append_string(old_id, buf)
wenzelm@29553
    58
    buf.append(" ")
wenzelm@29553
    59
    IsabelleSyntax.append_string(new_id, buf)
wenzelm@29553
    60
    buf.append(" ")
wenzelm@29553
    61
    IsabelleSyntax.append_list(append_edit, edits, buf)
wenzelm@29644
    62
    output_sync(buf.toString)
wenzelm@29553
    63
  }
wenzelm@29553
    64
}