src/Pure/PIDE/document.scala
author wenzelm
Tue, 08 May 2018 11:47:41 +0200
changeset 68114 ce7f35406f37
parent 68101 0699a0bacc50
child 68299 0b5a23477911
permissions -rw-r--r--
more robust: self-export only;
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
67265
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67264
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(
63020
02921dcc42c3 tuned signature;
wenzelm
parents: 62492
diff changeset
    84
      imports: List[(Name, Position.T)] = Nil,
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
    {
66773
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
    89
      def append_errors(msgs: List[String]): Header =
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
    90
        copy(errors = errors ::: msgs)
54549
2a3053472ec3 actually expose errors of cumulative theory dependencies;
wenzelm
parents: 54530
diff changeset
    91
2a3053472ec3 actually expose errors of cumulative theory dependencies;
wenzelm
parents: 54530
diff changeset
    92
      def cat_errors(msg2: String): Header =
62492
0e53fade87fe clarified modules;
wenzelm
parents: 61197
diff changeset
    93
        copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
    94
    }
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
    95
63020
02921dcc42c3 tuned signature;
wenzelm
parents: 62492
diff changeset
    96
    val no_header = Header()
02921dcc42c3 tuned signature;
wenzelm
parents: 62492
diff changeset
    97
    def bad_header(msg: String): Header = Header(errors = List(msg))
46737
09ab89658a5d clarified module Thy_Load;
wenzelm
parents: 46723
diff changeset
    98
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44676
diff changeset
    99
    object Name
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44676
diff changeset
   100
    {
54515
570ba266f5b5 clarified boundary cases of Document.Node.Name;
wenzelm
parents: 54513
diff changeset
   101
      val empty = Name("")
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   102
65471
05e5bffcf1d8 clarified loaded_theories: map to qualified theory name;
wenzelm
parents: 65445
diff changeset
   103
      def loaded_theory(theory: String): Name = Name(theory, "", theory)
05e5bffcf1d8 clarified loaded_theories: map to qualified theory name;
wenzelm
parents: 65445
diff changeset
   104
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   105
      object Ordering extends scala.math.Ordering[Name]
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   106
      {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   107
        def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   108
      }
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44676
diff changeset
   109
    }
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   110
54515
570ba266f5b5 clarified boundary cases of Document.Node.Name;
wenzelm
parents: 54513
diff changeset
   111
    sealed case class Name(node: String, master_dir: String = "", theory: String = "")
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   112
    {
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   113
      override def hashCode: Int = node.hashCode
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   114
      override def equals(that: Any): Boolean =
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   115
        that match {
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   116
          case other: Name => node == other.node
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   117
          case _ => false
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   118
        }
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
   119
66849
42311fd08899 more robust: allow Windows file names;
wenzelm
parents: 66773
diff changeset
   120
      def path: Path = Path.explode(File.standard_path(node))
66716
8737b866bd1c tuned signature;
wenzelm
parents: 66714
diff changeset
   121
67290
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67265
diff changeset
   122
      def is_bibtex: Boolean = Bibtex.is_bibtex(node)
67293
2fe338d91d47 tuned signature;
wenzelm
parents: 67290
diff changeset
   123
      def is_bibtex_theory: Boolean = Bibtex.is_bibtex(theory)
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   124
59319
wenzelm
parents: 59077
diff changeset
   125
      def is_theory: Boolean = theory.nonEmpty
65409
ad9e2c1665b6 tuned signature;
wenzelm
parents: 65361
diff changeset
   126
65439
862bfd2b4fd4 tuned signature;
wenzelm
parents: 65409
diff changeset
   127
      def theory_base_name: String = Long_Name.base_name(theory)
862bfd2b4fd4 tuned signature;
wenzelm
parents: 65409
diff changeset
   128
54510
wenzelm
parents: 54509
diff changeset
   129
      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
   130
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
   131
      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
   132
      def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
67943
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67895
diff changeset
   133
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67895
diff changeset
   134
      def json: JSON.Object.T =
b45f0c0ea14f clarified theory node name;
wenzelm
parents: 67895
diff changeset
   135
        JSON.Object("node_name" -> node, "theory_name" -> theory)
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   136
    }
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44613
diff changeset
   137
66714
9fc4e144693c tuned signature;
wenzelm
parents: 66379
diff changeset
   138
    sealed case class Entry(name: Node.Name, header: Node.Header)
9fc4e144693c tuned signature;
wenzelm
parents: 66379
diff changeset
   139
    {
9fc4e144693c tuned signature;
wenzelm
parents: 66379
diff changeset
   140
      override def toString: String = name.toString
9fc4e144693c tuned signature;
wenzelm
parents: 66379
diff changeset
   141
    }
9fc4e144693c tuned signature;
wenzelm
parents: 66379
diff changeset
   142
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   143
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   144
    /* node overlays */
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   145
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   146
    object Overlays
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   147
    {
52976
c3d82d58beaf tuned -- use Multi_Map;
wenzelm
parents: 52972
diff changeset
   148
      val empty = new Overlays(Multi_Map.empty)
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   149
    }
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   150
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   151
    final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   152
    {
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   153
      def commands: Set[Command] = rep.keySet
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   154
      def is_empty: Boolean = rep.isEmpty
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   155
      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
   156
      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
   157
        new Overlays(rep.insert(cmd, (fn, args)))
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52976
diff changeset
   158
      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
   159
        new Overlays(rep.remove(cmd, (fn, args)))
55800
wenzelm
parents: 55783
diff changeset
   160
wenzelm
parents: 55783
diff changeset
   161
      override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   162
    }
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   163
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   164
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   165
    /* edits */
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   166
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
   167
    sealed abstract class Edit[A, B]
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   168
    {
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   169
      def foreach(f: A => Unit)
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   170
      {
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   171
        this match {
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   172
          case Edits(es) => es.foreach(f)
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   173
          case _ =>
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   174
        }
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44222
diff changeset
   175
      }
57621
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   176
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   177
      def is_void: Boolean =
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   178
        this match {
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   179
          case Edits(Nil) => true
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   180
          case _ => false
caa37976801f more frugal edits;
wenzelm
parents: 57620
diff changeset
   181
        }
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   182
    }
56335
8953d4cc060a store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents: 56314
diff changeset
   183
    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
   184
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
   185
    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
   186
    case class Deps[A, B](header: Header) extends Edit[A, B]
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   187
    case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
57610
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   188
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   189
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   190
    /* perspective */
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   191
52808
143f225e50f5 allow explicit indication of required node: full eval, no prints;
wenzelm
parents: 52568
diff changeset
   192
    type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   193
    type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43780
diff changeset
   194
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   195
    val no_perspective_text: Perspective_Text =
57610
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   196
      Perspective(false, Text.Perspective.empty, Overlays.empty)
518e28a7c74b tuned signature;
wenzelm
parents: 56801
diff changeset
   197
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   198
    val no_perspective_command: Perspective_Command =
57614
wenzelm
parents: 57610
diff changeset
   199
      Perspective(false, Command.Perspective.empty, Overlays.empty)
wenzelm
parents: 57610
diff changeset
   200
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   201
    def is_no_perspective_text(perspective: Perspective_Text): Boolean =
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   202
      !perspective.required &&
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   203
      perspective.visible.is_empty &&
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   204
      perspective.overlays.is_empty
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   205
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   206
    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
   207
      !perspective.required &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   208
      perspective.visible.is_empty &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   209
      perspective.overlays.is_empty
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   210
52887
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   211
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   212
    /* commands */
98eac7b7eec3 tuned signature;
wenzelm
parents: 52862
diff changeset
   213
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   214
    object Commands
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   215
    {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   216
      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
   217
      val empty: Commands = apply(Linear_Set.empty)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   218
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   219
      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
   220
        : Iterator[(Command, Text.Offset)] =
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   221
      {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   222
        var i = offset
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   223
        for (command <- commands) yield {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   224
          val start = i
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   225
          i += command.length
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   226
          (command, start)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   227
        }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   228
      }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   229
67895
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   230
      def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start)
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   231
        : Iterator[(Command, Token.Pos)] =
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   232
      {
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   233
        var p = pos
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   234
        for (command <- commands) yield {
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   235
          val start = p
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   236
          p = (p /: command.span.content)(_.advance(_))
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   237
          (command, start)
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   238
        }
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   239
      }
cd00999d2d30 more position information;
wenzelm
parents: 67825
diff changeset
   240
56398
15d0821c8667 afford larger full_index, to save a few milliseconds during rendering (notably text_overview);
wenzelm
parents: 56394
diff changeset
   241
      private val block_size = 256
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   242
    }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   243
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   244
    final class Commands private(val commands: Linear_Set[Command])
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   245
    {
56314
9a513737a0b2 tuned signature;
wenzelm
parents: 56309
diff changeset
   246
      lazy val load_commands: List[Command] =
59319
wenzelm
parents: 59077
diff changeset
   247
        commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
54462
c9bb76303348 explicit indication of thy_load commands;
wenzelm
parents: 54328
diff changeset
   248
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   249
      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
   250
      {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   251
        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
   252
        var next_block = 0
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   253
        var last_stop = 0
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   254
        for ((command, start) <- Commands.starts(commands.iterator)) {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   255
          last_stop = start + command.length
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   256
          while (last_stop + 1 > next_block) {
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   257
            blocks += (command -> start)
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   258
            next_block += Commands.block_size
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   259
          }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   260
        }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   261
        (blocks.toArray, Text.Range(0, last_stop))
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   262
      }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   263
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   264
      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
   265
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   266
      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
   267
      {
59319
wenzelm
parents: 59077
diff changeset
   268
        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
   269
          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
   270
          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
   271
            case (cmd, start) => start + cmd.length <= i }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   272
        }
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   273
        else Iterator.empty
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   274
      }
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   275
    }
