src/Pure/PIDE/command.scala
author wenzelm
Sun, 29 Nov 2020 15:33:19 +0100
changeset 72774 51c0f79d6eed
parent 72772 a9ef39041114
child 72775 0a94eb91190d
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     1
/*  Title:      Pure/PIDE/command.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     2
    Author:     Fabian Immler, TU Munich
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     4
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
     5
Prover commands with accumulated results from execution.
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     6
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     7
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34865
diff changeset
     8
package isabelle
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    10
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    11
import scala.collection.mutable
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    12
import scala.collection.immutable.SortedMap
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    13
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    14
34637
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    15
object Command
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    16
{
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52642
diff changeset
    17
  type Edit = (Option[Command], Option[Command])
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
    18
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
    19
  sealed case class Blob(
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
    20
    name: Document.Node.Name,
72747
5f9d66155081 clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents: 72745
diff changeset
    21
    src_path: Path,
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
    22
    content: Option[(SHA1.Digest, Symbol.Text_Chunk)])
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
    23
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
    24
  type Blobs_Info = (List[Exn.Result[Blob]], Int)
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
    25
  val no_blobs: Blobs_Info = (Nil, -1)
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52642
diff changeset
    26
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52642
diff changeset
    27
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    28
  /** accumulated results from prover **/
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    29
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    30
  /* results */
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    31
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    32
  object Results
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    33
  {
51496
cb677987b7e3 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents: 51494
diff changeset
    34
    type Entry = (Long, XML.Tree)
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    35
    val empty: Results = new Results(SortedMap.empty)
59072
27c6936c6484 tuned signature;
wenzelm
parents: 57912
diff changeset
    36
    def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
27c6936c6484 tuned signature;
wenzelm
parents: 57912
diff changeset
    37
    def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    38
  }
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    39
51494
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    40
  final class Results private(private val rep: SortedMap[Long, XML.Tree])
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    41
  {
64802
adc4c84b692c suppress empty results;
wenzelm
parents: 64471
diff changeset
    42
    def is_empty: Boolean = rep.isEmpty
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    43
    def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    44
    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56359
diff changeset
    45
    def iterator: Iterator[Results.Entry] = rep.iterator
50508
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    46
51496
cb677987b7e3 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents: 51494
diff changeset
    47
    def + (entry: Results.Entry): Results =
50508
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    48
      if (defined(entry._1)) this
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    49
      else new Results(rep + entry)
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    50
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    51
    def ++ (other: Results): Results =
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    52
      if (this eq other) this
5b7150395568 tuned implementation according to Library.insert/merge in ML;
wenzelm
parents: 50507
diff changeset
    53
      else if (rep.isEmpty) other
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56359
diff changeset
    54
      else (this /: other.iterator)(_ + _)
50540
wenzelm
parents: 50508
diff changeset
    55
51494
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    56
    override def hashCode: Int = rep.hashCode
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    57
    override def equals(that: Any): Boolean =
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    58
      that match {
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    59
        case other: Results => rep == other.rep
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    60
        case _ => false
8f3d1a7bee26 structural equality for Command.Results;
wenzelm
parents: 51048
diff changeset
    61
      }
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56359
diff changeset
    62
    override def toString: String = iterator.mkString("Results(", ", ", ")")
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    63
  }
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    64
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    65
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    66
  /* exports */
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    67
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    68
  object Exports
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    69
  {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    70
    type Entry = (Long, Export.Entry)
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    71
    val empty: Exports = new Exports(SortedMap.empty)
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    72
    def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    73
  }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    74
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    75
  final class Exports private(private val rep: SortedMap[Long, Export.Entry])
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    76
  {
69634
70f1994988d4 more operations;
wenzelm
parents: 68758
diff changeset
    77
    def is_empty: Boolean = rep.isEmpty
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    78
    def iterator: Iterator[Exports.Entry] = rep.iterator
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    79
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    80
    def + (entry: Exports.Entry): Exports =
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    81
      if (rep.isDefinedAt(entry._1)) this
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    82
      else new Exports(rep + entry)
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    83
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    84
    def ++ (other: Exports): Exports =
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    85
      if (this eq other) this
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    86
      else if (rep.isEmpty) other
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    87
      else (this /: other.iterator)(_ + _)
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    88
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    89
    override def hashCode: Int = rep.hashCode
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    90
    override def equals(that: Any): Boolean =
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    91
      that match {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    92
        case other: Exports => rep == other.rep
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    93
        case _ => false
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    94
      }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    95
    override def toString: String = iterator.mkString("Exports(", ", ", ")")
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    96
  }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    97
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    98
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
    99
  /* markups */
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   100
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   101
  object Markup_Index
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   102
  {
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   103
    val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   104
  }
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   105
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   106
  sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   107
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   108
  object Markups
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   109
  {
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   110
    val empty: Markups = new Markups(Map.empty)
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   111
    def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   112
    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   113
  }
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   114
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   115
  final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   116
  {
56489
wenzelm
parents: 56476
diff changeset
   117
    def is_empty: Boolean = rep.isEmpty
wenzelm
parents: 56476
diff changeset
   118
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   119
    def apply(index: Markup_Index): Markup_Tree =
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   120
      rep.getOrElse(index, Markup_Tree.empty)
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   121
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   122
    def add(index: Markup_Index, markup: Text.Markup): Markups =
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   123
      new Markups(rep + (index -> (this(index) + markup)))
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   124
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   125
    def + (entry: (Markup_Index, Markup_Tree)): Markups =
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   126
    {
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   127
      val (index, tree) = entry
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   128
      new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   129
    }
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   130
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   131
    def ++ (other: Markups): Markups =
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   132
      if (this eq other) this
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   133
      else if (rep.isEmpty) other
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   134
      else (this /: other.rep.iterator)(_ + _)
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   135
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   136
    def redirection_iterator: Iterator[Document_ID.Generic] =
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   137
      for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   138
        yield id
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   139
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   140
    def redirect(other_id: Document_ID.Generic): Markups =
56489
wenzelm
parents: 56476
diff changeset
   141
    {
wenzelm
parents: 56476
diff changeset
   142
      val rep1 =
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   143
        (for {
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   144
          (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   145
          if other_id == id
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   146
        } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
56489
wenzelm
parents: 56476
diff changeset
   147
      if (rep1.isEmpty) Markups.empty else new Markups(rep1)
wenzelm
parents: 56476
diff changeset
   148
    }
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   149
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   150
    override def hashCode: Int = rep.hashCode
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   151
    override def equals(that: Any): Boolean =
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   152
      that match {
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   153
        case other: Markups => rep == other.rep
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   154
        case _ => false
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   155
      }
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   156
    override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   157
  }
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   158
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   159
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
   160
  /* state */
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   161
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   162
  object State
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   163
  {
67824
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   164
    def get_result(states: List[State], serial: Long): Option[XML.Tree] =
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   165
      states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get)
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   166
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   167
    def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] =
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   168
      for {
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   169
        serial <- Markup.Serial.unapply(props)
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   170
        tree @ XML.Elem(_, body) <- get_result(states, serial)
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   171
        if body.nonEmpty
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   172
      } yield (serial -> tree)
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   173
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   174
    def merge_results(states: List[State]): Results =
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   175
      Results.merge(states.map(_.results))
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   176
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   177
    def merge_exports(states: List[State]): Exports =
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   178
      Exports.merge(states.map(_.exports))
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   179
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   180
    def merge_markups(states: List[State]): Markups =
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   181
      Markups.merge(states.map(_.markups))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   182
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56299
diff changeset
   183
    def merge_markup(states: List[State], index: Markup_Index,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56514
diff changeset
   184
        range: Text.Range, elements: Markup.Elements): Markup_Tree =
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56299
diff changeset
   185
      Markup_Tree.merge(states.map(_.markup(index)), range, elements)
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   186
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   187
    def merge(command: Command, states: List[State]): State =
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   188
      State(command, states.flatMap(_.status), merge_results(states),
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   189
        merge_exports(states), merge_markups(states))
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   190
  }
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56295
diff changeset
   191
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 43662
diff changeset
   192
  sealed case class State(
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   193
    command: Command,
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   194
    status: List[Markup] = Nil,
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
   195
    results: Results = Results.empty,
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   196
    exports: Exports = Exports.empty,
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   197
    markups: Markups = Markups.empty)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   198
  {
68323
bf7336731981 more node status information;
wenzelm
parents: 68306
diff changeset
   199
    def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
70780
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70713
diff changeset
   200
    def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
68335
2f080a51a10d clarified: consolidated result is last command;
wenzelm
parents: 68323
diff changeset
   201
    def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
66379
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 65522
diff changeset
   202
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   203
    lazy val maybe_consolidated: Boolean =
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   204
    {
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   205
      var touched = false
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   206
      var forks = 0
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   207
      var runs = 0
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   208
      for (markup <- status) {
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   209
        markup.name match {
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   210
          case Markup.FORKED => touched = true; forks += 1
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   211
          case Markup.JOINED => forks -= 1
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   212
          case Markup.RUNNING => touched = true; runs += 1
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   213
          case Markup.FINISHED => runs -= 1
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   214
          case _ =>
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   215
        }
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   216
      }
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   217
      touched && forks == 0 && runs == 0
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   218
    }
68381
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68335
diff changeset
   219
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   220
    lazy val document_status: Document_Status.Command_Status =
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   221
    {
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   222
      val warnings =
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59072
diff changeset
   223
        if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   224
          List(Markup(Markup.WARNING, Nil))
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   225
        else Nil
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   226
      val errors =
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   227
        if (results.iterator.exists(p => Protocol.is_error(p._2)))
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   228
          List(Markup(Markup.ERROR, Nil))
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   229
        else Nil
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   230
      Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator)
56395
0546e036d1c0 more direct warning within persistent Protocol.Status;
wenzelm
parents: 56372
diff changeset
   231
    }
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   232
55650
349afd0fa0c4 tuned signature;
wenzelm
parents: 55649
diff changeset
   233
    def markup(index: Markup_Index): Markup_Tree = markups(index)
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   234
56489
wenzelm
parents: 56476
diff changeset
   235
    def redirect(other_command: Command): Option[State] =
