src/Pure/PIDE/protocol.scala
author wenzelm
Wed, 04 Apr 2012 14:19:47 +0200
changeset 47336 bed4b2738d8a
parent 46938 cda018294515
child 47343 b8aeab386414
permissions -rw-r--r--
separate module for prover command execution;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
     1
/*  Title:      Pure/PIDE/protocol.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
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
     4
Protocol message formats for interactive proof 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
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
    10
object Protocol
38412
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
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44474
diff changeset
    14
  object Assign
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44474
diff changeset
    15
  {
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    16
    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    17
      try {
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    18
        import XML.Decode._
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    19
        val body = YXML.parse_body(text)
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    20
        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    21
      }
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    22
      catch {
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    23
        case ERROR(_) => None
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    24
        case _: XML.XML_Atom => None
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
    25
        case _: XML.XML_Body => None
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    26
      }
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    27
  }
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    28
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    29
  object Removed
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    30
  {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    31
    def unapply(text: String): Option[List[Document.Version_ID]] =
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    32
      try {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    33
        import XML.Decode._
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    34
        Some(list(long)(YXML.parse_body(text)))
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    35
      }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    36
      catch {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    37
        case ERROR(_) => None
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    38
        case _: XML.XML_Atom => None
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    39
        case _: XML.XML_Body => None
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    40
      }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    41
  }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    42
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    43
46209
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
    44
  /* command status */
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    45
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    46
  object Status
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    47
  {
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    48
    val init = Status()
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    49
  }
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    50
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    51
  sealed case class Status(
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46812
diff changeset
    52
    private val parsed: Boolean = false,
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    53
    private val finished: Boolean = false,
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    54
    private val failed: Boolean = false,
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    55
    forks: Int = 0)
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    56
  {
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46812
diff changeset
    57
    def is_unprocessed: Boolean = parsed && !finished && !failed && forks == 0
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    58
    def is_running: Boolean = forks != 0
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    59
    def is_finished: Boolean = finished && forks == 0
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    60
    def is_failed: Boolean = failed && forks == 0
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    61
    def + (that: Status): Status =
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46812
diff changeset
    62
      Status(parsed || that.parsed, finished || that.finished,
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46812
diff changeset
    63
        failed || that.failed, forks + that.forks)
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    64
  }
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    65
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    66
  val command_status_markup: Set[String] =
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46812
diff changeset
    67
    Set(Isabelle_Markup.PARSED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    68
      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    69
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    70
  def command_status(status: Status, markup: Markup): Status =
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    71
    markup match {
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46812
diff changeset
    72
      case Markup(Isabelle_Markup.PARSED, _) => status.copy(parsed = true)
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    73
      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    74
      case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    75
      case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    76
      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    77
      case _ => status
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    78
    }
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    79
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    80
  def command_status(markups: List[Markup]): Status =
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46209
diff changeset
    81
    (Status.init /: markups)(command_status(_, _))
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
    82
46209
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
    83
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
    84
  /* node status */
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
    85
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
    86
  sealed case class Node_Status(
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
    87
    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44676
diff changeset
    88
  {
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
    89
    def total: Int = unprocessed + running + finished + warned + failed
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44676
diff changeset
    90
  }
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    91
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    92
  def node_status(
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    93
    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    94
  {
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    95
    var unprocessed = 0
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    96
    var running = 0
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    97
    var finished = 0
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
    98
    var warned = 0
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
    99
    var failed = 0
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   100
    node.commands.foreach(command =>
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
   101
      {
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   102
        val st = state.command_state(version, command)
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   103
        val status = command_status(st.status)
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
   104
        if (status.is_running) running += 1
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   105
        else if (status.is_finished) {
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   106
          if (st.results.exists(p => is_warning(p._2))) warned += 1
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   107
          else finished += 1
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   108
        }
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
   109
        else if (status.is_failed) failed += 1
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
   110
        else unprocessed += 1
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   111
      })
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   112
    Node_Status(unprocessed, running, finished, warned, failed)
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   113
  }
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   114
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
   115
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   116
  /* 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
   117
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
   118
  def clean_message(body: XML.Body): XML.Body =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   119
    body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
   120
      { 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
   121
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   122
  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
   123
    msg match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   124
      case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem)
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   125
      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
   126
      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
   127
    }
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   128
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
   129
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   130
  /* specific messages */
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   131
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39622
diff changeset
   132
 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
   133
    msg match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   134
      case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
   135
      case _ => false
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
   136
    }
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
   137
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   138
  def is_warning(msg: XML.Tree): Boolean =
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   139
    msg match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   140
      case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   141
      case _ => false
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   142
    }
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   143
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   144
  def is_error(msg: XML.Tree): Boolean =
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   145
    msg match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   146
      case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   147
      case _ => false
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   148
    }
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
   149
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   150
  def is_state(msg: XML.Tree): Boolean =
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   151
    msg match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   152
      case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   153
        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   154
      case _ => false
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   155
    }
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   156
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   157
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   158
  /* reported positions */
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   159
39627
wenzelm
parents: 39625
diff changeset
   160
  private val include_pos =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   161
    Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44979
