# HG changeset patch
# User wenzelm
# Date 1527452503 -7200
# Node ID 0b5a2347791165ee2e3247e6500dbeb40ff2d714
# Parent  2c3ce27cf4a8fe7d074990ff8a90599e790229c0
clarified signature -- avoid confusion with Resources.is_hidden;

diff -r 2c3ce27cf4a8 -r 0b5a23477911 src/Pure/PIDE/document.scala
--- 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]
diff -r 2c3ce27cf4a8 -r 0b5a23477911 src/Tools/jEdit/src/theories_dockable.scala
--- 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