src/Pure/PIDE/protocol.scala
author wenzelm
Mon, 07 Apr 2014 13:55:12 +0200
changeset 56449 f0592485b7fb
parent 56447 1e77ed11f2f7
child 56458 a8d960baa5c2
permissions -rw-r--r--
support for URL as file name, similar to treatment in jEdit.java;
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
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
    14
  object Assign_Update
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44474
diff changeset
    15
  {
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
    16
    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
44661
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)
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52111
diff changeset
    20
        Some(pair(long, list(pair(long, list(long))))(body))
44661
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
51987
7d8e0e3c553b tuned signature;
wenzelm
parents: 51818
diff changeset
    24
        case _: XML.Error => None
38412
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
  }
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    27
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    28
  object Removed
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    29
  {
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
    30
    def unapply(text: String): Option[List[Document_ID.Version]] =
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    31
      try {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    32
        import XML.Decode._
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    33
        Some(list(long)(YXML.parse_body(text)))
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    34
      }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    35
      catch {
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    36
        case ERROR(_) => None
51987
7d8e0e3c553b tuned signature;
wenzelm
parents: 51818
diff changeset
    37
        case _: XML.Error => None
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    38
      }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    39
  }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44673
diff changeset
    40
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    41
46209
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
    42
  /* command status */
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    43
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    44
  object Status
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    45
  {
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    46
    def make(markup_iterator: Iterator[Markup]): Status =
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    47
    {
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    48
      var touched = false
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    49
      var accepted = false
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    50
      var warned = false
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    51
      var failed = false
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    52
      var forks = 0
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    53
      var runs = 0
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    54
      for (markup <- markup_iterator) {
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    55
        markup.name match {
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    56
          case Markup.ACCEPTED => accepted = true
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    57
          case Markup.FORKED => touched = true; forks += 1
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    58
          case Markup.JOINED => forks -= 1
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    59
          case Markup.RUNNING => touched = true; runs += 1
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    60
          case Markup.FINISHED => runs -= 1
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    61
          case Markup.WARNING => warned = true
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    62
          case Markup.FAILED | Markup.ERROR => failed = true
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    63
          case _ =>
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    64
        }
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    65
      }
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    66
      Status(touched, accepted, warned, failed, forks, runs)
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    67
    }
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    68
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    69
    val empty = make(Iterator.empty)
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    70
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    71
    def merge(status_iterator: Iterator[Status]): Status =
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    72
      if (status_iterator.hasNext) {
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    73
        val status0 = status_iterator.next
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    74
        (status0 /: status_iterator)(_ + _)
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    75
      }
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    76
      else empty
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    77
  }
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    78
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
    79
  sealed case class Status(
56352
abdc524db8b4 more frugal command_status, which is often used in a tight loop;
wenzelm
parents: 56335
diff changeset
    80
    private val touched: Boolean,
abdc524db8b4 more frugal command_status, which is often used in a tight loop;
wenzelm
parents: 56335
diff changeset
    81
    private val accepted: Boolean,
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    82
    private val warned: Boolean,
56352
abdc524db8b4 more frugal command_status, which is often used in a tight loop;
wenzelm
parents: 56335
diff changeset
    83
    private val failed: Boolean,
abdc524db8b4 more frugal command_status, which is often used in a tight loop;
wenzelm
parents: 56335
diff changeset
    84
    forks: Int,
abdc524db8b4 more frugal command_status, which is often used in a tight loop;
wenzelm
parents: 56335
diff changeset
    85
    runs: Int)
38567
b670faa807c9 concentrate protocol message formats in Isar_Document;
wenzelm
parents: 38483
diff changeset
    86
  {
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    87
    def + (that: Status): Status =
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    88
      Status(
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    89
        touched || that.touched,
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    90
        accepted || that.accepted,
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    91
        warned || that.warned,
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    92
        failed || that.failed,
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    93
        forks + that.forks,
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    94
        runs + that.runs)
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
    95
49036
4680c4046814 further refinement of command status, to accomodate forked proofs;
wenzelm
parents: 49009
diff changeset
    96
    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
4680c4046814 further refinement of command status, to accomodate forked proofs;
wenzelm
parents: 49009
diff changeset
    97
    def is_running: Boolean = runs != 0
49039
e780d1bf767e clarified command status (again);
wenzelm
parents: 49036
diff changeset
    98
    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
    99
    def is_warned: Boolean = is_finished && warned
49036
4680c4046814 further refinement of command status, to accomodate forked proofs;
wenzelm
parents: 49009
diff changeset
   100
    def is_failed: Boolean = failed
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
   101
  }
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 46121
diff changeset
   102
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
   103
  val proper_status_elements =
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55783
diff changeset
   104
    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