wenzelm
parents: 56476
diff changeset
   236
    {
wenzelm
parents: 56476
diff changeset
   237
      val markups1 = markups.redirect(other_command.id)
wenzelm
parents: 56476
diff changeset
   238
      if (markups1.is_empty) None
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   239
      else Some(new State(other_command, markups = markups1))
56489
wenzelm
parents: 56476
diff changeset
   240
    }
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49527
diff changeset
   241
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   242
    private def add_status(st: Markup): State =
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   243
      copy(status = st :: status)
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   244
67826
wenzelm
parents: 67825
diff changeset
   245
    private def add_result(entry: Results.Entry): State =
wenzelm
parents: 67825
diff changeset
   246
      copy(results = results + entry)
wenzelm
parents: 67825
diff changeset
   247
68114
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   248
    def add_export(entry: Exports.Entry): Option[State] =
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   249
      if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   250
      else None
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   251
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   252
    private def add_markup(
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   253
      status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   254
    {
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   255
      val markups1 =
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 68729
diff changeset
   256
        if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56395
diff changeset
   257
          markups.add(Markup_Index(true, chunk_name), m)
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   258
        else markups
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56395
diff changeset
   259
      copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55648
diff changeset
   260
    }
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   261
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   262
    def accumulate(
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   263
        self_id: Document_ID.Generic => Boolean,
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   264
        other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
67825
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67824
diff changeset
   265
        message: XML.Elem,
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67824
diff changeset
   266
        xml_cache: XML.Cache): State =
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   267
      message match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
   268
        case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   269
          if (command.span.is_theory) this
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   270
          else {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   271
            (this /: msgs)((state, msg) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   272
              msg match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   273
                case elem @ XML.Elem(markup, Nil) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   274
                  state.
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   275
                    add_status(markup).
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   276
                    add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   277
                case _ =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   278
                  Output.warning("Ignored status message: " + msg)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   279
                  state
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   280
              })
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   281
          }
