src/Pure/Isar/isar_document.scala
author wenzelm
Thu, 25 Jun 2009 13:25:35 +0200
changeset 31797 203d5e61e3bc
parent 31237 5c1aca930404
child 32448 a89f876731c5
permissions -rw-r--r--
renamed IsabelleProcess to Isabelle_Process; renamed IsabelleSystem to Isabelle_System;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Isar/isar_document.scala
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     3
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     4
Interactive Isar documents.
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     5
*/
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     6
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     7
package isabelle
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
     8
29645
bbc8de8d1c8c plain non-dependent types;
wenzelm
parents: 29644
diff changeset
     9
object IsarDocument {
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    10
  /* unique identifiers */
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    11
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    12
  type State_ID = String
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    13
  type Command_ID = String
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    14
  type Document_ID = String
29645
bbc8de8d1c8c plain non-dependent types;
wenzelm
parents: 29644
diff changeset
    15
}
bbc8de8d1c8c plain non-dependent types;
wenzelm
parents: 29644
diff changeset
    16
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31237
diff changeset
    17
trait IsarDocument extends Isabelle_Process
29645
bbc8de8d1c8c plain non-dependent types;
wenzelm
parents: 29644
diff changeset
    18
{
bbc8de8d1c8c plain non-dependent types;
wenzelm
parents: 29644
diff changeset
    19
  import IsarDocument._
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    20
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    21
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    22
  /* commands */
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    23
29644
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    24
  def define_command(id: Command_ID, text: String) {
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    25
    output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    26
      IsabelleSyntax.encode_string(text))
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    27
  }
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    28
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    29
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    30
  /* documents */
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    31
29644
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    32
  def begin_document(id: Document_ID, path: String) {
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    33
    output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
31237
5c1aca930404 proper indentation;
wenzelm
parents: 29645
diff changeset
    34
      IsabelleSyntax.encode_string(path))
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    35
  }
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    36
29644
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    37
  def end_document(id: Document_ID) {
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    38
    output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    39
  }
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    40
29644
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    41
  def edit_document(old_id: Document_ID, new_id: Document_ID,
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    42
      edits: List[(Command_ID, Option[Command_ID])])
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    43
  {
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    44
    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    45
    {
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    46
      edit match {
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    47
        case (id, None) => IsabelleSyntax.append_string(id, result)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    48
        case (id, Some(id2)) =>
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    49
          IsabelleSyntax.append_string(id, result)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    50
          result.append(" ")
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    51
          IsabelleSyntax.append_string(id2, result)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    52
      }
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    53
    }
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    54
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    55
    val buf = new StringBuilder(40)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    56
    buf.append("Isar.edit_document ")
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    57
    IsabelleSyntax.append_string(old_id, buf)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    58
    buf.append(" ")
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    59
    IsabelleSyntax.append_string(new_id, buf)
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    60
    buf.append(" ")
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    61
    IsabelleSyntax.append_list(append_edit, edits, buf)
29644
fbbd0197155c turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents: 29553
diff changeset
    62
    output_sync(buf.toString)
29553
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    63
  }
c3b937e8597b Scala wrapper for interactive Isar documents;
wenzelm
parents:
diff changeset
    64
}