55646
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   105
      Markup.FINISHED, Markup.FAILED)
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   106
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
   107
  val liberal_status_elements =
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
   108
    proper_status_elements + Markup.WARNING + Markup.ERROR
55646
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   109
46209
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
   110
51818
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   111
  /* command timing */
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   112
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   113
  object Command_Timing
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   114
  {
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
   115
    def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
51818
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   116
      props match {
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   117
        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   118
          (args, args) match {
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   119
            case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   120
            case _ => None
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   121
          }
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   122
        case _ => None
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   123
      }
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   124
  }
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   125
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51533
diff changeset
   126
46209
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
   127
  /* node status */
aad604f74be0 tuned comments;
wenzelm
parents: 46207
diff changeset
   128
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   129
  sealed case class Node_Status(
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   130
    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44676
diff changeset
   131
  {
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   132
    def total: Int = unprocessed + running + finished + warned + failed
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44676
diff changeset
   133
  }
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   134
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   135
  def node_status(
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   136
    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   137
  {
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   138
    var unprocessed = 0
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   139
    var running = 0
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   140
    var finished = 0
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   141
    var warned = 0
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   142
    var failed = 0
56356
c3dbaa155ece tuned for-comprehensions -- less structure mapping;
wenzelm
parents: 56355
diff changeset
   143
    for (command <- node.commands.iterator) {
56355
1a9f569b5b7e some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
wenzelm
parents: 56353
diff changeset
   144
      val states = state.command_states(version, command)
56359
bca016a9a18d persistent protocol_status, to improve performance of node_status a little;
wenzelm
parents: 56356
diff changeset
   145
      val status = Status.merge(states.iterator.map(_.protocol_status))
56355
1a9f569b5b7e some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
wenzelm
parents: 56353
diff changeset
   146
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   147
      if (status.is_running) running += 1
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
   148
      else if (status.is_warned) warned += 1
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56387
diff changeset
   149
      else if (status.is_finished) finished += 1
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   150
      else if (status.is_failed) failed += 1
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   151
      else unprocessed += 1
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   152
    }
46688
134982ee4ecb include warning messages in node status;
wenzelm
parents: 46227
diff changeset
   153
    Node_Status(unprocessed, running, finished, warned, failed)
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   154
  }
a3255c85327b crude display of node status;
wenzelm
parents: 44612
diff changeset
   155
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
   156
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   157
  /* node timing */
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   158
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   159
  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   160
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   161
  val empty_node_timing = Node_Timing(0.0, Map.empty)
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   162
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   163
  def node_timing(
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   164
    state: Document.State,
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   165
    version: Document.Version,
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   166
    node: Document.Node,
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   167
    threshold: Double): Node_Timing =
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   168
  {
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   169
    var total = 0.0
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   170
    var commands = Map.empty[Command, Double]
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   171
    for {
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   172
      command <- node.commands.iterator
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   173
      st <- state.command_states(version, command)
56356
c3dbaa155ece tuned for-comprehensions -- less structure mapping;
wenzelm
parents: 56355
diff changeset
   174
    } {
c3dbaa155ece tuned for-comprehensions -- less structure mapping;
wenzelm
parents: 56355
diff changeset
   175
      val command_timing =
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   176
        (0.0 /: st.status)({
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   177
          case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   178
          case (timing, _) => timing
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   179
        })
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   180
      total += command_timing
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   181
      if (command_timing >= threshold) commands += (command -> command_timing)
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   182
    }
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   183
    Node_Timing(total, commands)
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   184
  }
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   185
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51294
diff changeset
   186
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   187
  /* 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
   188
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55783
diff changeset
   189
  private val clean_elements =
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55783
diff changeset
   190
    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50201
diff changeset
   191
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
   192
  def clean_message(body: XML.Body): XML.Body =
49445
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   193
    body filter {
55646
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   194
      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   195
      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
49445
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   196
      case _ => true
49650
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49648
diff changeset
   197
    } map {
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49648
diff changeset
   198
      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49648
diff changeset
   199
      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49648
diff changeset
   200
      case t => t
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49648
diff changeset
   201
    }
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
   202
49445
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   203
  def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   204
    body flatMap {
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50201
diff changeset
   205
      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50201
diff changeset
   206
        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   207
      case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   208
        List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
49650
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49648
diff changeset
   209
      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
49445
638cefe3ee99 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents: 49418
diff changeset
   210
      case XML.Elem(_, ts) => message_reports(props, ts)
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   211
      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
   212
    }
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   213
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39181
diff changeset
   214
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   215
  /* specific messages */
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   216
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   217
  def is_inlined(msg: XML.Tree): Boolean =
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   218
    !(is_result(msg) || is_tracing(msg) || is_state(msg))
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   219
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   220
  def is_result(msg: XML.Tree): Boolean =
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   221
    msg match {
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   222
      case XML.Elem(Markup(Markup.RESULT, _), _) => true
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   223
      case _ => false
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   224
    }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   225
50157
76efdb6daab2 tuned whitespace;
wenzelm
parents: 50128
diff changeset
   226
  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
   227
    msg match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   228
      case XML.Elem(Markup(Markup.TRACING, _), _) => true
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   229
      case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
   230
      case _ => false
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
   231
    }
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39511
diff changeset
   232
52650
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52582
diff changeset
   233
  def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   234
    msg match {
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   235
      case XML.Elem(Markup(Markup.WRITELN, _),
52650
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52582
diff changeset
   236
        List(XML.Elem(markup, _))) => markup.name == name
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   237
      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
52650
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52582
diff changeset
   238
        List(XML.Elem(markup, _))) => markup.name == name
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   239
      case _ => false
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   240
    }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   241
