src/Pure/Isar/isar_document.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 36682 3f989067f87d
child 38150 67fc24df3721
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     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   /* reports */
    20 
    21   object Assign {
    22     def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
    23       msg match {
    24         case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
    25         case _ => None
    26       }
    27   }
    28 
    29   object Edit {
    30     def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
    31       msg match {
    32         case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
    33           Some(cmd_id, state_id)
    34         case _ => None
    35       }
    36   }
    37 }
    38 
    39 
    40 trait Isar_Document extends Isabelle_Process
    41 {
    42   import Isar_Document._
    43 
    44 
    45   /* commands */
    46 
    47   def define_command(id: Command_ID, text: String) {
    48     output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
    49       Isabelle_Syntax.encode_string(text))
    50   }
    51 
    52 
    53   /* documents */
    54 
    55   def begin_document(id: Document_ID, path: String) {
    56     output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
    57       Isabelle_Syntax.encode_string(path))
    58   }
    59 
    60   def end_document(id: Document_ID) {
    61     output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
    62   }
    63 
    64   def edit_document(old_id: Document_ID, new_id: Document_ID,
    65       edits: List[(Command_ID, Option[Command_ID])])
    66   {
    67     def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
    68     {
    69       edit match {
    70         case (id, None) => Isabelle_Syntax.append_string(id, result)
    71         case (id, Some(id2)) =>
    72           Isabelle_Syntax.append_string(id, result)
    73           result.append(" ")
    74           Isabelle_Syntax.append_string(id2, result)
    75       }
    76     }
    77 
    78     val buf = new StringBuilder(40)
    79     buf.append("Isar.edit_document ")
    80     Isabelle_Syntax.append_string(old_id, buf)
    81     buf.append(" ")
    82     Isabelle_Syntax.append_string(new_id, buf)
    83     buf.append(" ")
    84     Isabelle_Syntax.append_list(append_edit, edits, buf)
    85     output_sync(buf.toString)
    86   }
    87 }