38581
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38579
diff changeset
   282
72709
cb9d5af781b4 more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm
parents: 72708
diff changeset
   283
        case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
   284
          (this /: msgs)((state, msg) =>
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   285
            {
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents: 56746
diff changeset
   286
              def bad(): Unit = Output.warning("Ignored report message: " + msg)
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   287
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   288
              msg match {
72709
cb9d5af781b4 more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm
parents: 72708
diff changeset
   289
                case XML.Elem(Markup(name, atts1), args) =>
cb9d5af781b4 more complete report positions, notably for command 'back' (amending eca176f773e0);
wenzelm
parents: 72708
diff changeset
   290
                  val atts = atts1 ::: atts0
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   291
                  command.reported_position(atts) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   292
                    case Some((id, chunk_name)) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   293
                      val target =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   294
                        if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   295
                          Some((chunk_name, command.chunks(chunk_name)))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   296
                        else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   297
                        else None
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   298
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   299
                      (target, atts) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   300
                        case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   301
                          target_chunk.incorporate(symbol_range) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   302
                            case Some(range) =>
72708
0cc96d337e8f tuned signature;
wenzelm
parents: 72704
diff changeset
   303
                              val props = atts.filterNot(Markup.position_property)
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   304
                              val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   305
                              state.add_markup(false, target_name, Text.Info(range, elem))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   306
                            case None => bad(); state
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   307
                          }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   308
                        case _ =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   309
                          // silently ignore excessive reports
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   310
                          state
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   311
                      }
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   312
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   313
                    case _ => bad(); state
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   314
                  }
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56469
diff changeset
   315
                case _ => bad(); state
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   316
              }
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   317
            })
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   318
52930
5fab62ae3532 retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents: 52849
diff changeset
   319
        case XML.Elem(Markup(name, props), body) =>