52650
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52582
diff changeset
   242
  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52582
diff changeset
   243
  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52582
diff changeset
   244
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   245
  def is_warning(msg: XML.Tree): Boolean =
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   246
    msg match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   247
      case XML.Elem(Markup(Markup.WARNING, _), _) => true
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   248
      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   249
      case _ => false
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   250
    }
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   251
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   252
  def is_error(msg: XML.Tree): Boolean =
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   253
    msg match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   254
      case XML.Elem(Markup(Markup.ERROR, _), _) => true
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50157
diff changeset
   255
      case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   256
      case _ => false
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   257
    }
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
   258
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   259
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   260
  /* dialogs */
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   261
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   262
  object Dialog_Args
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   263
  {
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
   264
    def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   265
      (props, props, props) match {
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   266
        case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   267
          Some((id, serial, result))
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   268
        case _ => None
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   269
      }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   270
  }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   271
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   272
  object Dialog
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   273
  {
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
   274
    def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   275
      tree match {
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   276
        case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   277
          Some((id, serial, result))
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   278
        case _ => None
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   279
      }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   280
  }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   281
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   282
  object Dialog_Result
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   283
  {
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
   284
    def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   285
    {
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   286
      val props = Position.Id(id) ::: Markup.Serial(serial)
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   287
      XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   288
    }
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   289
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   290
    def unapply(tree: XML.Tree): Option[String] =
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   291
      tree match {
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   292
        case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   293
        case _ => None
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   294
      }
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
   295
  }
39170
04ad0fed81f5 Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents: 39042
diff changeset
   296
39511
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   297
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   298
  /* reported positions */
5f318522e6fe some specific message classification;
wenzelm
parents: 39441
diff changeset
   299
