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;
     1 /*  Title:      Pure/Isar/isar_document.scala
     2     Author:     Makarius
     3 
     4 Interactive Isar documents.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Isar_Document
    11 {
    12   /* unique identifiers */
    13 
    14   type State_ID = String
    15   type Command_ID = String
    16   type Document_ID = String
    17 }
    18 
    19 
    20 trait Isar_Document extends Isabelle_Process
    21 {
    22   import Isar_Document._
    23 
    24 
    25   /* commands */
    26 
    27   def define_command(id: Command_ID, text: String) {
    28     output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
    29       Isabelle_Syntax.encode_string(text))
    30   }
    31 
    32 
    33   /* documents */
    34 
    35   def begin_document(id: Document_ID, path: String) {
    36     output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
    37       Isabelle_Syntax.encode_string(path))
    38   }
    39 
    40   def end_document(id: Document_ID) {
    41     output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
    42   }
    43 
    44   def edit_document(old_id: Document_ID, new_id: Document_ID,
    45       edits: List[(Command_ID, Option[Command_ID])])
    46   {
    47     def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
    48     {
    49       edit match {
    50         case (id, None) => Isabelle_Syntax.append_string(id, result)
    51         case (id, Some(id2)) =>
    52           Isabelle_Syntax.append_string(id, result)
    53           result.append(" ")
    54           Isabelle_Syntax.append_string(id2, result)
    55       }
    56     }
    57 
    58     val buf = new StringBuilder(40)
    59     buf.append("Isar.edit_document ")
    60     Isabelle_Syntax.append_string(old_id, buf)
    61     buf.append(" ")
    62     Isabelle_Syntax.append_string(new_id, buf)
    63     buf.append(" ")
    64     Isabelle_Syntax.append_list(append_edit, edits, buf)
    65     output_sync(buf.toString)
    66   }
    67 }