src/Pure/PIDE/document.scala
author wenzelm
Thu, 26 Nov 2020 15:16:37 +0100
changeset 72957 cb07791d86b8
parent 72956 59a7f82a7180
child 72959 79f5e843e5ec
permissions -rw-r--r--
more strict;
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/document.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     2
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
     4
Document as collection of named nodes, each consisting of an editable
38418
9a7af64d71bb more explicit / functional ML version of document model;
wenzelm
parents: 38417
diff changeset
     5
list of commands, associated with asynchronous execution process.
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     6
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34390
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: 34868
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
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    10
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
    11
import scala.collection.mutable
37073
5e42e36a6693 @tailrec annotation;
wenzelm
parents: 37072
diff changeset
    12
5e42e36a6693 @tailrec annotation;
wenzelm
parents: 37072
diff changeset
    13
34823
2f3ea37c5958 renamed Proof_Document to Document;
wenzelm
parents: 34819
diff changeset
    14
object Document
34483
0923926022d7 superficial tuning;
wenzelm
parents: 34482
diff changeset
    15
{
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
    16
  /** document structure **/
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
    17
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    18
  /* overlays -- print functions with arguments */
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    19
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    20
  object Overlays
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    21
  {
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    22
    val empty = new Overlays(Map.empty)
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    23
  }
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    24
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    25
  final class Overlays private(rep: Map[Node.Name, Node.Overlays])
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    26
  {
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
    27
    def apply(name: Node.Name): Node.Overlays =
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    28
      rep.getOrElse(name, Node.Overlays.empty)
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    29
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    30
    private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays =
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    31
    {
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    32
      val node_overlays = f(apply(name))
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    33
      new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays))
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    34
    }
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    35
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    36
    def insert(command: Command, fn: String, args: List[String]): Overlays =
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    37
      update(command.node_name, _.insert(command, fn, args))
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    38
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    39
    def remove(command: Command, fn: String, args: List[String]): Overlays =
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    40
      update(command.node_name, _.remove(command, fn, args))
55800
wenzelm
parents: 55783
diff changeset
    41
wenzelm
parents: 55783
diff changeset
    42
    override def toString: String = rep.mkString("Overlays(", ",", ")")
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    43
  }
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    44
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
    45
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    46
  /* document blobs: auxiliary files */
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    47
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67265
diff changeset
    48
  sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean)