57614
wenzelm
parents: 57610
diff changeset
   276
wenzelm
parents: 57610
diff changeset
   277
    val empty: Node = new Node()
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   278
  }
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   279
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   280
  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
   281
    val get_blob: Option[Document.Blob] = None,
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   282
    val header: Node.Header = Node.no_header,
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 63579
diff changeset
   283
    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
   284
    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
   285
    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
   286
    _commands: Node.Commands = Node.Commands.empty)
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   287
  {
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   288
    def is_empty: Boolean =
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   289
      get_blob.isEmpty &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   290
      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
   291
      text_perspective.is_empty &&
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   292
      Node.is_no_perspective_command(perspective) &&
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   293
      commands.isEmpty
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   294
59702
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59695
diff changeset
   295
    def has_header: Boolean = header != Node.no_header
58dfaa369c11 hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents: 59695
diff changeset
   296
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   297
    def commands: Linear_Set[Command] = _commands.commands
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   298
    def load_commands: List[Command] = _commands.load_commands
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   299
    def load_commands_changed(doc_blobs: Blobs): Boolean =
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   300
      load_commands.exists(_.blobs_changed(doc_blobs))
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57614
diff changeset
   301
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   302
    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
   303
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48706
diff changeset
   304
    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
   305
      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
   306
63584
68751fe1c036 tuned signature -- prover-independence is presently theoretical;
wenzelm
parents: 63579
diff changeset
   307
    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
   308
      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
   309
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   310
    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
   311
        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
   312
        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
   313
      new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
46680
234f1730582d more abstract class Document.Node;
wenzelm
parents: 46679
diff changeset
   314
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   315
    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
   316
      Node.Perspective(perspective.required, text_perspective, perspective.overlays)
46680
234f1730582d more abstract class Document.Node;
wenzelm
parents: 46679
diff changeset
   317
59372
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   318
    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
   319
        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
   320
        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
   321
      text_perspective == other_text_perspective &&
52849
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   322
      perspective.required == other_perspective.required &&
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   323
      perspective.visible.same(other_perspective.visible) &&
199e9fa5a5c2 maintain overlays within node perspective;
wenzelm
parents: 52808
diff changeset
   324
      perspective.overlays == other_perspective.overlays
52808
143f225e50f5 allow explicit indication of required node: full eval, no prints;
wenzelm
parents: 52568
diff changeset
   325
52901
8be75f53db82 maintain commands together with index -- avoid redundant reconstruction of full_index;
wenzelm
parents: 52900
diff changeset
   326
    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
   327
      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
   328
      else
503739360344 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
wenzelm
parents: 59319
diff changeset
   329
        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
   330
          Node.Commands(new_commands))
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   331
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   332
    def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   333
      _commands.iterator(i)
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   334
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   335
    def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
   336
      command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   337
