src/Pure/PIDE/isar_document.scala
author wenzelm
Fri, 12 Aug 2011 12:03:17 +0200
changeset 44159 9a35e88d9dc9
parent 44158 fe6d1ae7a065
child 44182 ecb51b457064
permissions -rw-r--r--
simplified class Thy_Header;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38483
3d16bebee1d3 moved Isar_Document to Pure/PIDE;
wenzelm
parents: 38448
diff changeset
     1
/*  Title:      Pure/PIDE/isar_document.scala
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     3
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
     4
Protocol message formats for interactive Isar documents.
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     5
*/
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     6
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     7
package isabelle
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     8
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     9
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    10
object Isar_Document
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    11
{
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    12
  /* document editing */
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    13
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    14
  object Assign {
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    15
    def unapply(msg: XML.Tree)
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    16
        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    17
      msg match {
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    18
        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    19
          val id_edits = edits.map(Edit.unapply)
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    20
          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    21
          else None
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    22
        case _ => None
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    23
      }
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    24
  }
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    25
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    26
  object Edit {
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    27
    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    28
      msg match {
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    29
        case XML.Elem(
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    30
          Markup(Markup.EDIT,
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
    31
            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    32
        case _ => None
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    33
      }
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    34
  }
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    35
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    36
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    37
  /* toplevel transactions */
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    38
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    39
  sealed abstract class Status
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    40
  case class Forked(forks: Int) extends Status
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    41
  case object Unprocessed extends Status
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    42
  case object Finished extends Status
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    43
  case object Failed extends Status
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    44
38581
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38567
diff changeset
    45
  def command_status(markup: List[Markup]): Status =
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    46
  {
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    47
    val forks = (0 /: markup) {
38581
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38567
diff changeset
    48
      case (i, Markup(Markup.FORKED, _)) => i + 1
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38567
diff changeset
    49
      case (i, Markup(Markup.JOINED, _)) => i - 1
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    50
      case (i, _) => i
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    51
    }
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    52
    if (forks != 0) Forked(forks)
38581
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38567
diff changeset
    53
    else if (markup.exists(_.name == Markup.FAILED)) Failed
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38567
diff changeset
    54
    else if (markup.exists(_.name == Markup.FINISHED)) Finished
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    55
    else Unprocessed
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    56
  }
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
    57
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
    58
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    59
  /* result messages */
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
    60
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
    61
  def clean_message(body: XML.Body): XML.Body =
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
    62
    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
    63
      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
    64
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    65
  def message_reports(msg: XML.Tree): List[XML.Elem] =
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    66
    msg match {
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    67
      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    68
      case XML.Elem(_, body) => body.flatMap(message_reports)
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    69
      case XML.Text(_) => Nil
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    70
    }
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
    71
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
    72
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    73
  /* specific messages */
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    74
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    75
  def is_ready(msg: XML.Tree): Boolean =
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    76
    msg match {
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    77
      case XML.Elem(Markup(Markup.STATUS, _),
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    78
        List(XML.Elem(Markup(Markup.READY, _), _))) => true
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    79
      case _ => false
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    80
    }
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    81
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
    82
 def is_tracing(msg: XML.Tree): Boolean =
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
    83
    msg match {
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
    84
      case XML.Elem(Markup(Markup.TRACING, _), _) => true
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
    85
      case _ => false
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
    86
    }
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
    87
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    88
  def is_warning(msg: XML.Tree): Boolean =
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    89
    msg match {
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    90
      case XML.Elem(Markup(Markup.WARNING, _), _) => true
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    91
      case _ => false
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    92
    }
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    93
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    94
  def is_error(msg: XML.Tree): Boolean =
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    95
    msg match {
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    96
      case XML.Elem(Markup(Markup.ERROR, _), _) => true
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    97
      case _ => false
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
    98
    }
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
    99
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   100
  def is_state(msg: XML.Tree): Boolean =
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   101
    msg match {
39627
wenzelm
parents: 39625
diff changeset
   102
      case XML.Elem(Markup(Markup.WRITELN, _),
wenzelm
parents: 39625
diff changeset
   103
        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   104
      case _ => false
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   105
    }
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   106
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   107
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   108
  /* reported positions */
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   109
39627
wenzelm
parents: 39625
diff changeset
   110
  private val include_pos =
wenzelm
parents: 39625
diff changeset
   111
    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   112
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   113
  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
   114
  {
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   115
    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
   116
      tree match {
39172
31b95e0da7b7 Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents: 39170
diff changeset
   117
        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
31b95e0da7b7 Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents: 39170
diff changeset
   118
        if include_pos(name) && id == command.id =>
31b95e0da7b7 Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents: 39170
diff changeset
   119
          val range = command.decode(raw_range).restrict(command.range)
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   120
          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   121
        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
39042
470fd769ae53 Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents: 38887
diff changeset
   122
        case _ => set
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
   123
      }
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   124
    val set = positions(Set.empty, message)
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   125
    if (set.isEmpty && !is_state(message))
39172
31b95e0da7b7 Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents: 39170
diff changeset
   126
      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
39042
470fd769ae53 Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents: 38887
diff changeset
   127
    else set
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38581
diff changeset
   128
  }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   129
}
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   130
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   131
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   132
trait Isar_Document extends Isabelle_Process
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   133
{
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   134
  /* commands */
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   135
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   136
  def define_command(id: Document.Command_ID, text: String): Unit =
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
   137
    input("Isar_Document.define_command", Document.ID(id), text)
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   138
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   139
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   140
  /* document versions */
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   141
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   142
  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   143
    edits: List[Document.Edit_Command_ID])
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   144
  {
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   145
    val edits_yxml =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43748
diff changeset
   146
    { import XML.Encode._
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43767
diff changeset
   147
      def encode: T[List[Document.Edit_Command_ID]] =
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43767
diff changeset
   148
        list(pair(string,
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43767
diff changeset
   149
          variant(List(
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43767
diff changeset
   150
            { case Document.Node.Remove() => (Nil, Nil) },
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   151
            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   152
            { case Document.Node.Update_Header(
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44158
diff changeset
   153
                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   154
                (Nil, triple(string, list(string), list(string))(a, b, c)) },
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   155
            { case Document.Node.Update_Header(
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 44157
diff changeset
   156
                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   157
      YXML.string_of_body(encode(edits)) }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   158
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   159
    input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   160
  }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   161
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   162
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   163
  /* method invocation service */
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   164
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   165
  def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   166
  {
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   167
    input("Isar_Document.invoke_scala", id, tag.toString, res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   168
  }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   169
}