56335
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56314
diff changeset
    49
  {
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56314
diff changeset
    50
    def unchanged: Blob = copy(changed = false)
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56314
diff changeset
    51
  }
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    52
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    53
  object Blobs
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    54
  {
56336
60434514ec0a tuned signature -- more static typing;
wenzelm
parents: 56335
diff changeset
    55
    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    56
    val empty: Blobs = apply(Map.empty)
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    57
  }
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    58
56336
60434514ec0a tuned signature -- more static typing;
wenzelm
parents: 56335
diff changeset
    59
  final class Blobs private(blobs: Map[Node.Name, Blob])
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    60
  {
56336
60434514ec0a tuned signature -- more static typing;
wenzelm
parents: 56335
diff changeset
    61
    def get(name: Node.Name): Option[Blob] = blobs.get(name)
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    62
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    63
    def changed(name: Node.Name): Boolean =
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    64
      get(name) match {
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    65
        case Some(blob) => blob.changed
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    66
        case None => false
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    67
      }
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    68
55800
wenzelm
parents: 55783
diff changeset
    69
    override def toString: String = blobs.mkString("Blobs(", ",", ")")
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    70
  }
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    71
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    72
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55782
diff changeset
    73
  /* document nodes: theories and auxiliary files */
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
    74
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
    75
  type Edit[A, B] = (Node.Name, Node.Edit[A, B])
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
    76
  type Edit_Text = Edit[Text.Edit, Text.Perspective]
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
    77
  type Edit_Command = Edit[Command.Edit, Command.Perspective]
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
    78
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
    79
  object Node
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
    80
  {
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
    81
    /* header and name */
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
    82
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
    83
    sealed case class Header(
70828
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 70826
diff changeset
    84
      imports_pos: List[(Name, Position.T)] = Nil,
63020
02921dcc42c3 tuned signature;
wenzelm
parents: 62492
diff changeset
    85
      keywords: Thy_Header.Keywords = Nil,
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63032
diff changeset
    86
      abbrevs: Thy_Header.Abbrevs = Nil,
63020
02921dcc42c3 tuned signature;
wenzelm
parents: 62492
diff changeset
    87
      errors: List[String] = Nil)
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
    88
    {
72905
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72295
diff changeset
    89
      def imports_offset: Map[Int, Name] =
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72295
diff changeset
    90
        (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72295
diff changeset
    91
70828
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 70826
diff changeset
    92
      def imports: List[Name] = imports_pos.map(_._1)
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 70826
diff changeset
    93
66773
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
    94
      def append_errors(msgs: List[String]): Header =
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
    95
        copy(errors = errors ::: msgs)
54549
2a3053472ec3 actually expose errors of cumulative theory dependencies;
wenzelm
parents: 54530
diff changeset
    96
2a3053472ec3 actually expose errors of cumulative theory dependencies;
wenzelm
parents: 54530
diff changeset
    97
      def cat_errors(msg2: String): Header =
62492
0e53fade87fe clarified modules;
wenzelm
parents: 61197
diff changeset
    98
        copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
    99
    }
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
   100
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
   101
    val no_header: Header = Header()
63020
02921dcc42c3 tuned signature;
wenzelm
parents: 62492
diff changeset
   102
    def bad_header(msg: String): Header = Header(errors = List(msg))
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46723
diff changeset
   103
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44676
diff changeset
   104
    object Name
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44676
diff changeset
   105
    {
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
   106
      val empty: Name = Name("")
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   107
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   108
      object Ordering extends scala.math.Ordering[Name]
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   109
      {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   110
        def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   111
      }
70826
a56eab490f4e clarified signature: full dependency graph;
wenzelm
parents: 70725
diff changeset
   112
70864
29bb1ebb188f clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents: 70840
diff changeset
   113
      type Graph[A] = isabelle.Graph[Node.Name, A]
29bb1ebb188f clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents: 70840
diff changeset
   114
70882
41b5e515c238 clarified signature: eliminated unused option;
wenzelm
parents: 70866
diff changeset
   115
      def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] =
41b5e515c238 clarified signature: eliminated unused option;
wenzelm
parents: 70866
diff changeset
   116
        Graph.make(entries, symmetric = true)(Ordering)
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44676
diff changeset
   117
    }
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   118
54515
570ba266f5b5 clarified boundary cases of Document.Node.Name;
wenzelm
parents: 54513
diff changeset
   119
    sealed case class Name(node: String, master_dir: String = "", theory: String = "")
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   120
    {
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   121
      override def hashCode: Int = node.hashCode
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   122
      override def equals(that: Any): Boolean =
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   123
        that match {
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   124
          case other: Name => node == other.node
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   125
          case _ => false
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   126
        }
54509
1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents: 54462
diff changeset
   127
66849
42311fd08899 more robust: allow Windows file names;
wenzelm
parents: 66773
diff changeset
   128
      def path: Path = Path.explode(File.standard_path(node))
70866
73812c598a26 check session directories;
wenzelm
parents: 70864
diff changeset
   129
      def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
66716
8737b866bd1c tuned signature;
wenzelm
parents: 66714
diff changeset
   130
59319
wenzelm
parents: 59077
diff changeset
   131
      def is_theory: Boolean = theory.nonEmpty
65410
ad9e2c1665b6 tuned signature;
wenzelm
parents: 65361
diff changeset
   132
65439
862bfd2b4fd4 tuned signature;
wenzelm
parents: 65410
diff changeset
   133
      def theory_base_name: String = Long_Name.base_name(theory)
862bfd2b4fd4 tuned signature;
wenzelm
parents: 65410
diff changeset
   134
54510
wenzelm
parents: 54509
diff changeset
   135
      override def toString: String = if (is_theory) theory else node
56801
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56746
diff changeset
   136
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56746
diff changeset
   137
      def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
66195
bb886f13623a proper bootstrap_name (amending b42743f5b595);
wenzelm
parents: 66150
diff changeset
   138
      def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67895
diff changeset
   139
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67895
diff changeset
   140
      def json: JSON.Object.T =
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67895
diff changeset
   141
        JSON.Object("node_name" -> node, "theory_name" -> theory)
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   142
    }
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   143
66714
9fc4e144693c tuned signature;
wenzelm
parents: 66382
diff changeset
   144
    sealed case class Entry(name: Node.Name, header: Node.Header)
9fc4e144693c tuned signature;
wenzelm
parents: 66382
diff changeset
   145
    {
68307
d575281e18d0 clarified signature: Known.theories retains Document.Node.Entry (with header);
wenzelm
parents: 68301
diff changeset
   146
      def map(f: String => String): Entry = copy(name = name.map(f))
d575281e18d0 clarified signature: Known.theories retains Document.Node.Entry (with header);
wenzelm
parents: 68301
diff changeset
   147
66714
9fc4e144693c tuned signature;
wenzelm
parents: 66382
diff changeset
   148
      override def toString: String = name.toString
9fc4e144693c tuned signature;
wenzelm
parents: 66382
diff changeset
   149
    }
9fc4e144693c tuned signature;
wenzelm
parents: 66382
diff changeset
   150
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   151
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   152
    /* node overlays */
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   153
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   154
    object Overlays
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   155
    {
52976
c3d82d58beaf tuned -- use Multi_Map;
wenzelm
parents: 52972
diff changeset
   156
      val empty = new Overlays(Multi_Map.empty)
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   157
    }
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   158
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   159
    final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   160
    {
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   161
      def commands: Set[Command] = rep.keySet
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   162
      def is_empty: Boolean = rep.isEmpty
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   163
      def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   164
      def insert(cmd: Command, fn: String, args: List[String]): Overlays =
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   165
        new Overlays(rep.insert(cmd, (fn, args)))
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   166
      def remove(cmd: Command, fn: String, args: List[String]): Overlays =
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   167
        new Overlays(rep.remove(cmd, (fn, args)))
55800
wenzelm
parents: 55783
diff changeset
   168
wenzelm
parents: 55783
diff changeset
   169
      override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   170
    }
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   171
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   172
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   173
    /* edits */
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   174
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
   175
    sealed abstract class Edit[A, B]
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   176
    {
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   177
      def foreach(f: A => Unit)
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   178
      {
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   179
        this match {
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   180
          case Edits(es) => es.foreach(f)
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   181
          case _ =>
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   182
        }
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   183
      }
57621
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   184
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   185
      def is_void: Boolean =
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   186
        this match {
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   187
          case Edits(Nil) => true
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   188
          case _ => false
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   189
        }
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   190
    }
56335
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56314
diff changeset
   191
    case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
54562
301a721af68b clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
wenzelm
parents: 54549
diff changeset
   192
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
   193
    case class Edits[A, B](edits: List[A]) extends Edit[A, B]
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
   194
    case class Deps[A, B](header: Header) extends Edit[A, B]
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   195
    case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
57610
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   196
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   197
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   198
    /* perspective */
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   199
52808
143f225e50f5 allow explicit indication of required node: full eval, no prints;
wenzelm
parents: 52568
diff changeset
   200
    type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   201
    type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   202
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   203
    val no_perspective_text: Perspective_Text =
57610
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   204
      Perspective(false, Text.Perspective.empty, Overlays.empty)
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   205
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   206
    val no_perspective_command: Perspective_Command =
57614
wenzelm
parents: 57610
diff changeset
   207
      Perspective(false, Command.Perspective.empty, Overlays.empty)
wenzelm
parents: 57610
diff changeset
   208
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   209
    def is_no_perspective_text(perspective: Perspective_Text): Boolean =
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   210
      !perspective.required &&
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   211
      perspective.visible.is_empty &&
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   212
      perspective.overlays.is_empty
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   213
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   214
    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   215
      !perspective.required &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   216
      perspective.visible.is_empty &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   217
      perspective.overlays.is_empty
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   218
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   219
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   220
    /* commands */
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   221
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   222
    object Commands
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   223
    {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   224
      def apply(commands: Linear_Set[Command]): Commands = new Commands(commands)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   225
      val empty: Commands = apply(Linear_Set.empty)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   226
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   227
      def starts(commands: Iterator[Command], offset: Text.Offset = 0)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   228
        : Iterator[(Command, Text.Offset)] =
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   229
      {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   230
        var i = offset
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   231
        for (command <- commands) yield {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   232
          val start = i
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   233
          i += command.length
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   234
          (command, start)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   235
        }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   236
      }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   237
67895
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   238
      def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start)
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   239
        : Iterator[(Command, Token.Pos)] =
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   240
      {
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   241
        var p = pos
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   242
        for (command <- commands) yield {
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   243
          val start = p
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   244
          p = (p /: command.span.content)(_.advance(_))
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   245
          (command, start)
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   246
        }
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   247
      }
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   248
56398
15d0821c8667 afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
wenzelm
parents: 56394
diff changeset
   249
      private val block_size = 256
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   250
    }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   251
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   252
    final class Commands private(val commands: Linear_Set[Command])
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   253
    {
56314
9a513737a0b2 tuned signature;
wenzelm
parents: 56309
diff changeset
   254
      lazy val load_commands: List[Command] =
59319
wenzelm
parents: 59077
diff changeset
   255
        commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
54462
c9bb76303348 explicit indication of thy_load commands;
wenzelm
parents: 54328
diff changeset
   256
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   257
      private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   258
      {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   259
        val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   260
        var next_block = 0
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   261
        var last_stop = 0
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   262
        for ((command, start) <- Commands.starts(commands.iterator)) {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   263
          last_stop = start + command.length
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   264
          while (last_stop + 1 > next_block) {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   265
            blocks += (command -> start)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   266
            next_block += Commands.block_size
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   267
          }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   268
        }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   269
        (blocks.toArray, Text.Range(0, last_stop))
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   270
      }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   271
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   272
      private def full_range: Text.Range = full_index._2
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   273
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   274
      def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   275
      {
59319
wenzelm
parents: 59077
diff changeset
   276
        if (commands.nonEmpty && full_range.contains(i)) {
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   277
          val (cmd0, start0) = full_index._1(i / Commands.block_size)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   278
          Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   279
            case (cmd, start) => start + cmd.length <= i }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   280
        }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   281
        else Iterator.empty
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   282
      }
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   283
    }
57614
wenzelm
parents: 57610
diff changeset
   284