5fab62ae3532 retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents: 52849
diff changeset
   320
          props match {
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50163
diff changeset
   321
            case Markup.Serial(i) =>
67825
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67824
diff changeset
   322
              val markup_message =
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67824
diff changeset
   323
                xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67824
diff changeset
   324
              val message_markup =
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67824
diff changeset
   325
                xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50158
diff changeset
   326
67826
wenzelm
parents: 67825
diff changeset
   327
              var st = add_result(i -> markup_message)
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   328
              if (Protocol.is_inlined(message)) {
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   329
                for {
56469
ffc94a271633 avoid data redundancy;
wenzelm
parents: 56468
diff changeset
   330
                  (chunk_name, chunk) <- command.chunks.iterator
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   331
                  range <- command.message_positions(self_id, chunk_name, chunk, message)
67824
661cd25304ae more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
wenzelm
parents: 67446
diff changeset
   332
                } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup))
55433
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   333
              }
d2960d67f163 clarified message_positions: cover alt_id as well;
wenzelm
parents: 55432
diff changeset
   334
              st
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   335
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
   336
            case _ =>
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents: 56746
diff changeset
   337
              Output.warning("Ignored message without serial number: " + message)
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
   338
              this
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
   339
          }
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 67826
diff changeset
   340
      }
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   341
  }
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
   342
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
   343
55431
e0f20a44ff9d common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents: 55430
diff changeset
   344
e0f20a44ff9d common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents: 55430
diff changeset
   345
  /** static content **/
e0f20a44ff9d common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents: 55430
diff changeset
   346
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   347
  /* make commands */
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   348
55648
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   349
  def apply(
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   350
    id: Document_ID.Command,
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   351
    node_name: Document.Node.Name,
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   352
    blobs_info: Blobs_Info,
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57904
diff changeset
   353
    span: Command_Span.Span): Command =
55648
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   354
  {
57901
e1abca2527da more explicit type Span in Scala, according to ML version;
wenzelm
parents: 57842
diff changeset
   355
    val (source, span1) = span.compact_source
72722
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   356
    new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty)
