turned IsarDocument into trait for IsabelleProcess;
authorwenzelm
Tue Jan 27 15:22:46 2009 +0100 (2009-01-27)
changeset 29644fbbd0197155c
parent 29643 5e0df4b6849e
child 29645 bbc8de8d1c8c
turned IsarDocument into trait for IsabelleProcess;
src/Pure/Isar/isar_document.scala
     1.1 --- a/src/Pure/Isar/isar_document.scala	Tue Jan 27 14:45:52 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_document.scala	Tue Jan 27 15:22:46 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -object IsarDocument
     1.8 +trait IsarDocument extends IsabelleProcess
     1.9  {
    1.10    /* unique identifiers */
    1.11  
    1.12 @@ -18,24 +18,24 @@
    1.13  
    1.14    /* commands */
    1.15  
    1.16 -  def define_command(proc: IsabelleProcess, id: Command_ID, text: String) {
    1.17 -    proc.output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
    1.18 +  def define_command(id: Command_ID, text: String) {
    1.19 +    output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
    1.20        IsabelleSyntax.encode_string(text))
    1.21    }
    1.22  
    1.23  
    1.24    /* documents */
    1.25  
    1.26 -  def begin_document(proc: IsabelleProcess, id: Document_ID, path: String) {
    1.27 -    proc.output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
    1.28 +  def begin_document(id: Document_ID, path: String) {
    1.29 +    output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
    1.30         IsabelleSyntax.encode_string(path))
    1.31    }
    1.32  
    1.33 -  def end_document(proc: IsabelleProcess, id: Document_ID) {
    1.34 -    proc.output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
    1.35 +  def end_document(id: Document_ID) {
    1.36 +    output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
    1.37    }
    1.38  
    1.39 -  def edit_document(proc: IsabelleProcess, old_id: Document_ID, new_id: Document_ID,
    1.40 +  def edit_document(old_id: Document_ID, new_id: Document_ID,
    1.41        edits: List[(Command_ID, Option[Command_ID])])
    1.42    {
    1.43      def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
    1.44 @@ -56,6 +56,6 @@
    1.45      IsabelleSyntax.append_string(new_id, buf)
    1.46      buf.append(" ")
    1.47      IsabelleSyntax.append_list(append_edit, edits, buf)
    1.48 -    proc.output_sync(buf.toString)
    1.49 +    output_sync(buf.toString)
    1.50    }
    1.51  }