wenzelm
parents: 57610
diff changeset
   285
    val empty: Node = new Node()
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   286
  }
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   287
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   288
  final class Node private(
56335
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56314
diff changeset
   289
    val get_blob: Option[Document.Blob] = None,
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   290
    val header: Node.Header = Node.no_header,
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 63579
diff changeset
   291
    val syntax: Option[Outer_Syntax] = None,
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   292
    val text_perspective: Text.Perspective = Text.Perspective.empty,
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   293
    val perspective: Node.Perspective_Command = Node.no_perspective_command,
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   294
    _commands: Node.Commands = Node.Commands.empty)
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   295
  {
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   296
    def is_empty: Boolean =
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   297
      get_blob.isEmpty &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   298
      header == Node.no_header &&
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   299
      text_perspective.is_empty &&
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   300
      Node.is_no_perspective_command(perspective) &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   301
      commands.isEmpty
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   302
59704
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59695
diff changeset
   303
    def has_header: Boolean = header != Node.no_header
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59695
diff changeset
   304
69570
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
   305
    override def toString: String =
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
   306
      if (is_empty) "empty"
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
   307
      else if (get_blob.isDefined) "blob"
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
   308
      else "node"
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
   309
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   310
    def commands: Linear_Set[Command] = _commands.commands
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   311
    def load_commands: List[Command] = _commands.load_commands
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   312
    def load_commands_changed(doc_blobs: Blobs): Boolean =
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   313
      load_commands.exists(_.blobs_changed(doc_blobs))
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   314
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   315
    def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
55435
662e0fd39823 maintain blob edits within history, which is important for Snapshot.convert/revert;
wenzelm
parents: 55434
diff changeset
   316
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
   317
    def update_header(new_header: Node.Header): Node =
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   318
      new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 57976
diff changeset
   319
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 63579
diff changeset
   320
    def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   321
      new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   322
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   323
    def update_perspective(
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   324
        new_text_perspective: Text.Perspective,
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   325
        new_perspective: Node.Perspective_Command): Node =
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   326
      new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
46680
234f1730582d more abstract class Document.Node;
wenzelm
parents: 46679
diff changeset
   327
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   328
    def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   329
      Node.Perspective(perspective.required, text_perspective, perspective.overlays)
46680
234f1730582d more abstract class Document.Node;
wenzelm
parents: 46679
diff changeset
   330
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   331
    def same_perspective(
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   332
        other_text_perspective: Text.Perspective,
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   333
        other_perspective: Node.Perspective_Command): Boolean =
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   334
      text_perspective == other_text_perspective &&
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   335
      perspective.required == other_perspective.required &&
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   336
      perspective.visible.same(other_perspective.visible) &&
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   337
      perspective.overlays == other_perspective.overlays
52808
143f225e50f5 allow explicit indication of required node: full eval, no prints;
wenzelm
parents: 52568
diff changeset
   338
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   339
    def update_commands(new_commands: Linear_Set[Command]): Node =
52918
038458a4d11b proper low-level comparison -- heed warning by Scala compiler;
wenzelm
parents: 52901
diff changeset
   340
      if (new_commands eq _commands.commands) this
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   341
      else
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   342
        new Node(get_blob, header, syntax, text_perspective, perspective,
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   343
          Node.Commands(new_commands))
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   344
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   345
    def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   346
      _commands.iterator(i)
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   347
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   348
    def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   349
      command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   350
38879
dde403450419 Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents: 38872
diff changeset
   351
    def command_start(cmd: Command): Option[Text.Offset] =
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   352
      Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   353
67252
573077aa2826 tuned signature;
wenzelm
parents: 67247
diff changeset
   354
    def source: String =
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   355
      get_blob match {
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67265
diff changeset
   356
        case Some(blob) => blob.source
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   357
        case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   358
      }
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   359
  }
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   360
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   361
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   362
  /* development graph */
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   363
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   364
  object Nodes
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   365
  {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   366
    val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   367
  }
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   368
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   369
  final class Nodes private(graph: Graph[Node.Name, Node])
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   370
  {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   371
    def apply(name: Node.Name): Node =
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   372
      graph.default_node(name, Node.empty).get_node(name)
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   373
68300
0b5a23477911 clarified signature -- avoid confusion with Resources.is_hidden;
wenzelm
parents: 68119
diff changeset
   374
    def is_suppressed(name: Node.Name): Boolean =
57619
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   375
    {
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   376
      val graph1 = graph.default_node(name, Node.empty)
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   377
      graph1.is_maximal(name) && graph1.get_node(name).is_empty
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   378
    }
57617
335750d989a3 clarified display;
wenzelm
parents: 57616
diff changeset
   379
68301
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   380
    def purge_suppressed: Option[Nodes] =
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
   381
      graph.keys_iterator.filter(is_suppressed).toList match {
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   382
        case Nil => None
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   383
        case del => Some(new Nodes((graph /: del)(_.del_node(_))))
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   384
      }
67110
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   385
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   386
    def + (entry: (Node.Name, Node)): Nodes =
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   387
    {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   388
      val (name, node) = entry
70828
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 70826
diff changeset
   389
      val imports = node.header.imports
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   390
      val graph1 =
46739
6024353549ca clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents: 46737
diff changeset
   391
        (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   392
      val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
46739
6024353549ca clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents: 46737
diff changeset
   393
      val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
67110
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   394
      new Nodes(graph3.map_node(name, _ => node))
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   395
    }
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   396
68322
daca5f2a0c90 tuned signature;
wenzelm
parents: 68307
diff changeset
   397
    def domain: Set[Node.Name] = graph.domain
daca5f2a0c90 tuned signature;
wenzelm
parents: 68307
diff changeset
   398
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   399
    def iterator: Iterator[(Node.Name, Node)] =
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   400
      graph.iterator.map({ case (name, (node, _)) => (name, node) })
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   401
70725
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70469
diff changeset
   402
    def theory_name(theory: String): Option[Node.Name] =
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70469
diff changeset
   403
      graph.keys_iterator.find(name => name.theory == theory)
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70469
diff changeset
   404
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   405
    def commands_loading(file_name: Node.Name): List[Command] =
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   406
      (for {
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   407
        (_, node) <- iterator
56314
9a513737a0b2 tuned signature;
wenzelm
parents: 56309
diff changeset
   408
        cmd <- node.load_commands.iterator
54530
2c1440f70028 ranges of thy_load commands count as visible within perspective;
wenzelm
parents: 54528
diff changeset
   409
        name <- cmd.blobs_names.iterator
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   410
        if name == file_name
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   411
      } yield cmd).toList
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   412
46942
f5c2d66faa04 basic support for outer syntax keywords in theory header;
wenzelm
parents: 46941
diff changeset
   413
    def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
72295
11dc8929832d clarified order --- proper sorting of requirements;
wenzelm
parents: 71816
diff changeset
   414
    def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds_rev(names)
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   415
    def topological_order: List[Node.Name] = graph.topological_order
56337
520148f9921d tuned output;
wenzelm
parents: 56336
diff changeset
   416
520148f9921d tuned output;
wenzelm
parents: 56336
diff changeset
   417
    override def toString: String = topological_order.mkString("Nodes(", ",", ")")
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   418
  }
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   419
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   420
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   421
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   422
  /** versioning **/
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   423
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   424
  /* particular document versions */
34485
6475bfb4ff99 joined Document with ProofDocument;
wenzelm
parents: 34483
diff changeset
   425
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   426
  object Version
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   427
  {
46681
c083a3f621c0 more abstract class Document.Version;
wenzelm
parents: 46680
diff changeset
   428
    val init: Version = new Version()
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 57976
diff changeset
   429
    def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   430
68067
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   431
    def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version])
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   432
      : Future[Version] =
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   433
    {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   434
      if (future.is_finished) {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   435
        val version = future.join
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   436
        versions.get(version.id) match {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   437
          case Some(version1) if !(version eq version1) => Future.value(version1)
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   438
          case _ => future
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   439
        }
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   440
      }
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   441
      else future
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   442
    }