55648
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   357
  }
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   358
57901
e1abca2527da more explicit type Span in Scala, according to ML version;
wenzelm
parents: 57842
diff changeset
   359
  val empty: Command =
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   360
    Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
55648
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   361
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   362
  def unparsed(
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   363
    source: String,
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   364
    theory: Boolean = false,
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   365
    id: Document_ID.Command = Document_ID.none,
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   366
    node_name: Document.Node.Name = Document.Node.Name.empty,
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   367
    results: Results = Results.empty,
72722
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   368
    markups: Markups = Markups.empty): Command =
55648
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   369
  {
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   370
    val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
72722
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   371
    new Command(id, node_name, no_blobs, span1, source1, results, markups)
55648
38f264741609 tuned signature -- avoid obscure default arguments;
wenzelm
parents: 55622
diff changeset
   372
  }
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   373
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   374
  def text(source: String): Command = unparsed(source)
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
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 rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
72722
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   377
    unparsed(XML.content(body), id = id, results = results,
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   378
      markups = Markups.init(Markup_Tree.from_XML(body)))
49359
c1262d7389fb refined output panel: more value-oriented approach to update and caret focus;
wenzelm
parents: 49037
diff changeset
   379
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   380
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   381
  /* perspective */
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   382
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   383
  object Perspective
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   384
  {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   385
    val empty: Perspective = Perspective(Nil)
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   386
  }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   387
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   388
  sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   389
  {
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 56782
diff changeset
   390
    def is_empty: Boolean = commands.isEmpty
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 56782
diff changeset
   391
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   392
    def same(that: Perspective): Boolean =
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   393
    {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   394
      val cmds1 = this.commands
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   395
      val cmds2 = that.commands
48754
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   396
      require(!cmds1.exists(_.is_undefined))
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48745
diff changeset
   397
      require(!cmds2.exists(_.is_undefined))
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   398
      cmds1.length == cmds2.length &&
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   399
        (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   400
    }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   401
  }
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59684
diff changeset
   402
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59684
diff changeset
   403
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   404
  /* blobs: inlined errors and auxiliary files */
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59684
diff changeset
   405
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   406
  def blobs_info(
59699
wenzelm
parents: 59698
diff changeset
   407
    resources: Resources,
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 62969
diff changeset
   408
    syntax: Outer_Syntax,
59699
wenzelm
parents: 59698
diff changeset
   409
    get_blob: Document.Node.Name => Option[Document.Blob],
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   410
    can_import: Document.Node.Name => Boolean,
59699
wenzelm
parents: 59698
diff changeset
   411
    node_name: Document.Node.Name,
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   412
    span: Command_Span.Span): Blobs_Info =
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59684
diff changeset
   413
  {
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59715
diff changeset
   414
    span.name match {
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   415
      // inlined errors
59735
24bee1b11fce misc tuning and simplification;
wenzelm
parents: 59715
diff changeset
   416
      case Thy_Header.THEORY =>
64825
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   417
        val reader = Scan.char_reader(Token.implode(span.content))
72772
a9ef39041114 clarified signature;
wenzelm
parents: 72765
diff changeset
   418
        val header = resources.check_thy(node_name, reader)
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72747
diff changeset
   419
        val imports_pos = header.imports_pos
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66379
diff changeset
   420
        val raw_imports =
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66379
diff changeset
   421
          try {
72774
51c0f79d6eed tuned signature;
wenzelm
parents: 72772
diff changeset
   422
            val read_imports = Thy_Header.read(reader).imports
70638
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 69891
diff changeset
   423
            if (imports_pos.length == read_imports.length) read_imports else error("")
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66379
diff changeset
   424
          }
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72747
diff changeset
   425
          catch { case _: Throwable => List.fill(imports_pos.length)("") }
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66379
diff changeset
   426
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   427
        val errors =
70638
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 69891
diff changeset
   428
          for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
66768
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66379
diff changeset
   429
          yield {
f27488f47a47 completion supports theory header imports;
wenzelm
parents: 66379
diff changeset
   430
            val completion =
70713
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   431
              if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   432
            val msg =
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   433
              "Bad theory import " +
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   434
                Markup.Path(import_name.node).markup(quote(import_name.toString)) +
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   435
                Position.here(pos) + Completion.report_theories(pos, completion)
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   436
            Exn.Exn[Command.Blob](ERROR(msg))
59708
aed304412e43 more markup, which helps to create missing imports;
wenzelm
parents: 59706
diff changeset
   437
          }
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72757
diff changeset
   438
        (errors, -1)
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   439
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   440
      // auxiliary files
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   441
      case _ =>
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
   442
        val loaded_files = span.loaded_files(syntax)
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   443
        val blobs =
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
   444
          loaded_files.files.map(file =>
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   445
            (Exn.capture {
72747
5f9d66155081 clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents: 72745
diff changeset
   446
              val src_path = Path.explode(file)
5f9d66155081 clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents: 72745
diff changeset
   447
              val name = Document.Node.Name(resources.append(node_name, src_path))
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   448
              val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
72747
5f9d66155081 clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents: 72745
diff changeset
   449
              Blob(name, src_path, content)
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   450
            }).user_error)
72757
38e05b7ded61 tuned signature --- more explicit types;
wenzelm
parents: 72748
diff changeset
   451
        (blobs, loaded_files.index)
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   452
    }
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59684
diff changeset
   453
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   454
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   455
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   456
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46164
diff changeset
   457
final class Command private(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   458
    val id: Document_ID.Command,
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44607
diff changeset
   459
    val node_name: Document.Node.Name,
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   460
    val blobs_info: Command.Blobs_Info,
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57904
diff changeset
   461
    val span: Command_Span.Span,
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49359
diff changeset
   462
    val source: String,
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   463
    val init_results: Command.Results,
72722
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   464
    val init_markups: Command.Markups)
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   465
{
57912
wenzelm
parents: 57911
diff changeset
   466
  override def toString: String = id + "/" + span.kind.toString
34495
722533c532da Command: added name field and toString;
wenzelm
parents: 34491
diff changeset
   467
57910
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57905
diff changeset
   468
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57905
diff changeset
   469
  /* classification */
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 57905
diff changeset
   470
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57904
diff changeset
   471
  def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57904
diff changeset
   472
  def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
57904
922273b7bf8a tuned signature;
wenzelm
parents: 57902
diff changeset
   473
922273b7bf8a tuned signature;
wenzelm
parents: 57902
diff changeset
   474
  def is_undefined: Boolean = id == Document_ID.none
922273b7bf8a tuned signature;
wenzelm
parents: 57902
diff changeset
   475
  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
922273b7bf8a tuned signature;
wenzelm
parents: 57902
diff changeset
   476
  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
922273b7bf8a tuned signature;
wenzelm
parents: 57902
diff changeset
   477
68323
bf7336731981 more node status information;
wenzelm
parents: 68306
diff changeset
   478
  def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
bf7336731981 more node status information;
wenzelm
parents: 68306
diff changeset
   479
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   480
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54517
diff changeset
   481
  /* blobs */
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54517
diff changeset
   482
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   483
  def blobs: List[Exn.Result[Command.Blob]] = blobs_info._1
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   484
  def blobs_index: Int = blobs_info._2
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59699
diff changeset
   485
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   486
  def blobs_ok: Boolean =
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   487
    blobs.forall({ case Exn.Res(_) => true case _ => false })
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 64825
diff changeset
   488
54530
2c1440f70028 ranges of thy_load commands count as visible within perspective;
wenzelm
parents: 54524
diff changeset
   489
  def blobs_names: List[Document.Node.Name] =
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   490
    for (Exn.Res(blob) <- blobs) yield blob.name
54530
2c1440f70028 ranges of thy_load commands count as visible within perspective;
wenzelm
parents: 54524
diff changeset
   491
60916
a6e2a667b0a8 resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents: 60215
diff changeset
   492
  def blobs_undefined: List[Document.Node.Name] =
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   493
    for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name
60916
a6e2a667b0a8 resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents: 60215
diff changeset
   494
57842
8e4ae2db1849 more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents: 57615
diff changeset
   495
  def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   496
    for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest)
57842
8e4ae2db1849 more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents: 57615
diff changeset
   497
8e4ae2db1849 more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents: 57615
diff changeset
   498
  def blobs_changed(doc_blobs: Document.Blobs): Boolean =
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   499
    blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false })
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54517
diff changeset
   500
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
   501
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56395
diff changeset
   502
  /* source chunks */
