src/Pure/Isar/isar_document.scala
changeset 29553 c3b937e8597b
child 29644 fbbd0197155c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/isar_document.scala	Sun Jan 18 20:06:51 2009 +0100
     1.3 @@ -0,0 +1,61 @@
     1.4 +/*  Title:      Pure/Isar/isar_document.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Interactive Isar documents.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object IsarDocument
    1.14 +{
    1.15 +  /* unique identifiers */
    1.16 +
    1.17 +  type State_ID = String
    1.18 +  type Command_ID = String
    1.19 +  type Document_ID = String
    1.20 +
    1.21 +
    1.22 +  /* commands */
    1.23 +
    1.24 +  def define_command(proc: IsabelleProcess, id: Command_ID, text: String) {
    1.25 +    proc.output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
    1.26 +      IsabelleSyntax.encode_string(text))
    1.27 +  }
    1.28 +
    1.29 +
    1.30 +  /* documents */
    1.31 +
    1.32 +  def begin_document(proc: IsabelleProcess, id: Document_ID, path: String) {
    1.33 +    proc.output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
    1.34 +       IsabelleSyntax.encode_string(path))
    1.35 +  }
    1.36 +
    1.37 +  def end_document(proc: IsabelleProcess, id: Document_ID) {
    1.38 +    proc.output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
    1.39 +  }
    1.40 +
    1.41 +  def edit_document(proc: IsabelleProcess, old_id: Document_ID, new_id: Document_ID,
    1.42 +      edits: List[(Command_ID, Option[Command_ID])])
    1.43 +  {
    1.44 +    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
    1.45 +    {
    1.46 +      edit match {
    1.47 +        case (id, None) => IsabelleSyntax.append_string(id, result)
    1.48 +        case (id, Some(id2)) =>
    1.49 +          IsabelleSyntax.append_string(id, result)
    1.50 +          result.append(" ")
    1.51 +          IsabelleSyntax.append_string(id2, result)
    1.52 +      }
    1.53 +    }
    1.54 +
    1.55 +    val buf = new StringBuilder(40)
    1.56 +    buf.append("Isar.edit_document ")
    1.57 +    IsabelleSyntax.append_string(old_id, buf)
    1.58 +    buf.append(" ")
    1.59 +    IsabelleSyntax.append_string(new_id, buf)
    1.60 +    buf.append(" ")
    1.61 +    IsabelleSyntax.append_list(append_edit, edits, buf)
    1.62 +    proc.output_sync(buf.toString)
    1.63 +  }
    1.64 +}