55646
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   300
  private val position_elements =
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55783
diff changeset
   301
    Document.Elements(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
   302
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   303
  def message_positions(
56295
a40e67ce4f84 clarified valid_id: always standardize towards static command.id;
wenzelm
parents: 55884
diff changeset
   304
    valid_id: Document_ID.Generic => Boolean,
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   305
    chunk: Command.Chunk,
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   306
    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
   307
  {
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   308
    def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   309
      props match {
55884
f2c0eaedd579 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents: 55822
diff changeset
   310
        case Position.Reported(id, file_name, symbol_range)
56295
a40e67ce4f84 clarified valid_id: always standardize towards static command.id;
wenzelm
parents: 55884
diff changeset
   311
        if valid_id(id) && file_name == chunk.file_name =>
55884
f2c0eaedd579 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents: 55822
diff changeset
   312
          chunk.incorporate(symbol_range) match {
55822
ccf2d784be97 incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents: 55820
diff changeset
   313
            case Some(range) => set + range
55548
a645277885cf more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
wenzelm
parents: 55433
diff changeset
   314
            case _ => set
a645277885cf more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
wenzelm
parents: 55433
diff changeset
   315
          }
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   316
        case _ => set
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   317
      }
50157
76efdb6daab2 tuned whitespace;
wenzelm
parents: 50128
diff changeset
   318
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   319
    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
   320
      tree match {
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   321
        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
55646
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   322
          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   323
        case XML.Elem(Markup(name, props), body) =>
55646
ec4651c697e3 tuned signature;
wenzelm
parents: 55548
diff changeset
   324
          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   325
        case XML.Text(_) => 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
   326
      }
50157
76efdb6daab2 tuned whitespace;
wenzelm
parents: 50128
diff changeset
   327
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39439
diff changeset
   328
    val set = positions(Set.empty, message)
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   329
    if (set.isEmpty) elem_positions(message.markup.properties, set)
39042
470fd769ae53 Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents: 38887
diff changeset
   330
    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
   331
  }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   332
}
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   333
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   334
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   335
trait Protocol extends Prover
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   336
{
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   337
  /* options */
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   338
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   339
  def options(opts: Options): Unit =
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   340
    protocol_command("Prover.options", YXML.string_of_body(opts.encode))
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   341
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   342
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   343
  /* interned items */
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   344
56335
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56306
diff changeset
   345
  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56372
diff changeset
   346
    protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   347
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44615
diff changeset
   348
  def define_command(command: Command): Unit =
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   349
  {
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   350
    val blobs_yxml =
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   351
    { import XML.Encode._
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   352
      val encode_blob: T[Command.Blob] =
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   353
        variant(List(
54526
92961f196d9e load files that are not provided by PIDE blobs;
wenzelm
parents: 54524
diff changeset
   354
          { case Exn.Res((a, b)) =>
56447
1e77ed11f2f7 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents: 56395
diff changeset
   355
              (Nil, triple(string, string, option(string))(
56449
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56447
diff changeset
   356
                (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
54526
92961f196d9e load files that are not provided by PIDE blobs;
wenzelm
parents: 54524
diff changeset
   357
          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   358
      YXML.string_of_body(list(encode_blob)(command.blobs))
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   359
    }
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52563
diff changeset
   360
    protocol_command("Document.define_command",
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   361
      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   362
  }
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   363
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   364
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   365
  /* execution */
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   366
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   367
  def discontinue_execution(): Unit =
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   368
    protocol_command("Document.discontinue_execution")
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   369
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   370
  def cancel_exec(id: Document_ID.Exec): Unit =
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   371
    protocol_command("Document.cancel_exec", Document_ID(id))
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   372
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   373
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   374
  /* document versions */
47343
b8aeab386414 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents: 46938
diff changeset
   375
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   376
  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44185
diff changeset
   377
    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
   378
  {
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   379
    val edits_yxml =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43748
diff changeset
   380
    { import XML.Encode._
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44185
diff changeset
   381
      def id: T[Command] = (cmd => long(cmd.id))
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46688
diff changeset
   382
      def encode_edit(name: Document.Node.Name)
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   383
          : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
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
   384
        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
   385
          { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48705
diff changeset
   386
          { case Document.Node.Deps(header) =>
56449
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56447
diff changeset
   387
              val master_dir = Isabelle_System.posix_path_url(name.master_dir)
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48705
diff changeset
   388
              val imports = header.imports.map(_.node)
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 49650
diff changeset
   389
              val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
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
   390
              (Nil,
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48705
diff changeset
   391
                pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48755
diff changeset
   392
                  pair(list(pair(Encode.string,
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48755
diff changeset
   393
                    option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
   394
                  list(Encode.string)))))(
54515
570ba266f5b5 clarified boundary cases of Document.Node.Name;
wenzelm
parents: 54509
diff changeset
   395
                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   396
          { case Document.Node.Perspective(a, b, c) =>
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   397
              (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
52862
930ce8eacb87 tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents: 52849
diff changeset
   398
                list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 47542
diff changeset
   399
      def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
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
   400
      {
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
   401
        val (name, edit) = node_edit
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46688
diff changeset
   402
        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
   403
      })
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 47542
diff changeset
   404
      YXML.string_of_body(encode_edits(edits)) }
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52563
diff changeset
   405
    protocol_command("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
   406
  }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   407
44673
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   408
  def remove_versions(versions: List[Document.Version])
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   409
  {
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   410
    val versions_yxml =
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   411
      { import XML.Encode._
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   412
        YXML.string_of_body(list(long)(versions.map(_.id))) }
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52563
diff changeset
   413
    protocol_command("Document.remove_versions", versions_yxml)
44673
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   414
  }
2fa51ac191bc Document.remove_versions on ML side;
wenzelm
parents: 44661
diff changeset
   415
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43731
diff changeset
   416
50498
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
   417
  /* dialog via document content */
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
   418
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52862
diff changeset
   419
  def dialog_result(serial: Long, result: String): Unit =
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52563
diff changeset
   420
    protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   421
}