55431
e0f20a44ff9d common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents: 55430
diff changeset
   503
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   504
  val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
56473
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56470
diff changeset
   505
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   506
  val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   507
    ((Symbol.Text_Chunk.Default -> chunk) ::
72745
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   508
      (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content)
5a6f7212fc4d more explicit types;
wenzelm
parents: 72744
diff changeset
   509
        yield Symbol.Text_Chunk.File(blob.name.node) -> file)).toMap
56473
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56470
diff changeset
   510
46813
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   511
  def length: Int = source.length
56473
5b5c750e9763 simplified Text.Chunk -- eliminated ooddities;
wenzelm
parents: 56470
diff changeset
   512
  def range: Text.Range = chunk.range
46813
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   513
68728
c07f6fa02c59 tuned signature;
wenzelm
parents: 68381
diff changeset
   514
  val core_range: Text.Range =
57901
e1abca2527da more explicit type Span in Scala, according to ML version;
wenzelm
parents: 57842
diff changeset
   515
    Text.Range(0,
68729
3a02b424d5fb clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents: 68728
diff changeset
   516
      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
46813
bb7280848c99 added Command.proper_range (still unused);
wenzelm
parents: 46712
diff changeset
   517
65522
4d7c5df70a14 tuned signature;
wenzelm
parents: 65488
diff changeset
   518
  def source(range: Text.Range): String = range.substring(source)
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
   519
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   520
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   521
  /* reported positions */
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   522
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   523
  def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   524
    pos match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   525
      case Position.Id(id) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   526
        val chunk_name =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   527
          pos match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   528
            case Position.File(name) if name != node_name.node =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   529
              Symbol.Text_Chunk.File(name)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   530
            case _ => Symbol.Text_Chunk.Default
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   531
          }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   532
        Some((id, chunk_name))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   533
      case _ => None
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   534
    }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   535
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   536
  def message_positions(
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   537
    self_id: Document_ID.Generic => Boolean,
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   538
    chunk_name: Symbol.Text_Chunk.Name,
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   539
    chunk: Symbol.Text_Chunk,
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   540
    message: XML.Elem): Set[Text.Range] =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   541
  {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   542
    def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   543
      reported_position(props) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   544
        case Some((id, name)) if self_id(id) && name == chunk_name =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   545
          val opt_range =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   546
            Position.Range.unapply(props) orElse {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   547
              if (name == Symbol.Text_Chunk.Default)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   548
                Position.Range.unapply(span.position)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   549
              else None
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   550
            }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   551
          opt_range match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   552
            case Some(symbol_range) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   553
              chunk.incorporate(symbol_range) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   554
                case Some(range) => set + range
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   555
                case _ => set
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   556
              }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   557
            case None => set
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   558
          }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   559
        case _ => set
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   560
      }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   561
    def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   562
      t match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   563
        case XML.Wrapped_Elem(Markup(name, props), _, body) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   564
          body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   565
        case XML.Elem(Markup(name, props), body) =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   566
          body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   567
        case XML.Text(_) => set
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   568
      }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   569
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   570
    val set = tree(Set.empty, message)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   571
    if (set.isEmpty) elem(message.markup.properties, set)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   572
    else set
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   573
  }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   574
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 70780
diff changeset
   575
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   576
  /* accumulated results */
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   577
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50500
diff changeset
   578
  val init_state: Command.State =
72722
ade53fbc6f03 clarified signature: initial markup is_empty, not init_markup;
wenzelm
parents: 72709
diff changeset
   579
    Command.State(this, results = init_results, markups = init_markups)
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   580
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52524
diff changeset
   581
  val empty_state: Command.State = Command.State(this)
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   582
}