68301
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   443
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   444
    def purge_suppressed(
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   445
      versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] =
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   446
    {
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   447
      (versions /:
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   448
        (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _)
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   449
    }
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   450
  }
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   451
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   452
  final class Version private(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   453
    val id: Document_ID.Version = Document_ID.none,
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   454
    val nodes: Nodes = Nodes.empty)
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46940
diff changeset
   455
  {
55777
90484dff4dc4 tuned output;
wenzelm
parents: 55710
diff changeset
   456
    override def toString: String = "Version(" + id + ")"
67110
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   457
68300
0b5a23477911 clarified signature -- avoid confusion with Resources.is_hidden;
wenzelm
parents: 68119
diff changeset
   458
    def purge_suppressed: Option[Version] =
68301
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   459
      nodes.purge_suppressed.map(new Version(id, _))
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46940
diff changeset
   460
  }
34660
e0561943bfc9 Change consisting of a list of Edits
immler@in.tum.de
parents: 34657
diff changeset
   461
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34855
diff changeset
   462
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   463
  /* changes of plain text, eventually resulting in document edits */
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   464
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   465
  object Change
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   466
  {
46678
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   467
    val init: Change = new Change()
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   468
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   469
    def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
57620
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   470
      new Change(Some(previous), edits.reverse, version)
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   471
  }
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   472
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   473
  final class Change private(
46677
wenzelm
parents: 46208
diff changeset
   474
    val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
57620
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   475
    val rev_edits: List[Edit_Text] = Nil,
46677
wenzelm
parents: 46208
diff changeset
   476
    val version: Future[Version] = Future.value(Version.init))
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   477
  {
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   478
    def is_finished: Boolean =
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   479
      (previous match { case None => true case Some(future) => future.is_finished }) &&
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   480
      version.is_finished
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   481
46678
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   482
    def truncate: Change = new Change(None, Nil, version)
68067
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   483
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   484
    def purge(versions: Map[Document_ID.Version, Version]): Option[Change] =
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   485
    {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   486
      val previous1 = previous.map(Version.purge_future(versions, _))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   487
      val version1 = Version.purge_future(versions, version)
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   488
      if ((previous eq previous1) && (version eq version1)) None
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   489
      else Some(new Change(previous1, rev_edits, version1))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   490
    }
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   491
  }
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   492
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   493
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   494
  /* history navigation */
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   495
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   496
  object History
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   497
  {
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   498
    val init: History = new History()
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   499
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   500
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   501
  final class History private(
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   502
    val undo_list: List[Change] = List(Change.init))  // non-empty list
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   503
  {
67114
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   504
    override def toString: String = "History(" + undo_list.length + ")"
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   505
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   506
    def tip: Change = undo_list.head
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   507
    def + (change: Change): History = new History(change :: undo_list)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   508
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   509
    def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   510
    {
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   511
      val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   512
      val (retained, dropped) = undo_list.splitAt(n max retain)
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   513
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   514
      retained.splitAt(retained.length - 1) match {
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   515
        case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   516
        case _ => None
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   517
      }
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   518
    }
68067
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   519
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   520
    def purge(versions: Map[Document_ID.Version, Version]): History =
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   521
    {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   522
      val undo_list1 = undo_list.map(_.purge(versions))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   523
      if (undo_list1.forall(_.isEmpty)) this
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   524
      else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   525
    }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   526
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   527
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   528
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   529
  /* snapshot */
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   530
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   531
  object Snapshot
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   532
  {
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
   533
    val init: Snapshot = State.init.snapshot()
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   534
  }
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   535
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   536
  abstract class Snapshot
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   537
  {
64798
wenzelm
parents: 64797
diff changeset
   538
    def state: State
wenzelm
parents: 64797
diff changeset
   539
    def version: Version
wenzelm
parents: 64797
diff changeset
   540
    def is_outdated: Boolean
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   541
38427
7066fbd315ae some derived operations on Text.Range;
wenzelm
parents: 38426
diff changeset
   542
    def convert(i: Text.Offset): Text.Offset
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52887
diff changeset
   543
    def revert(i: Text.Offset): Text.Offset
39177
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38976
diff changeset
   544
    def convert(range: Text.Range): Text.Range
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38976
diff changeset
   545
    def revert(range: Text.Range): Text.Range
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   546
64798
wenzelm
parents: 64797
diff changeset
   547
    def node_name: Node.Name
wenzelm
parents: 64797
diff changeset
   548
    def node: Node
69570
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
   549
    def nodes: List[(Node.Name, Node)]
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 65471
diff changeset
   550
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   551
    def commands_loading: List[Command]
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   552
    def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
65199
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
   553
    def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   554
72956
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   555
    def command_snippet(command: Command): Snapshot =
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   556
    {
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   557
      val node_name = command.node_name
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   558
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   559
      val nodes0 = version.nodes
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   560
      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   561
      val version1 = Document.Version.make(nodes1)
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   562
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   563
      val edits: List[Edit_Text] =
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   564
        List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   565
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   566
      val state0 = state.define_command(command)
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   567
      val state1 =
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   568
        state0.continue_history(Future.value(version), edits, Future.value(version1))
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   569
          .define_version(version1, state0.the_assignment(version))
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   570
          .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   571
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   572
      state1.snapshot()
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   573
    }
59a7f82a7180 clarified signature;
wenzelm
parents: 72928
diff changeset
   574
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   575
    def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
68366
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
   576
    def messages: List[(XML.Tree, Position.T)]
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
   577
    def exports: List[Export.Entry]
68421
21465884037a clarified signature: persistent results;
wenzelm
parents: 68382
diff changeset
   578
    def exports_map: Map[String, Export.Entry]
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 65471
diff changeset
   579
64665
wenzelm
parents: 63584
diff changeset
   580
    def find_command(id: Document_ID.Generic): Option[(Node, Command)]
wenzelm
parents: 63584
diff changeset
   581
    def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
wenzelm
parents: 63584
diff changeset
   582
      : Option[Line.Node_Position]
wenzelm
parents: 63584
diff changeset
   583
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   584
    def cumulate[A](
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   585
      range: Text.Range,
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   586
      info: A,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
   587
      elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
   588
      result: List[Command.State] => (A, Text.Markup) => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   589
      status: Boolean = false): List[Text.Info[A]]
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   590
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   591
    def select[A](
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   592
      range: Text.Range,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
   593
      elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
   594
      result: List[Command.State] => Text.Markup => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   595
      status: Boolean = false): List[Text.Info[A]]
65332
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
   596
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
   597
    def command_results(range: Text.Range): Command.Results
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
   598
    def command_results(command: Command): Command.Results
68836
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   599
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   600
    def command_id_map: Map[Document_ID.Generic, Command]
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   601
  }
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   602
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   603
64814
wenzelm
parents: 64799
diff changeset
   604
  /* model */
wenzelm
parents: 64799
diff changeset
   605
65221
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   606
  trait Session
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   607
  {
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   608
    def resources: Resources
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   609
  }
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   610
64814
wenzelm
parents: 64799
diff changeset
   611
  trait Model
wenzelm
parents: 64799
diff changeset
   612
  {
wenzelm
parents: 64799
diff changeset
   613
    def session: Session
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   614
    def is_stable: Boolean
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   615
    def snapshot(): Snapshot
64814
wenzelm
parents: 64799
diff changeset
   616
65356
wenzelm
parents: 65355
diff changeset
   617
    def node_name: Node.Name
64814
wenzelm
parents: 64799
diff changeset
   618
    def is_theory: Boolean = node_name.is_theory
wenzelm
parents: 64799
diff changeset
   619
    override def toString: String = node_name.toString
wenzelm
parents: 64799
diff changeset
   620
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66849
diff changeset
   621
    def get_text(range: Text.Range): Option[String]
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66043
diff changeset
   622
64815
wenzelm
parents: 64814
diff changeset
   623
    def node_required: Boolean
65356
wenzelm
parents: 65355
diff changeset
   624
    def get_blob: Option[Blob]
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66114
diff changeset
   625
    def bibtex_entries: List[Text.Info[String]]
64815
wenzelm
parents: 64814
diff changeset
   626
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   627
    def node_edits(
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   628
      node_header: Node.Header,
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   629
      text_edits: List[Text.Edit],
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   630
      perspective: Node.Perspective_Text): List[Edit_Text] =
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   631
    {
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   632
      val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   633
        get_blob match {
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   634
          case None =>
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   635
            List(
65356
wenzelm
parents: 65355
diff changeset
   636
              Node.Deps(
66773
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   637
                if (session.resources.session_base.loaded_theory(node_name)) {
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   638
                  node_header.append_errors(
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   639
                    List("Cannot update finished theory " + quote(node_name.theory)))
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   640
                }
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   641
                else node_header),
65356
wenzelm
parents: 65355
diff changeset
   642
              Node.Edits(text_edits), perspective)
wenzelm
parents: 65355
diff changeset
   643
          case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   644
        }
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   645
      edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   646
    }
64814
wenzelm
parents: 64799
diff changeset
   647
  }
wenzelm
parents: 64799
diff changeset
   648
wenzelm
parents: 64799
diff changeset
   649
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   650
  /** global state -- document structure, execution process, editing history **/
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   651
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   652
  type Assign_Update =
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   653
    List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   654
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   655
  object State
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   656
  {
38373
wenzelm
parents: 38370
diff changeset
   657
    class Fail(state: State) extends Exception
wenzelm
parents: 38370
diff changeset
   658
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   659
    object Assignment
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   660
    {
46683
fb160aa7a9a8 more abstract class Document.State.Assignment;
wenzelm
parents: 46682
diff changeset
   661
      val init: Assignment = new Assignment()
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   662
    }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   663
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   664
    final class Assignment private(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   665
      val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
46677
wenzelm
parents: 46208
diff changeset
   666
      val is_finished: Boolean = false)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   667
    {
67114
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   668
      override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   669
44477
086bb1083552 maintain last_execs assignment on Scala side;
wenzelm
parents: 44476
diff changeset
   670
      def check_finished: Assignment = { require(is_finished); this }
47388
fe4b245af74c discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents: 46997
diff changeset
   671
      def unfinished: Assignment = new Assignment(command_execs, false)
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   672
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   673
      def assign(update: Assign_Update): Assignment =
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   674
      {
38976
a4a465dc89d9 Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;
wenzelm
parents: 38885
diff changeset
   675
        require(!is_finished)
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   676
        val command_execs1 =
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   677
          (command_execs /: update) {
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   678
            case (res, (command_id, exec_ids)) =>
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   679
              if (exec_ids.isEmpty) res - command_id
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   680
              else res + (command_id -> exec_ids)
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   681
          }
47388
fe4b245af74c discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents: 46997
diff changeset
   682
        new Assignment(command_execs1, true)
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   683
      }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   684
    }
46682
4a74fbd6f28b tuned signature;
wenzelm
parents: 46681
diff changeset
   685
4a74fbd6f28b tuned signature;
wenzelm
parents: 46681
diff changeset
   686
    val init: State =
70469
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   687
      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   688
  }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   689
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   690
  final case class State private(
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   691
    /*reachable versions*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   692
    versions: Map[Document_ID.Version, Version] = Map.empty,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   693
    /*inlined auxiliary files*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   694
    blobs: Set[SHA1.Digest] = Set.empty,
72928
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   695
    /*loaded theories in batch builds*/
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   696
    theories: Map[Document_ID.Exec, Command.State] = Map.empty,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   697
    /*static markup from define_command*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   698
    commands: Map[Document_ID.Command, Command.State] = Map.empty,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   699
    /*dynamic markup from execution*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   700
    execs: Map[Document_ID.Exec, Command.State] = Map.empty,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   701
    /*command-exec assignment for each version*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   702
    assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   703
    /*commands with markup produced by other commands (imm_succs)*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   704
    commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   705
    /*explicit (linear) history*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   706
    history: History = History.init,
57976
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   707
    /*intermediate state between remove_versions/removed_versions*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59704
diff changeset
   708
    removing_versions: Boolean = false)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   709
  {
68497
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   710
    override def toString: String =
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   711
      "State(versions = " + versions.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   712
      ", blobs = " + blobs.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   713
      ", commands = " + commands.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   714
      ", execs = " + execs.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   715
      ", assignments = " + assignments.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   716
      ", commands_redirection = " + commands_redirection.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   717
      ", history = " + history.undo_list.size +
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   718
      ", removing_versions = " + removing_versions + ")"
7266fb64de69 more scalable output;
wenzelm
parents: 68421
diff changeset
   719
38373
wenzelm
parents: 38370
diff changeset
   720
    private def fail[A]: A = throw new State.Fail(this)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   721
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   722
    def define_version(version: Version, assignment: State.Assignment): State =
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   723
    {
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   724
      val id = version.id
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   725
      copy(versions = versions + (id -> version),
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   726
        assignments = assignments + (id -> assignment.unfinished))
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   727
    }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   728
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   729
    def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest)
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   730
    def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   731
38373
wenzelm
parents: 38370
diff changeset
   732
    def define_command(command: Command): State =
wenzelm
parents: 38370
diff changeset
   733
    {
wenzelm
parents: 38370
diff changeset
   734
      val id = command.id
72957
cb07791d86b8 more strict;
wenzelm
parents: 72956
diff changeset
   735
      if (commands.isDefinedAt(id)) fail
cb07791d86b8 more strict;
wenzelm
parents: 72956
diff changeset
   736
      else copy(commands = commands + (id -> command.init_state))
38373
wenzelm
parents: 38370
diff changeset
   737
    }
wenzelm
parents: 38370
diff changeset
   738
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   739
    def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
44582
479c07072992 tuned signature;
wenzelm
parents: 44581
diff changeset
   740
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   741
    def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
52564
4e855c120f6a tuned signature -- NB: Command.read is actually part of Command.eval;
wenzelm
parents: 52563
diff changeset
   742
    def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
4e855c120f6a tuned signature -- NB: Command.read is actually part of Command.eval;
wenzelm
parents: 52563
diff changeset
   743
    def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   744
    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   745
68857
b888de4fe58c clarified signature;
wenzelm
parents: 68836
diff changeset
   746
    def lookup_id(id: Document_ID.Generic): Option[Command.State] =
72928
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   747
      theories.get(id) orElse commands.get(id) orElse execs.get(id)
68857
b888de4fe58c clarified signature;
wenzelm
parents: 68836
diff changeset
   748
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   749
    private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
56295
a40e67ce4f84 clarified valid_id: always standardize towards static command.id;
wenzelm
parents: 56176
diff changeset
   750
      id == st.command.id ||
a40e67ce4f84 clarified valid_id: always standardize towards static command.id;
wenzelm
parents: 56176
diff changeset
   751
      (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
a40e67ce4f84 clarified valid_id: always standardize towards static command.id;
wenzelm
parents: 56176
diff changeset
   752
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   753
    private def other_id(id: Document_ID.Generic)
63032
e0fa59bbc956 reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents: 63020
diff changeset
   754
      : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] =
68857
b888de4fe58c clarified signature;
wenzelm
parents: 68836
diff changeset
   755
      lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   756
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   757
    private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   758
      (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   759
        graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   760
67825
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67309
diff changeset
   761
    def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache)
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67309
diff changeset
   762
      : (Command.State, State) =
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   763
    {
72928
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   764
      def update(st: Command.State): (Command.State, State) =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   765
      {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   766
        val st1 = st.accumulate(self_id(st), other_id, message, xml_cache)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   767
        (st1, copy(commands_redirection = redirection(st1)))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   768
      }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   769
      execs.get(id).map(update) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   770
        case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1)))
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   771
        case None =>
72928
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   772
          commands.get(id).map(update) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   773
            case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1)))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   774
            case None =>
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   775
              theories.get(id).map(update) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   776
                case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1)))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   777
                case None => fail
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   778
              }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   779
          }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   780
      }
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   781
    }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   782
68104
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   783
    def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   784
    {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   785
      execs.get(id) match {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   786
        case Some(st) =>
68119
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   787
          st.add_export(entry) match {
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   788
            case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   789
            case None => fail
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   790
          }
68104
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   791
        case None =>
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   792
          commands.get(id) match {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   793
            case Some(st) =>
68119
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   794
              st.add_export(entry) match {
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   795
                case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   796
                case None => fail
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68104
diff changeset
   797
              }
68104
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   798
            case None => fail
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   799
          }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   800
      }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   801
    }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68067
diff changeset
   802
69646
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   803
    def node_exports(version: Version, node_name: Node.Name): Command.Exports =
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   804
      Command.Exports.merge(
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   805
        for {
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   806
          command <- version.nodes(node_name).commands.iterator
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   807
          st <- command_states(version, command).iterator
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   808
        } yield st.exports)
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
   809
72928
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   810
    def begin_theory(node_name: Node.Name, id: Document_ID.Exec, source: String): State =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   811
      if (theories.isDefinedAt(id)) fail
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   812
      else {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   813
        val command = Command.unparsed(source, theory = true, id = id, node_name = node_name)
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   814
        copy(theories = theories + (id -> command.empty_state))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   815
      }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   816
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   817
    def end_theory(theory: String): (Command.State, State) =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   818
      theories.find({ case (_, st) => st.command.node_name.theory == theory }) match {
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   819
        case None => fail
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   820
        case Some((id, st)) => (st, copy(theories = theories - id))
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   821
      }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72905
diff changeset
   822
70469
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   823
    def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   824
      : ((List[Node.Name], List[Command]), State) =
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   825
    {
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   826
      val version = the_version(id)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   827
70469
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   828
      val edited_set = edited.toSet
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   829
      val edited_nodes =
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   830
        (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   831
52566
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   832
      def upd(exec_id: Document_ID.Exec, st: Command.State)
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   833
          : Option[(Document_ID.Exec, Command.State)] =
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   834
        if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   835
44543
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   836
      val (changed_commands, new_execs) =
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   837
        ((Nil: List[Command], execs) /: update) {
52566
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   838
          case ((commands1, execs1), (command_id, exec)) =>
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   839
            val st = the_static_state(command_id)
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   840
            val command = st.command
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   841
            val commands2 = command :: commands1
44543
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   842
            val execs2 =
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   843
              exec match {
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   844
                case Nil => execs1
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   845
                case eval_id :: print_ids =>
52566
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   846
                  execs1 ++ upd(eval_id, st) ++
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   847
                    (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up)
44543
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   848
              }
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   849
            (commands2, execs2)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   850
        }
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   851
      val new_assignment = the_assignment(version).assign(update)
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   852
      val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   853
70469
3e17c3a5fd39 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents: 69646
diff changeset
   854
      ((edited_nodes, changed_commands), new_state)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   855
    }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   856
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   857
    def is_assigned(version: Version): Boolean =
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   858
      assignments.get(version.id) match {
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   859
        case Some(assgn) => assgn.is_finished
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   860
        case None => false
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   861
      }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   862
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   863
    def is_stable(change: Change): Boolean =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   864
      change.is_finished && is_assigned(change.version.get_finished)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   865
46944
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   866
    def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   867
    def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
60933
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60916
diff changeset
   868
    def stable_tip_version: Option[Version] =
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60916
diff changeset
   869
      if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   870
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44443
diff changeset
   871
    def continue_history(
56711
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   872
      previous: Future[Version],
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   873
      edits: List[Edit_Text],
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   874
      version: Future[Version]): State =
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   875
    {
46678
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   876
      val change = Change.make(previous, edits, version)
56711
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   877
      copy(history = history + change)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   878
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   879
57976
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   880
    def remove_versions(retain: Int = 0): (List[Version], State) =
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   881
    {
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   882
      history.prune(is_stable, retain) match {
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   883
        case Some((dropped, history1)) =>
57976
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   884
          val old_versions = dropped.map(change => change.version.get_finished)
59319
wenzelm
parents: 59077
diff changeset
   885
          val removing = old_versions.nonEmpty
57976
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   886
          val state1 = copy(history = history1, removing_versions = removing)
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   887
          (old_versions, state1)
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   888
        case None => fail
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   889
      }
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   890
    }
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   891
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   892
    def removed_versions(removed: List[Document_ID.Version]): State =
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   893
    {
68301
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   894
      val versions1 = Version.purge_suppressed(versions -- removed)
67110
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   895
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   896
      val assignments1 = assignments -- removed
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   897
      var blobs1_names = Set.empty[Node.Name]
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   898
      var blobs1 = Set.empty[SHA1.Digest]
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   899
      var commands1 = Map.empty[Document_ID.Command, Command.State]
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   900
      var execs1 = Map.empty[Document_ID.Exec, Command.State]
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   901
      for {
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   902
        (version_id, version) <- versions1.iterator
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46944
diff changeset
   903
        command_execs = assignments1(version_id).command_execs
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   904
        (_, node) <- version.nodes.iterator
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   905
        command <- node.commands.iterator
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   906
      } {
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   907
        for ((name, digest) <- command.blobs_defined) {
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   908
          blobs1_names += name
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   909
          blobs1 += digest
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   910
        }
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   911
52568
wenzelm
parents: 52566
diff changeset
   912
        if (!commands1.isDefinedAt(command.id))
wenzelm
parents: 52566
diff changeset
   913
          commands.get(command.id).foreach(st => commands1 += (command.id -> st))
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   914
52568
wenzelm
parents: 52566
diff changeset
   915
        for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   916
          if (!execs1.isDefinedAt(exec_id))
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   917
            execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   918
        }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   919
      }
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   920
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   921
      copy(
68301
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   922
        versions = versions1,
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   923
        blobs = blobs1,
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   924
        commands = commands1,
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   925
        execs = execs1,
70889
3eb30d80cee6 tuned signature;
wenzelm
parents: 70882
diff changeset
   926
        commands_redirection = commands_redirection.restrict(commands1.keySet),
57976
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   927
        assignments = assignments1,
68301
cd8ab1a7a286 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
wenzelm
parents: 68300
diff changeset
   928
        history = history.purge(versions1),
57976
bf99106b6672 postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
wenzelm
parents: 57842
diff changeset
   929
        removing_versions = false)
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   930
    }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   931
68836
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   932
    def command_id_map(version: Version, commands: Iterable[Command])
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   933
      : Map[Document_ID.Generic, Command] =
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   934
    {
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   935
      require(is_assigned(version))
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   936
      val assignment = the_assignment(version).check_finished
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   937
      (for {
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   938
        command <- commands.iterator
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   939
        id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   940
      } yield (id -> command)).toMap
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   941
    }
cf52379c0776 systematic access to command ids;
wenzelm
parents: 68728
diff changeset
   942
70970
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
   943
    def command_maybe_consolidated(version: Version, command: Command): Boolean =
68382
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   944
    {
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   945
      require(is_assigned(version))
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   946
      try {
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   947
        the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
70970
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
   948
          case eval_id :: print_ids =>
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
   949
            the_dynamic_state(eval_id).maybe_consolidated &&
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
   950
            !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating)
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
   951
          case Nil => false
68382
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   952
        }
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   953
      }
70970
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
   954
      catch { case _: State.Fail => false }
68382
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   955
    }
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
   956
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   957
    private def command_states_self(version: Version, command: Command)
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   958
      : List[(Document_ID.Generic, Command.State)] =
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   959
    {
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   960
      require(is_assigned(version))
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   961
      try {
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   962
        the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   963
          .map(id => id -> the_dynamic_state(id)) match {
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   964
            case Nil => fail
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   965
            case res => res
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   966
          }
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   967
      }
47395
e6261a493f04 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents: 47388
diff changeset
   968
      catch {
e6261a493f04 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents: 47388
diff changeset
   969
        case _: State.Fail =>
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   970
          try { List(command.id -> the_static_state(command.id)) }
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   971
          catch { case _: State.Fail => List(command.id -> command.init_state) }
47395
e6261a493f04 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents: 47388
diff changeset
   972
      }
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   973
    }
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   974
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   975
    def command_states(version: Version, command: Command): List[Command.State] =
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   976
    {
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   977
      val self = command_states_self(version, command)
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   978
      val others =
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   979
        if (commands_redirection.defined(command.id)) {
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   980
          (for {
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   981
            command_id <- commands_redirection.imm_succs(command.id).iterator
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   982
            (id, st) <- command_states_self(version, the_static_state(command_id).command)
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   983
            if !self.exists(_._1 == id)
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   984
          } yield (id, st)).toMap.valuesIterator.toList
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   985
        }
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   986
        else Nil
56489
wenzelm
parents: 56475
diff changeset
   987
      self.map(_._2) ::: others.flatMap(_.redirect(command))
56470
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   988
    }
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   989
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56298
diff changeset
   990
    def command_results(version: Version, command: Command): Command.Results =
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56298
diff changeset
   991
      Command.State.merge_results(command_states(version, command))
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56298
diff changeset
   992
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   993
    def command_markup(version: Version, command: Command, index: Command.Markup_Index,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
   994
        range: Text.Range, elements: Markup.Elements): Markup_Tree =
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   995
      Command.State.merge_markup(command_states(version, command), index, range, elements)
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56298
diff changeset
   996
66041
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   997
    def markup_to_XML(
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   998
      version: Version,
67265
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
   999
      node_name: Node.Name,
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
  1000
      range: Text.Range,
66041
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
  1001
      elements: Markup.Elements): XML.Body =
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
  1002
    {
67265
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1003
      val node = version.nodes(node_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1004
      if (node_name.is_theory) {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1005
        val markup_index = Command.Markup_Index.markup
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1006
        (for {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1007
          command <- node.commands.iterator
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1008
          command_range <- command.range.try_restrict(range).iterator
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1009
          markup = command_markup(version, command, markup_index, command_range, elements)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1010
          tree <- markup.to_XML(command_range, command.source, elements).iterator
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1011
        } yield tree).toList
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1012
      }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1013
      else {
67266
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67265
diff changeset
  1014
        val node_source = node.source
67265
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1015
        Text.Range(0, node_source.length).try_restrict(range) match {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1016
          case None => Nil
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1017
          case Some(node_range) =>
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1018
            val markup =
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1019
              version.nodes.commands_loading(node_name).headOption match {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1020
                case None => Markup_Tree.empty
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1021
                case Some(command) =>
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1022
                  val chunk_name = Symbol.Text_Chunk.File(node_name.node)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1023
                  val markup_index = Command.Markup_Index(false, chunk_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1024
                  command_markup(version, command, markup_index, node_range, elements)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1025
              }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1026
            markup.to_XML(node_range, node_source, elements)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1027
        }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1028
      }
66041
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
  1029
    }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1030
68324
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1031
    def node_initialized(version: Version, name: Node.Name): Boolean =
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1032
      name.is_theory &&
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1033
      (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1034
        case None => false
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1035
        case Some(command) => command_states(version, command).headOption.exists(_.initialized)
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1036
      })
bf7336731981 more node status information;
wenzelm
parents: 68323
diff changeset
  1037
68382
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
  1038
    def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
  1039
      name.is_theory &&
70970
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70906
diff changeset
  1040
      version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))
68382
2fd3a6d6ba2e less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents: 68366
diff changeset
  1041
66382
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
  1042
    def node_consolidated(version: Version, name: Node.Name): Boolean =
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
  1043
      !name.is_theory ||
68336
2f080a51a10d clarified: consolidated result is last command;
wenzelm
parents: 68324
diff changeset
  1044
      {
2f080a51a10d clarified: consolidated result is last command;
wenzelm
parents: 68324
diff changeset
  1045
        val it = version.nodes(name).commands.reverse.iterator
2f080a51a10d clarified: consolidated result is last command;
wenzelm
parents: 68324
diff changeset
  1046
        it.hasNext && command_states(version, it.next).exists(_.consolidated)
2f080a51a10d clarified: consolidated result is last command;
wenzelm
parents: 68324
diff changeset
  1047
      }
66382
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
  1048
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1049
    // persistent user-view
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 48923
diff changeset
  1050
    def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 48923
diff changeset
  1051
      : Snapshot =
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
  1052
    {
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
  1053
      val stable = recent_stable
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
  1054
      val latest = history.tip
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1055
57620
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1056
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1057
      /* pending edits and unstable changes */
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1058
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1059
      val rev_pending_changes =
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1060
        for {
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1061
          change <- history.undo_list.takeWhile(_ != stable)
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1062
          (a, edits) <- change.rev_edits
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1063
          if a == name
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1064
        } yield edits
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1065
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1066
      val edits =
64819
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
  1067
        (pending_edits /: rev_pending_changes)({
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
  1068
          case (edits, Node.Edits(es)) => es ::: edits
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
  1069
          case (edits, _) => edits
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
  1070
        })
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1071
      lazy val reverse_edits = edits.reverse
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1072
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1073
      new Snapshot
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1074
      {
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
  1075
        /* global information */
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
  1076
64798
wenzelm
parents: 64797
diff changeset
  1077
        val state: State = State.this
wenzelm
parents: 64797
diff changeset
  1078
        val version: Version = stable.version.get_finished
wenzelm
parents: 64797
diff changeset
  1079
        val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1080
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1081
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1082
        /* local node content */
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1083
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
  1084
        def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i))
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
  1085
        def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i))
