src/Pure/Isar/isar_document.scala
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 32467 4dab52ca1402
child 36682 3f989067f87d
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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@29645
    17
}
wenzelm@29645
    18
wenzelm@32450
    19
wenzelm@32467
    20
trait Isar_Document extends Isabelle_Process
wenzelm@29645
    21
{
wenzelm@32467
    22
  import Isar_Document._
wenzelm@29553
    23
wenzelm@29553
    24
wenzelm@29553
    25
  /* commands */
wenzelm@29553
    26
wenzelm@29644
    27
  def define_command(id: Command_ID, text: String) {
wenzelm@32448
    28
    output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
wenzelm@32448
    29
      Isabelle_Syntax.encode_string(text))
wenzelm@29553
    30
  }
wenzelm@29553
    31
wenzelm@29553
    32
wenzelm@29553
    33
  /* documents */
wenzelm@29553
    34
wenzelm@29644
    35
  def begin_document(id: Document_ID, path: String) {
wenzelm@32448
    36
    output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
wenzelm@32448
    37
      Isabelle_Syntax.encode_string(path))
wenzelm@29553
    38
  }
wenzelm@29553
    39
wenzelm@29644
    40
  def end_document(id: Document_ID) {
wenzelm@32448
    41
    output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
wenzelm@29553
    42
  }
wenzelm@29553
    43
wenzelm@29644
    44
  def edit_document(old_id: Document_ID, new_id: Document_ID,
wenzelm@29553
    45
      edits: List[(Command_ID, Option[Command_ID])])
wenzelm@29553
    46
  {
wenzelm@29553
    47
    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
wenzelm@29553
    48
    {
wenzelm@29553
    49
      edit match {
wenzelm@32448
    50
        case (id, None) => Isabelle_Syntax.append_string(id, result)
wenzelm@29553
    51
        case (id, Some(id2)) =>
wenzelm@32448
    52
          Isabelle_Syntax.append_string(id, result)
wenzelm@29553
    53
          result.append(" ")
wenzelm@32448
    54
          Isabelle_Syntax.append_string(id2, result)
wenzelm@29553
    55
      }
wenzelm@29553
    56
    }
wenzelm@29553
    57
wenzelm@29553
    58
    val buf = new StringBuilder(40)
wenzelm@29553
    59
    buf.append("Isar.edit_document ")
wenzelm@32448
    60
    Isabelle_Syntax.append_string(old_id, buf)
wenzelm@29553
    61
    buf.append(" ")
wenzelm@32448
    62
    Isabelle_Syntax.append_string(new_id, buf)
wenzelm@29553
    63
    buf.append(" ")
wenzelm@32448
    64
    Isabelle_Syntax.append_list(append_edit, edits, buf)
wenzelm@29644
    65
    output_sync(buf.toString)
wenzelm@29553
    66
  }
wenzelm@29553
    67
}