Scala wrapper for interactive Isar documents;
authorwenzelm
Sun Jan 18 20:06:51 2009 +0100 (2009-01-18)
changeset 29553c3b937e8597b
parent 29552 5b21c79785b0
child 29554 7e5e5ebb7bf7
Scala wrapper for interactive Isar documents;
src/Pure/IsaMakefile
src/Pure/Isar/isar_document.scala
     1.1 --- a/src/Pure/IsaMakefile	Sun Jan 18 20:05:01 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Sun Jan 18 20:06:51 2009 +0100
     1.3 @@ -126,9 +126,9 @@
     1.4  SCALA_FILES = General/event_bus.scala General/markup.scala		\
     1.5    General/position.scala General/swing.scala General/symbol.scala	\
     1.6    General/xml.scala General/yxml.scala Isar/isar.scala			\
     1.7 -  Isar/outer_keyword.scala Thy/thy_header.scala				\
     1.8 -  Tools/isabelle_process.scala Tools/isabelle_syntax.scala		\
     1.9 -  Tools/isabelle_system.scala
    1.10 +  Isar/isar_document.scala Isar/outer_keyword.scala			\
    1.11 +  Thy/thy_header.scala Tools/isabelle_process.scala			\
    1.12 +  Tools/isabelle_syntax.scala Tools/isabelle_system.scala
    1.13  
    1.14  
    1.15  SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Isar/isar_document.scala	Sun Jan 18 20:06:51 2009 +0100
     2.3 @@ -0,0 +1,61 @@
     2.4 +/*  Title:      Pure/Isar/isar_document.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Interactive Isar documents.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object IsarDocument
    2.14 +{
    2.15 +  /* unique identifiers */
    2.16 +
    2.17 +  type State_ID = String
    2.18 +  type Command_ID = String
    2.19 +  type Document_ID = String
    2.20 +
    2.21 +
    2.22 +  /* commands */
    2.23 +
    2.24 +  def define_command(proc: IsabelleProcess, id: Command_ID, text: String) {
    2.25 +    proc.output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
    2.26 +      IsabelleSyntax.encode_string(text))
    2.27 +  }
    2.28 +
    2.29 +
    2.30 +  /* documents */
    2.31 +
    2.32 +  def begin_document(proc: IsabelleProcess, id: Document_ID, path: String) {
    2.33 +    proc.output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
    2.34 +       IsabelleSyntax.encode_string(path))
    2.35 +  }
    2.36 +
    2.37 +  def end_document(proc: IsabelleProcess, id: Document_ID) {
    2.38 +    proc.output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
    2.39 +  }
    2.40 +
    2.41 +  def edit_document(proc: IsabelleProcess, old_id: Document_ID, new_id: Document_ID,
    2.42 +      edits: List[(Command_ID, Option[Command_ID])])
    2.43 +  {
    2.44 +    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
    2.45 +    {
    2.46 +      edit match {
    2.47 +        case (id, None) => IsabelleSyntax.append_string(id, result)
    2.48 +        case (id, Some(id2)) =>
    2.49 +          IsabelleSyntax.append_string(id, result)
    2.50 +          result.append(" ")
    2.51 +          IsabelleSyntax.append_string(id2, result)
    2.52 +      }
    2.53 +    }
    2.54 +
    2.55 +    val buf = new StringBuilder(40)
    2.56 +    buf.append("Isar.edit_document ")
    2.57 +    IsabelleSyntax.append_string(old_id, buf)
    2.58 +    buf.append(" ")
    2.59 +    IsabelleSyntax.append_string(new_id, buf)
    2.60 +    buf.append(" ")
    2.61 +    IsabelleSyntax.append_list(append_edit, edits, buf)
    2.62 +    proc.output_sync(buf.toString)
    2.63 +  }
    2.64 +}