57620
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
  1086
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
  1087
        def convert(range: Text.Range): Text.Range = range.map(convert)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
  1088
        def revert(range: Text.Range): Text.Range = range.map(revert)
39177
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38976
diff changeset
  1089
64798
wenzelm
parents: 64797
diff changeset
  1090
        val node_name: Node.Name = name
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1091
        val node: Node = version.nodes(name)
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
  1092
69570
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
  1093
        def nodes: List[(Node.Name, Node)] =
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
  1094
          (node_name :: node.load_commands.flatMap(_.blobs_names)).
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
  1095
            map(name => (name, version.nodes(name)))
0a38f23ca4c5 clarified signature;
wenzelm
parents: 69260
diff changeset
  1096
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1097
        val commands_loading: List[Command] =
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
  1098
          if (node_name.is_theory) Nil
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1099
          else version.nodes.commands_loading(node_name)
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 55431
diff changeset
  1100
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1101
        def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1102
          (for {
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1103
            cmd <- node.load_commands.iterator
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1104
            blob_name <- cmd.blobs_names.iterator
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1105
            if pred(blob_name)
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
  1106
            start <- node.command_start(cmd)
68728
c07f6fa02c59 tuned signature;
wenzelm
parents: 68497
diff changeset
  1107
          } yield convert(cmd.core_range + start)).toList
