--- a/src/Pure/PIDE/document.scala Sun May 27 13:42:01 2018 +0200
+++ b/src/Pure/PIDE/document.scala Sun May 27 22:21:43 2018 +0200
@@ -358,7 +358,7 @@
def apply(name: Node.Name): Node =
graph.default_node(name, Node.empty).get_node(name)
- def is_hidden(name: Node.Name): Boolean =
+ def is_suppressed(name: Node.Name): Boolean =
{
val graph1 = graph.default_node(name, Node.empty)
graph1.is_maximal(name) && graph1.get_node(name).is_empty
@@ -433,8 +433,8 @@
{
override def toString: String = "Version(" + id + ")"
- def purge_hidden: Option[Version] =
- nodes.purge(nodes.is_hidden(_)).map(new Version(id, _))
+ def purge_suppressed: Option[Version] =
+ nodes.purge(nodes.is_suppressed(_)).map(new Version(id, _))
def purge_blobs(blobs: Set[Node.Name]): Option[Version] =
nodes.purge(name => nodes(name).get_blob.isDefined && !blobs.contains(name)).
@@ -807,7 +807,7 @@
def removed_versions(removed: List[Document_ID.Version]): State =
{
- val versions1 = Version.purge(_.purge_hidden, versions -- removed)
+ val versions1 = Version.purge(_.purge_suppressed, versions -- removed)
val assignments1 = assignments -- removed
var blobs1_names = Set.empty[Node.Name]
--- a/src/Tools/jEdit/src/theories_dockable.scala Sun May 27 13:42:01 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sun May 27 22:21:43 2018 +0200
@@ -245,7 +245,7 @@
})
val nodes_status2 =
- nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
+ nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_))
if (nodes_status != nodes_status2) {
nodes_status = nodes_status2