wenzelm@29553: /*  Title:      Pure/Isar/isar_document.scala
wenzelm@29553:     Author:     Makarius
wenzelm@29553: 
wenzelm@29553: Interactive Isar documents.
wenzelm@29553: */
wenzelm@29553: 
wenzelm@29553: package isabelle
wenzelm@29553: 
wenzelm@29645: object IsarDocument {
wenzelm@29553:   /* unique identifiers */
wenzelm@29553: 
wenzelm@29553:   type State_ID = String
wenzelm@29553:   type Command_ID = String
wenzelm@29553:   type Document_ID = String
wenzelm@29645: }
wenzelm@29645: 
wenzelm@29645: trait IsarDocument extends IsabelleProcess
wenzelm@29645: {
wenzelm@29645:   import IsarDocument._
wenzelm@29553: 
wenzelm@29553: 
wenzelm@29553:   /* commands */
wenzelm@29553: 
wenzelm@29644:   def define_command(id: Command_ID, text: String) {
wenzelm@29644:     output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
wenzelm@29553:       IsabelleSyntax.encode_string(text))
wenzelm@29553:   }
wenzelm@29553: 
wenzelm@29553: 
wenzelm@29553:   /* documents */
wenzelm@29553: 
wenzelm@29644:   def begin_document(id: Document_ID, path: String) {
wenzelm@29644:     output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
wenzelm@29553:        IsabelleSyntax.encode_string(path))
wenzelm@29553:   }
wenzelm@29553: 
wenzelm@29644:   def end_document(id: Document_ID) {
wenzelm@29644:     output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
wenzelm@29553:   }
wenzelm@29553: 
wenzelm@29644:   def edit_document(old_id: Document_ID, new_id: Document_ID,
wenzelm@29553:       edits: List[(Command_ID, Option[Command_ID])])
wenzelm@29553:   {
wenzelm@29553:     def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
wenzelm@29553:     {
wenzelm@29553:       edit match {
wenzelm@29553:         case (id, None) => IsabelleSyntax.append_string(id, result)
wenzelm@29553:         case (id, Some(id2)) =>
wenzelm@29553:           IsabelleSyntax.append_string(id, result)
wenzelm@29553:           result.append(" ")
wenzelm@29553:           IsabelleSyntax.append_string(id2, result)
wenzelm@29553:       }
wenzelm@29553:     }
wenzelm@29553: 
wenzelm@29553:     val buf = new StringBuilder(40)
wenzelm@29553:     buf.append("Isar.edit_document ")
wenzelm@29553:     IsabelleSyntax.append_string(old_id, buf)
wenzelm@29553:     buf.append(" ")
wenzelm@29553:     IsabelleSyntax.append_string(new_id, buf)
wenzelm@29553:     buf.append(" ")
wenzelm@29553:     IsabelleSyntax.append_list(append_edit, edits, buf)
wenzelm@29644:     output_sync(buf.toString)
wenzelm@29553:   }
wenzelm@29553: }