56176
0bc9b0ad6287 tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
wenzelm
parents: 55820
diff changeset
  1108
65199
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1109
        def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1110
          if (other_node_name.is_theory) {
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1111
            val other_node = version.nodes(other_node_name)
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1112
            val iterator = other_node.command_iterator(revert(offset) max 0)
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1113
            if (iterator.hasNext) {
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1114
              val (command0, _) = iterator.next
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1115
              other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1116
            }
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1117
            else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1118
          }
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1119
          else version.nodes.commands_loading(other_node_name).headOption
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
  1120
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
  1121
        def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
67265
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67252
diff changeset
  1122
          state.markup_to_XML(version, node_name, range, elements)
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 65471
diff changeset
  1123
68421
21465884037a clarified signature: persistent results;
wenzelm
parents: 68382
diff changeset
  1124
        lazy val messages: List[(XML.Tree, Position.T)] =
68366
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1125
          (for {
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1126
            (command, start) <-
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1127
              Document.Node.Commands.starts_pos(
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1128
                node.commands.iterator, Token.Pos.file(node_name.node))
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1129
            pos = command.span.keyword_pos(start).position(command.span.name)
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1130
            (_, tree) <- state.command_results(version, command).iterator
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1131
           } yield (tree, pos)).toList
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1132
68421
21465884037a clarified signature: persistent results;
wenzelm
parents: 68382
diff changeset
  1133
        lazy val exports: List[Export.Entry] =