38879
dde403450419 Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents: 38872
diff changeset
   338
    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
   339
      Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   340
67251
573077aa2826 tuned signature;
wenzelm
parents: 67247
diff changeset
   341
    def source: String =
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   342
      get_blob match {
67265
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67264
diff changeset
   343
        case Some(blob) => blob.source
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   344
        case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   345
      }
38151
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   346
  }
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   347
2837c952ca31 explicit Change.Snapshot and Document.Node;
wenzelm
parents: 38150
diff changeset
   348
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   349
  /* development graph */
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   350
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   351
  object Nodes
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   352
  {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   353
    val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   354
  }
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   355
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   356
  final class Nodes private(graph: Graph[Node.Name, Node])
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   357
  {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   358
    def apply(name: Node.Name): Node =
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   359
      graph.default_node(name, Node.empty).get_node(name)
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   360
57619
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   361
    def is_hidden(name: Node.Name): Boolean =
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   362
    {
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   363
      val graph1 = graph.default_node(name, Node.empty)
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   364
      graph1.is_maximal(name) && graph1.get_node(name).is_empty
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   365
    }
57617
335750d989a3 clarified display;
wenzelm
parents: 57616
diff changeset
   366
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   367
    def purge(pred: Node.Name => Boolean): Option[Nodes] =
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   368
      graph.keys_iterator.filter(pred).toList match {
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   369
        case Nil => None
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   370
        case del => Some(new Nodes((graph /: del)(_.del_node(_))))
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   371
      }
67110
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   372
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   373
    def + (entry: (Node.Name, Node)): Nodes =
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   374
    {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   375
      val (name, node) = entry
59695
a03e0561bdbf clarified positions of theory imports;
wenzelm
parents: 59372
diff changeset
   376
      val imports = node.header.imports.map(_._1)
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   377
      val graph1 =
46739
6024353549ca clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents: 46737
diff changeset
   378
        (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
   379
      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
   380
      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
   381
      new Nodes(graph3.map_node(name, _ => node))
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   382
    }
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   383
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   384
    def iterator: Iterator[(Node.Name, Node)] =
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   385
      graph.iterator.map({ case (name, (node, _)) => (name, node) })
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   386
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   387
    def commands_loading(file_name: Node.Name): List[Command] =
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   388
      (for {
56372
fadb0fef09d7 more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents: 56354
diff changeset
   389
        (_, node) <- iterator
56314
9a513737a0b2 tuned signature;
wenzelm
parents: 56309
diff changeset
   390
        cmd <- node.load_commands.iterator
54530
2c1440f70028 ranges of thy_load commands count as visible within perspective;
wenzelm
parents: 54528
diff changeset
   391
        name <- cmd.blobs_names.iterator
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   392
        if name == file_name
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   393
      } yield cmd).toList
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54521
diff changeset
   394
46942
f5c2d66faa04 basic support for outer syntax keywords in theory header;
wenzelm
parents: 46941
diff changeset
   395
    def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   396
    def topological_order: List[Node.Name] = graph.topological_order
56337
520148f9921d tuned output;
wenzelm
parents: 56336
diff changeset
   397
520148f9921d tuned output;
wenzelm
parents: 56336
diff changeset
   398
    override def toString: String = topological_order.mkString("Nodes(", ",", ")")
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   399
  }
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   400
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   401
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   402
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   403
  /** versioning **/
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   404
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   405
  /* particular document versions */
34485
6475bfb4ff99 joined Document with ProofDocument;
wenzelm
parents: 34483
diff changeset
   406
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   407
  object Version
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   408
  {
46681
c083a3f621c0 more abstract class Document.Version;
wenzelm
parents: 46680
diff changeset
   409
    val init: Version = new Version()
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 57976
diff changeset
   410
    def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   411
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   412
    def purge(f: Version => Option[Version], versions: Map[Document_ID.Version, Version])
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   413
      : Map[Document_ID.Version, Version] =
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   414
      (versions /: (for ((id, v) <- versions.iterator; v1 <- f(v)) yield (id, v1)))(_ + _)
68066
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   415
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   416
    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
   417
      : Future[Version] =
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   418
    {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   419
      if (future.is_finished) {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   420
        val version = future.join
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   421
        versions.get(version.id) match {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   422
          case Some(version1) if !(version eq version1) => Future.value(version1)
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   423
          case _ => future
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   424
        }
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   425
      }
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   426
      else future
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   427
    }
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   428
  }
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   429
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   430
  final class Version private(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   431
    val id: Document_ID.Version = Document_ID.none,
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46712
diff changeset
   432
    val nodes: Nodes = Nodes.empty)
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46940
diff changeset
   433
  {
55777
90484dff4dc4 tuned output;
wenzelm
parents: 55710
diff changeset
   434
    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
   435
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   436
    def purge_hidden: Option[Version] =
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   437
      nodes.purge(nodes.is_hidden(_)).map(new Version(id, _))
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   438
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   439
    def purge_blobs(blobs: Set[Node.Name]): Option[Version] =
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   440
      nodes.purge(name => nodes(name).get_blob.isDefined && !blobs.contains(name)).
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   441
        map(new Version(id, _))
46941
c0f776b661fa maintain Version.syntax within document state;
wenzelm
parents: 46940
diff changeset
   442
  }
34660
e0561943bfc9 Change consisting of a list of Edits
immler@in.tum.de
parents: 34657
diff changeset
   443
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34855
diff changeset
   444
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   445
  /* changes of plain text, eventually resulting in document edits */
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   446
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   447
  object Change
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   448
  {
46678
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   449
    val init: Change = new Change()
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   450
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   451
    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
   452
      new Change(Some(previous), edits.reverse, version)
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   453
  }
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   454
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   455
  final class Change private(
46677
wenzelm
parents: 46208
diff changeset
   456
    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
   457
    val rev_edits: List[Edit_Text] = Nil,
46677
wenzelm
parents: 46208
diff changeset
   458
    val version: Future[Version] = Future.value(Version.init))
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   459
  {
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   460
    def is_finished: Boolean =
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   461
      (previous match { case None => true case Some(future) => future.is_finished }) &&
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   462
      version.is_finished
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   463
46678
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   464
    def truncate: Change = new Change(None, Nil, version)
68066
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   465
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   466
    def purge(versions: Map[Document_ID.Version, Version]): Option[Change] =
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   467
    {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   468
      val previous1 = previous.map(Version.purge_future(versions, _))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   469
      val version1 = Version.purge_future(versions, version)
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   470
      if ((previous eq previous1) && (version eq version1)) None
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   471
      else Some(new Change(previous1, rev_edits, version1))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   472
    }
38227
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   473
  }
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   474
6bbb42843b6e concentrate structural document notions in document.scala;
wenzelm
parents: 38220
diff changeset
   475
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   476
  /* history navigation */
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   477
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   478
  object History
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   479
  {
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   480
    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
   481
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   482
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   483
  final class History private(
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   484
    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
   485
  {
67114
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   486
    override def toString: String = "History(" + undo_list.length + ")"
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   487
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   488
    def tip: Change = undo_list.head
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   489
    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
   490
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   491
    def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   492
    {
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   493
      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
   494
      val (retained, dropped) = undo_list.splitAt(n max retain)
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   495
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   496
      retained.splitAt(retained.length - 1) match {
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   497
        case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   498
        case _ => None
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   499
      }
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   500
    }
68066
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   501
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   502
    def purge(versions: Map[Document_ID.Version, Version]): History =
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   503
    {
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   504
      val undo_list1 = undo_list.map(_.purge(versions))
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   505
      if (undo_list1.forall(_.isEmpty)) this
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   506
      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
   507
    }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   508
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   509
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   510
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   511
  /* snapshot */
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   512
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   513
  object Snapshot
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   514
  {
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   515
    val init = State.init.snapshot()
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   516
  }
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   517
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   518
  abstract class Snapshot
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   519
  {
64798
wenzelm
parents: 64797
diff changeset
   520
    def state: State
wenzelm
parents: 64797
diff changeset
   521
    def version: Version
wenzelm
parents: 64797
diff changeset
   522
    def is_outdated: Boolean
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   523
38427
7066fbd315ae some derived operations on Text.Range;
wenzelm
parents: 38426
diff changeset
   524
    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
   525
    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
   526
    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
   527
    def revert(range: Text.Range): Text.Range
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   528
64798
wenzelm
parents: 64797
diff changeset
   529
    def node_name: Node.Name
wenzelm
parents: 64797
diff changeset
   530
    def node: Node
66379
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   531
    def node_consolidated: Boolean
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 65471
diff changeset
   532
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   533
    def commands_loading: List[Command]
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   534
    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
   535
    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
   536
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   537
    def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 65471
diff changeset
   538
64665
wenzelm
parents: 63584
diff changeset
   539
    def find_command(id: Document_ID.Generic): Option[(Node, Command)]
wenzelm
parents: 63584
diff changeset
   540
    def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
wenzelm
parents: 63584
diff changeset
   541
      : Option[Line.Node_Position]
wenzelm
parents: 63584
diff changeset
   542
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   543
    def cumulate[A](
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   544
      range: Text.Range,
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   545
      info: A,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
   546
      elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
   547
      result: List[Command.State] => (A, Text.Markup) => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   548
      status: Boolean = false): List[Text.Info[A]]
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   549
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   550
    def select[A](
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   551
      range: Text.Range,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
   552
      elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
   553
      result: List[Command.State] => Text.Markup => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
   554
      status: Boolean = false): List[Text.Info[A]]
65332
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
   555
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
   556
    def command_results(range: Text.Range): Command.Results
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
   557
    def command_results(command: Command): Command.Results
38424
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   558
  }
940a404e45e2 moved History/Snapshot to document.scala;
wenzelm
parents: 38418
diff changeset
   559
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   560
64814
wenzelm
parents: 64799
diff changeset
   561
  /* model */
wenzelm
parents: 64799
diff changeset
   562
65221
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   563
  trait Session
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   564
  {
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   565
    def resources: Resources
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   566
  }
6af51a47545b more abstract module Document;
wenzelm
parents: 65199
diff changeset
   567
64814
wenzelm
parents: 64799
diff changeset
   568
  trait Model
wenzelm
parents: 64799
diff changeset
   569
  {
wenzelm
parents: 64799
diff changeset
   570
    def session: Session
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   571
    def is_stable: Boolean
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   572
    def snapshot(): Snapshot
64814
wenzelm
parents: 64799
diff changeset
   573
65356
wenzelm
parents: 65355
diff changeset
   574
    def node_name: Node.Name
64814
wenzelm
parents: 64799
diff changeset
   575
    def is_theory: Boolean = node_name.is_theory
wenzelm
parents: 64799
diff changeset
   576
    override def toString: String = node_name.toString
wenzelm
parents: 64799
diff changeset
   577
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66849
diff changeset
   578
    def get_text(range: Text.Range): Option[String]
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66043
diff changeset
   579
64815
wenzelm
parents: 64814
diff changeset
   580
    def node_required: Boolean
65356
wenzelm
parents: 65355
diff changeset
   581
    def get_blob: Option[Blob]
67247
3a9651318015 clarified signature;
wenzelm
parents: 67114
diff changeset
   582
    def is_bibtex: Boolean = node_name.is_bibtex
67309
0e322d7325c3 tuned signature;
wenzelm
parents: 67293
diff changeset
   583
    def is_bibtex_theory: Boolean = node_name.is_bibtex_theory
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66114
diff changeset
   584
    def bibtex_entries: List[Text.Info[String]]
64815
wenzelm
parents: 64814
diff changeset
   585
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   586
    def node_edits(
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   587
      node_header: Node.Header,
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   588
      text_edits: List[Text.Edit],
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
   589
      perspective: Node.Perspective_Text): List[Edit_Text] =
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   590
    {
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   591
      val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   592
        get_blob match {
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   593
          case None =>
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   594
            List(
65356
wenzelm
parents: 65355
diff changeset
   595
              Node.Deps(
66773
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   596
                if (session.resources.session_base.loaded_theory(node_name)) {
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   597
                  node_header.append_errors(
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   598
                    List("Cannot update finished theory " + quote(node_name.theory)))
0cd29455a5e8 tuned signature;
wenzelm
parents: 66716
diff changeset
   599
                }
64827
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   600
                else node_header),
65356
wenzelm
parents: 65355
diff changeset
   601
              Node.Edits(text_edits), perspective)
wenzelm
parents: 65355
diff changeset
   602
          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
   603
        }
4ef1eb75f1cd uniform Document.Model.node_edits (without void edits);
wenzelm
parents: 64819
diff changeset
   604
      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
   605
    }
64814
wenzelm
parents: 64799
diff changeset
   606
  }
wenzelm
parents: 64799
diff changeset
   607
wenzelm
parents: 64799
diff changeset
   608
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   609
  /** global state -- document structure, execution process, editing history **/
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55801
diff changeset
   610
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   611
  type Assign_Update =
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   612
    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
   613
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   614
  object State
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   615
  {
38373
wenzelm
parents: 38370
diff changeset
   616
    class Fail(state: State) extends Exception
wenzelm
parents: 38370
diff changeset
   617
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   618
    object Assignment
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   619
    {
46683
fb160aa7a9a8 more abstract class Document.State.Assignment;
wenzelm
parents: 46682
diff changeset
   620
      val init: Assignment = new Assignment()
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   621
    }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   622
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   623
    final class Assignment private(
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   624
      val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
46677
wenzelm
parents: 46208
diff changeset
   625
      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
   626
    {
67114
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   627
      override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
3d8626cbaff8 tuned output;
wenzelm
parents: 67112
diff changeset
   628
44477
086bb1083552 maintain last_execs assignment on Scala side;
wenzelm
parents: 44476
diff changeset
   629
      def check_finished: Assignment = { require(is_finished); this }
47388
fe4b245af74c discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents: 46997
diff changeset
   630
      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
   631
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   632
      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
   633
      {
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
   634
        require(!is_finished)
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   635
        val command_execs1 =
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   636
          (command_execs /: update) {
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   637
            case (res, (command_id, exec_ids)) =>
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   638
              if (exec_ids.isEmpty) res - command_id
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   639
              else res + (command_id -> exec_ids)
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   640
          }
47388
fe4b245af74c discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents: 46997
diff changeset
   641
        new Assignment(command_execs1, true)
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
   642
      }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   643
    }
46682
4a74fbd6f28b tuned signature;
wenzelm
parents: 46681
diff changeset
   644
4a74fbd6f28b tuned signature;
wenzelm
parents: 46681
diff changeset
   645
    val init: State =
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   646
      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   647
  }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   648
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46684
diff changeset
   649
  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
   650
    /*reachable versions*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   651
    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
   652
    /*inlined auxiliary files*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   653
    blobs: Set[SHA1.Digest] = Set.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
   654
    /*static markup from define_command*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   655
    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
   656
    /*dynamic markup from execution*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   657
    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
   658
    /*command-exec assignment for each version*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   659
    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
   660
    /*commands with markup produced by other commands (imm_succs)*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   661
    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
   662
    /*explicit (linear) history*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   663
    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
   664
    /*intermediate state between remove_versions/removed_versions*/
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59702
diff changeset
   665
    removing_versions: Boolean = false)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   666
  {
38373
wenzelm
parents: 38370
diff changeset
   667
    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
   668
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   669
    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
   670
    {
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   671
      val id = version.id
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   672
      copy(versions = versions + (id -> version),
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   673
        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
   674
    }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   675
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   676
    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
   677
    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
   678
38373
wenzelm
parents: 38370
diff changeset
   679
    def define_command(command: Command): State =
wenzelm
parents: 38370
diff changeset
   680
    {
wenzelm
parents: 38370
diff changeset
   681
      val id = command.id
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49346
diff changeset
   682
      copy(commands = commands + (id -> command.init_state))
38373
wenzelm
parents: 38370
diff changeset
   683
    }
wenzelm
parents: 38370
diff changeset
   684
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   685
    def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
44582
479c07072992 tuned signature;
wenzelm
parents: 44581
diff changeset
   686
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   687
    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
   688
    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
   689
    def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   690
    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
   691
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
   692
    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
   693
      id == st.command.id ||
a40e67ce4f84 clarified valid_id: always standardize towards static command.id;
wenzelm
parents: 56176
diff changeset
   694
      (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
   695
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   696
    private def other_id(id: Document_ID.Generic)
63032
e0fa59bbc956 reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents: 63020
diff changeset
   697
      : Option[(Symbol.Text_Chunk.Id, Symbol.Text_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
   698
      (execs.get(id) orElse commands.get(id)).map(st =>
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56743
diff changeset
   699
        ((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
   700
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   701
    private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   702
      (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
   703
        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
   704
67825
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67309
diff changeset
   705
    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
   706
      : (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
   707
    {
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   708
      execs.get(id) match {
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44443
diff changeset
   709
        case Some(st) =>
67825
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67309
diff changeset
   710
          val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
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
   711
          val execs1 = execs + (id -> new_st)
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   712
          (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   713
        case None =>
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   714
          commands.get(id) match {
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   715
            case Some(st) =>
67825
f9c071cc958b update XML cache for slightly modified messages;
wenzelm
parents: 67309
diff changeset
   716
              val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
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
   717
              val commands1 = commands + (id -> new_st)
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   718
              (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   719
            case None => fail
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   720
          }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   721
      }
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
   722
    }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   723
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   724
    def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   725
    {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   726
      execs.get(id) match {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   727
        case Some(st) =>
68114
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   728
          st.add_export(entry) match {
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   729
            case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   730
            case None => fail
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   731
          }
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   732
        case None =>
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   733
          commands.get(id) match {
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   734
            case Some(st) =>
68114
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   735
              st.add_export(entry) match {
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   736
                case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   737
                case None => fail
ce7f35406f37 more robust: self-export only;
wenzelm
parents: 68101
diff changeset
   738
              }
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   739
            case None => fail
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   740
          }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   741
      }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   742
    }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68066
diff changeset
   743
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   744
    def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   745
    {
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   746
      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
   747
52566
52a0eacf04d1 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents: 52564
diff changeset
   748
      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
   749
          : 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
   750
        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
   751
44543
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   752
      val (changed_commands, new_execs) =
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   753
        ((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
   754
          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
   755
            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
   756
            val command = st.command
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   757
            val commands2 = command :: commands1
44543
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   758
            val execs2 =
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   759
              exec match {
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   760
                case Nil => execs1
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   761
                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
   762
                  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
   763
                    (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
   764
              }
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   765
            (commands2, execs2)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   766
        }
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52531
diff changeset
   767
      val new_assignment = the_assignment(version).assign(update)
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   768
      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
   769
44543
ba8f24f7156e de-assigned commands also count as changed;
wenzelm
parents: 44484
diff changeset
   770
      (changed_commands, new_state)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   771
    }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   772
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38414
diff changeset
   773
    def is_assigned(version: Version): Boolean =
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   774
      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
   775
        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
   776
        case None => false
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   777
      }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   778
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   779
    def is_stable(change: Change): Boolean =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   780
      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
   781
46944
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   782
    def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   783
    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
   784
    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
   785
      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
   786
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44443
diff changeset
   787
    def continue_history(
56711
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   788
      previous: Future[Version],
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   789
      edits: List[Edit_Text],
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   790
      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
   791
    {
46678
c2dba08548f9 more abstract class Document.Change;
wenzelm
parents: 46677
diff changeset
   792
      val change = Change.make(previous, edits, version)
56711
ef3d00153e3b tuned signature;
wenzelm
parents: 56590
diff changeset
   793
      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
   794
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   795
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
   796
    def remove_versions(retain: Int = 0): (List[Version], State) =
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   797
    {
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   798
      history.prune(is_stable, retain) match {
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   799
        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
   800
          val old_versions = dropped.map(change => change.version.get_finished)
59319
wenzelm
parents: 59077
diff changeset
   801
          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
   802
          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
   803
          (old_versions, state1)
46679
bce11e807488 more abstract class Document.History;
wenzelm
parents: 46678
diff changeset
   804
        case None => fail
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   805
      }
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   806
    }
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   807
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52527
diff changeset
   808
    def removed_versions(removed: List[Document_ID.Version]): State =
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   809
    {
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   810
      val versions1 = Version.purge(_.purge_hidden, versions -- removed)
67110
3156faac30a7 purge hidden nodes more thoroughly: is_hidden may become true only later;
wenzelm
parents: 67014
diff changeset
   811
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   812
      val assignments1 = assignments -- removed
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   813
      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
   814
      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
   815
      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
   816
      var execs1 = Map.empty[Document_ID.Exec, Command.State]
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   817
      for {
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   818
        (version_id, version) <- versions1.iterator
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46944
diff changeset
   819
        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
   820
        (_, node) <- version.nodes.iterator
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   821
        command <- node.commands.iterator
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   822
      } {
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   823
        for ((name, digest) <- command.blobs_defined) {
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   824
          blobs1_names += name
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   825
          blobs1 += digest
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   826
        }
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 54515
diff changeset
   827
52568
wenzelm
parents: 52566
diff changeset
   828
        if (!commands1.isDefinedAt(command.id))
wenzelm
parents: 52566
diff changeset
   829
          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
   830
52568
wenzelm
parents: 52566
diff changeset
   831
        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
   832
          if (!execs1.isDefinedAt(exec_id))
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   833
            execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   834
        }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   835
      }
67112
deb2fcbda16e removed inaccessible blobs from Document.Nodes;
wenzelm
parents: 67110
diff changeset
   836
68066
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   837
      val versions2 = Version.purge(_.purge_blobs(blobs1_names), versions1)
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   838
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
   839
      copy(
68066
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   840
        versions = versions2,
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
   841
        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
   842
        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
   843
        execs = execs1,
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   844
        commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
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
   845
        assignments = assignments1,
68066
63f03ee4057e purge history more thoroughly (see also 3156faac30a7);
wenzelm
parents: 67943
diff changeset
   846
        history = history.purge(versions2),
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
   847
        removing_versions = false)
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   848
    }
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44672
diff changeset
   849
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
   850
    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
   851
      : List[(Document_ID.Generic, Command.State)] =
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   852
    {
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   853
      require(is_assigned(version))
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   854
      try {
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   855
        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
   856
          .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
   857
            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
   858
            case res => res
52527
dbac84eab3bc separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents: 52508
diff changeset
   859
          }
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   860
      }
47395
e6261a493f04 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents: 47388
diff changeset
   861
      catch {
e6261a493f04 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents: 47388
diff changeset
   862
        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
   863
          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
   864
          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
   865
      }
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   866
    }
a3255c85327b crude display of node status;
wenzelm
parents: 44607
diff changeset
   867
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
   868
    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
   869
    {
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   870
      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
   871
      val others =
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   872
        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
   873
          (for {
56475
710dee42b3d0 tuned signature;
wenzelm
parents: 56473
diff changeset
   874
            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
   875
            (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
   876
            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
   877
          } 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
   878
        }
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   879
        else Nil
56489
wenzelm
parents: 56475
diff changeset
   880
      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
   881
    }
8eda56033203 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents: 56468
diff changeset
   882
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 56298
diff changeset
   883
    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
   884
      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
   885
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   886
    def command_markup(version: Version, command: Command, index: Command.Markup_Index,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
   887
        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
   888
      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
   889
66041
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   890
    def markup_to_XML(
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   891
      version: Version,
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   892
      node_name: Node.Name,
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   893
      range: Text.Range,
66041
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   894
      elements: Markup.Elements): XML.Body =
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   895
    {
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   896
      val node = version.nodes(node_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   897
      if (node_name.is_theory) {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   898
        val markup_index = Command.Markup_Index.markup
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   899
        (for {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   900
          command <- node.commands.iterator
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   901
          command_range <- command.range.try_restrict(range).iterator
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   902
          markup = command_markup(version, command, markup_index, command_range, elements)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   903
          tree <- markup.to_XML(command_range, command.source, elements).iterator
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   904
        } yield tree).toList
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   905
      }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   906
      else {
67265
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67264
diff changeset
   907
        val node_source = node.source
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   908
        Text.Range(0, node_source.length).try_restrict(range) match {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   909
          case None => Nil
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   910
          case Some(node_range) =>
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   911
            val markup =
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   912
              version.nodes.commands_loading(node_name).headOption match {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   913
                case None => Markup_Tree.empty
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   914
                case Some(command) =>
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   915
                  val chunk_name = Symbol.Text_Chunk.File(node_name.node)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   916
                  val markup_index = Command.Markup_Index(false, chunk_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   917
                  command_markup(version, command, markup_index, node_range, elements)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   918
              }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   919
            markup.to_XML(node_range, node_source, elements)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   920
        }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
   921
      }
66041
c49bd8bb4839 clarified signature;
wenzelm
parents: 66040
diff changeset
   922
    }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   923
66379
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   924
    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
   925
      !name.is_theory ||
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   926
        version.nodes(name).commands.reverse.iterator.
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   927
          flatMap(command_states(version, _)).exists(_.consolidated)
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   928
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   929
    // persistent user-view
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 48923
diff changeset
   930
    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
   931
      : Snapshot =
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   932
    {
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44642
diff changeset
   933
      val stable = recent_stable
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   934
      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
   935
57620
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   936
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   937
      /* pending edits and unstable changes */
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   938
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   939
      val rev_pending_changes =
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   940
        for {
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   941
          change <- history.undo_list.takeWhile(_ != stable)
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   942
          (a, edits) <- change.rev_edits
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   943
          if a == name
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   944
        } yield edits
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   945
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   946
      val edits =
64819
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
   947
        (pending_edits /: rev_pending_changes)({
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
   948
          case (edits, Node.Edits(es)) => es ::: edits
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
   949
          case (edits, _) => edits
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
   950
        })
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   951
      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
   952
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   953
      new Snapshot
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
   954
      {
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   955
        /* global information */
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   956
64798
wenzelm
parents: 64797
diff changeset
   957
        val state: State = State.this
wenzelm
parents: 64797
diff changeset
   958
        val version: Version = stable.version.get_finished
wenzelm
parents: 64797
diff changeset
   959
        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
   960
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   961
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   962
        /* local node content */
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
   963
64819
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
   964
        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
bebe7a164068 obsolete;
wenzelm
parents: 64815
diff changeset
   965
        def revert(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
   966
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   967
        def convert(range: Text.Range) = range.map(convert(_))
c30ab960875e more explicit treatment of cleared nodes (removal is implicit);
wenzelm
parents: 57619
diff changeset
   968
        def revert(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
   969
64798
wenzelm
parents: 64797
diff changeset
   970
        val node_name: Node.Name = name
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   971
        val node: Node = version.nodes(name)
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52918
diff changeset
   972
66379
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   973
        def node_consolidated: Boolean = state.node_consolidated(version, node_name)
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66195
diff changeset
   974
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   975
        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
   976
          if (node_name.is_theory) Nil
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   977
          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
   978
64799
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   979
        def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   980
          (for {
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   981
            cmd <- node.load_commands.iterator
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   982
            blob_name <- cmd.blobs_names.iterator
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   983
            if pred(blob_name)
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   984
            start <- node.command_start(cmd)
c0c648911f1a misc tuning and clarification;
wenzelm
parents: 64798
diff changeset
   985
          } yield convert(cmd.proper_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
   986
65199
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
   987
        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
   988
          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
   989
            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
   990
            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
   991
            if (iterator.hasNext) {
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
   992
              val (command0, _) = iterator.next
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
   993
              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
   994
            }
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
   995
            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
   996
          }
6bd7081f8319 clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents: 65196
diff changeset
   997
          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
   998
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   999
        def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67251
diff changeset
  1000
          state.markup_to_XML(version, node_name, range, elements)
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 65471
diff changeset
  1001
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1002
64665
wenzelm
parents: 63584
diff changeset
  1003
        /* find command */
wenzelm
parents: 63584
diff changeset
  1004
wenzelm
parents: 63584
diff changeset
  1005
        def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
wenzelm
parents: 63584
diff changeset
  1006
          state.commands.get(id) orElse state.execs.get(id) match {
wenzelm
parents: 63584
diff changeset
  1007
            case None => None
wenzelm
parents: 63584
diff changeset
  1008
            case Some(st) =>
wenzelm
parents: 63584
diff changeset
  1009
              val command = st.command
wenzelm
parents: 63584
diff changeset
  1010
              val node = version.nodes(command.node_name)
wenzelm
parents: 63584
diff changeset
  1011
              if (node.commands.contains(command)) Some((node, command)) else None
wenzelm
parents: 63584
diff changeset
  1012
          }
wenzelm
parents: 63584
diff changeset
  1013
wenzelm
parents: 63584
diff changeset
  1014
        def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
wenzelm
parents: 63584
diff changeset
  1015
            : Option[Line.Node_Position] =
wenzelm
parents: 63584
diff changeset
  1016
          for ((node, command) <- find_command(id))
wenzelm
parents: 63584
diff changeset
  1017
          yield {
wenzelm
parents: 63584
diff changeset
  1018
            val name = command.node_name.node
wenzelm
parents: 63584
diff changeset
  1019
            val sources_iterator =
wenzelm
parents: 63584
diff changeset
  1020
              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm
parents: 63584
diff changeset
  1021
                (if (offset == 0) Iterator.empty
wenzelm
parents: 63584
diff changeset
  1022
                 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
  1023
            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
64665
wenzelm
parents: 63584
diff changeset
  1024
            Line.Node_Position(name, pos)
wenzelm
parents: 63584
diff changeset
  1025
          }
wenzelm
parents: 63584
diff changeset
  1026
wenzelm
parents: 63584
diff changeset
  1027
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1028
        /* cumulate markup */
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1029
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1030
        def cumulate[A](
55649
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1031
          range: Text.Range,
1532ab0dc67b more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents: 55620
diff changeset
  1032
          info: A,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
  1033
          elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1034
          result: List[Command.State] => (A, Text.Markup) => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1035
          status: Boolean = false): List[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45243
diff changeset
  1036
        {
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
  1037
          val former_range = revert(range).inflate_singularity
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56398
diff changeset
  1038
          val (chunk_name, command_iterator) =
65187
wenzelm
parents: 64867
diff changeset
  1039
            commands_loading.headOption match {
wenzelm
parents: 64867
diff changeset
  1040
              case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
wenzelm
parents: 64867
diff changeset
  1041
              case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1042
            }
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56398
diff changeset
  1043
          val markup_index = Command.Markup_Index(status, chunk_name)
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1044
          (for {
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56372
diff changeset
  1045
            (command, command_start) <- command_iterator
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56398
diff changeset
  1046
            chunk <- command.chunks.get(chunk_name).iterator
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1047
            states = state.command_states(version, command)
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1048
            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
  1049
            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
  1050
            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
  1051
            Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
56309
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1052
              {
5003ea266aef tuned -- avoid code duplication;
wenzelm
parents: 56301
diff changeset
  1053
                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
  1054
              }).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
  1055
            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
  1056
          } yield Text.Info(r1, a)).toList
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45243
diff changeset
  1057
        }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45243
diff changeset
  1058
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1059
        def select[A](
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1060
          range: Text.Range,
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56711
diff changeset
  1061
          elements: Markup.Elements,
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1062
          result: List[Command.State] => Text.Markup => Option[A],
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1063
          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
  1064
        {
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1065
          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
  1066
          {
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56337
diff changeset
  1067
            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
  1068
            (_: 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
  1069
              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
  1070
                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
  1071
                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
  1072
              }
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50204
diff changeset
  1073
          }
55651
fa42cf3fe79b tuned signature -- avoid redundancy and confusion of flags;
wenzelm
parents: 55650
diff changeset
  1074
          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
  1075
            yield Text.Info(r, x)
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38841
diff changeset
  1076
        }
55800
wenzelm
parents: 55783
diff changeset
  1077
wenzelm
parents: 55783
diff changeset
  1078
65332
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1079
        /* command results */
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1080
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1081
        def command_results(range: Text.Range): Command.Results =
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1082
          Command.State.merge_results(
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1083
            select[List[Command.State]](range, Markup.Elements.full, command_states =>
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1084
              { case _ => Some(command_states) }).flatMap(_.info))
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1085
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1086
        def command_results(command: Command): Command.Results =
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1087
          state.command_results(version, command)
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1088
7dbb780f24a9 tuned signature;
wenzelm
parents: 65221
diff changeset
  1089
55800
wenzelm
parents: 55783
diff changeset
  1090
        /* output */
wenzelm
parents: 55783
diff changeset
  1091
wenzelm
parents: 55783
diff changeset
  1092
        override def toString: String =
wenzelm
parents: 55783
diff changeset
  1093
          "Snapshot(node = " + node_name.node + ", version = " + version.id +
wenzelm
parents: 55783
diff changeset
  1094
            (if (is_outdated) ", outdated" else "") + ")"
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38569
diff changeset
  1095
      }
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37849
diff changeset
  1096
    }
34485
6475bfb4ff99 joined Document with ProofDocument;
wenzelm
parents: 34483
diff changeset
  1097
  }
34840
6c5560d48561 more precise treatment of document/state assigment;
wenzelm
parents: 34838
diff changeset
  1098
}