diff changeset
   162
      Isabelle_Markup.POSITION)
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   163
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   164
  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
   165
  {
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   166
    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
   167
      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
   168
        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
   169
        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
   170
          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
   171
          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
   172
        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
   173
        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
   174
      }
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   175
    val set = positions(Set.empty, message)
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   176
    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
   177
      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
   178
    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
   179
  }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   180
}
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   181
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   182
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   183
trait Protocol extends Isabelle_Process
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   184
{
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   185
  /* commands */
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   186
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44615
diff changeset
   187
  def define_command(command: Command): Unit =
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   188
    input("Document.define_command",
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44615
diff changeset
   189
      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   190
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   191
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   192
  /* document versions */
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   193
44612
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44481
diff changeset
   194
  def cancel_execution()
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44481
diff changeset
   195
  {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   196
    input("Document.cancel_execution")
44612
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44481
diff changeset
   197
  }
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44481
diff changeset
   198
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   199
  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   200
    name: Document.Node.Name, perspective: Command.Perspective)
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   201
  {
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   202
    val ids =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   203
    { import XML.Encode._
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44436
diff changeset
   204
      list(long)(perspective.commands.map(_.id)) }
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   205
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   206
    input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   207
      name.node, YXML.string_of_body(ids))
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   208
  }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44384
diff changeset
   209
44481
bb42bc831570 tuned signature;
wenzelm
parents: 44479
diff changeset
   210
  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44185
diff changeset
   211
    edits: List[Document.Edit_Command])
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   212
  {
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   213
    val edits_yxml =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43748
diff changeset
   214
    { import XML.Encode._
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44185
diff changeset
   215
      def id: T[Command] = (cmd => long(cmd.id))
46770
44c28a33c461 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents: 46755
diff changeset
   216
      def symbol_string: T[String] = (s => string(Symbol.encode(s)))
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46688
diff changeset
   217
      def encode_edit(name: Document.Node.Name)
44979
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   218
          : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   219
        variant(List(
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   220
          { case Document.Node.Clear() => (Nil, Nil) },
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   221
          { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46688
diff changeset
   222
          { case Document.Node.Header(Exn.Res(deps)) =>
46770
44c28a33c461 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents: 46755
diff changeset
   223
              val dir = Isabelle_System.posix_path(name.dir)
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46688
diff changeset
   224
              val imports = deps.imports.map(_.node)
46770
44c28a33c461 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents: 46755
diff changeset
   225
              // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
44c28a33c461 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents: 46755
diff changeset
   226
              val uses = deps.uses
44979
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   227
              (Nil,
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46910
diff changeset
   228
                pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46910
diff changeset
   229
                  list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46910
diff changeset
   230
                    list(pair(symbol_string, bool)))(
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46910
diff changeset
   231
                (((dir, name.theory), imports), deps.keywords), uses)) },
46755
f676b5ade7d7 Symbol.encode header edits;
wenzelm
parents: 46737
diff changeset
   232
          { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
44979
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   233
          { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   234
      def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   235
      {
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   236
        val (name, edit) = node_edit
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46688
diff changeset
   237
        pair(string, encode_edit(name))(name.node, edit)
44979
68b990e950b1 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents: 44866
diff changeset
   238
      })
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   239
      YXML.string_of_body(encode(edits)) }
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   240
    input("Document.update", 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
   241
  }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   242
44673
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   243
  def remove_versions(versions: List[Document.Version])
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   244
  {
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   245
    val versions_yxml =
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   246
      { import XML.Encode._
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   247
        YXML.string_of_body(list(long)(versions.map(_.id))) }
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   248
    input("Document.remove_versions", versions_yxml)
44673
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   249
  }
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   250
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   251
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   252
  /* method invocation service */
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   253
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   254
  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
   255
  {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   256
    input("Document.invoke_scala", id, tag.toString, res)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   257
  }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   258
}