69646
3d91a7a58113 tuned signature;
wenzelm
parents: 69570
diff changeset
  1134
          state.node_exports(version, node_name).iterator.map(_._2).toList
68366
f9379279f98c clarified signature: prefer Document.Snapshot;
wenzelm
parents: 68336
diff changeset
  1135
68421
21465884037a clarified signature: persistent results;
wenzelm
parents: 68382
diff changeset
  1136
        lazy val exports_map: Map[String, Export.Entry] =
21465884037a clarified signature: persistent results;
wenzelm
parents: 68382
diff changeset
  1137
          (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
21465884037a clarified signature: persistent results;
wenzelm
parents: 68382
diff changeset
  1138
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1139
64665
wenzelm
parents: 63584
diff changeset
  1140
        /* find command */
wenzelm
parents: 63584
diff changeset
  1141
wenzelm
parents: 63584
diff changeset
  1142
        def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
68857
b888de4fe58c clarified signature;
wenzelm
parents: 68836
diff changeset
  1143
          state.lookup_id(id) match {
64665
wenzelm
parents: 63584
diff changeset
  1144
            case None => None
wenzelm
parents: 63584
diff changeset
  1145
            case Some(st) =>
wenzelm
parents: 63584
diff changeset
  1146
              val command = st.command
wenzelm
parents: 63584
diff changeset
  1147
              val node = version.nodes(command.node_name)
wenzelm
parents: 63584
diff changeset
  1148
              if (node.commands.contains(command)) Some((node, command)) else None
wenzelm
parents: 63584
diff changeset
  1149
          }
wenzelm
parents: 63584
diff changeset
  1150
wenzelm
parents: 63584
diff changeset
  1151
        def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
wenzelm
parents: 63584
diff changeset
  1152
            : Option[Line.Node_Position] =
wenzelm
parents: 63584
diff changeset
  1153
          for ((node, command) <- find_command(id))
wenzelm
parents: 63584
diff changeset
  1154
          yield {
wenzelm
parents: 63584
diff changeset
  1155
            val name = command.node_name.node
wenzelm
parents: 63584
diff changeset
  1156
            val sources_iterator =
wenzelm
parents: 63584
diff changeset
  1157
              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm
parents: 63584
diff changeset
  1158
                (if (offset == 0) Iterator.empty
wenzelm
parents: 63584
diff changeset
  1159
                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
65196
e8760a98db78 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents: 65195
diff changeset
  1160
            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
64665
wenzelm
parents: 63584
diff changeset
  1161
            Line.Node_Position(name, pos)
wenzelm
parents: 63584
diff changeset
  1162
          }
wenzelm
parents: 63584
diff changeset
  1163
wenzelm
parents: 63584
diff changeset
  1164
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1165
        /* cumulate markup */
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1166
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1167
        def cumulate[A](
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1168
          range: Text.Range,
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1169
          info: A,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
  1170
          elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1171
          result: List[Command.State] => (A, Text.Markup) => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1172
          status: Boolean = false): List[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45243
diff changeset
  1173
        {
56590
d01d183e84ea clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents: 56514
diff changeset
  1174
          val former_range = revert(range).inflate_singularity
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56398
diff changeset
  1175
          val (chunk_name, command_iterator) =
65187
wenzelm
parents: 64867
diff changeset
  1176
            commands_loading.headOption match {
wenzelm
parents: 64867
diff changeset
  1177
              case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
wenzelm
parents: 64867
diff changeset
  1178
              case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1179
            }
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56398
diff changeset
  1180
          val markup_index = Command.Markup_Index(status, chunk_name)
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1181
          (for {
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
  1182
            (command, command_start) <- command_iterator
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56398
diff changeset
  1183
            chunk <- command.chunks.get(chunk_name).iterator
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1184
            states = state.command_states(version, command)
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1185
            res = result(states)
56590
d01d183e84ea clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents: 56514
diff changeset
  1186
            markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
d01d183e84ea clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents: 56514
diff changeset
  1187
            markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
d01d183e84ea clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents: 56514
diff changeset
  1188
            Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1189
              {
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1190
                case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1191
              }).iterator
56590
d01d183e84ea clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents: 56514
diff changeset
  1192
            r1 <- convert(r0 + command_start).try_restrict(range).iterator
d01d183e84ea clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents: 56514
diff changeset
  1193
          } yield Text.Info(r1, a)).toList
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45243
diff changeset
  1194
        }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45243
diff changeset
  1195
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1196
        def select[A](
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1197
          range: Text.Range,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
  1198
          elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1199
          result: List[Command.State] => Text.Markup => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1200
          status: Boolean = false): List[Text.Info[A]] =
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38841
diff changeset
  1201
        {
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1202
          def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] =
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50204
diff changeset
  1203
          {
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1204
            val res = result(states)
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52887
diff changeset
  1205
            (_: Option[A], x: Text.Markup) =>
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52887
diff changeset
  1206
              res(x) match {
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52887
diff changeset
  1207
                case None => None
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52887
diff changeset
  1208
                case some => Some(some)
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52887
diff changeset
  1209
              }
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50204
diff changeset
  1210
          }
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71182
diff changeset
  1211
          for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46178
diff changeset
  1212
            yield Text.Info(r, x)
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38841
diff changeset
  1213
        }
55800
wenzelm
parents: 55783
diff changeset
  1214
wenzelm
parents: 55783
diff changeset
  1215
65332
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1216
        /* command results */
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1217
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1218
        def command_results(range: Text.Range): Command.Results =
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1219
          Command.State.merge_results(
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1220
            select[List[Command.State]](range, Markup.Elements.full, command_states =>
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1221
              { case _ => Some(command_states) }).flatMap(_.info))
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1222
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1223
        def command_results(command: Command): Command.Results =
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1224
          state.command_results(version, command)
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1225
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1226