--- a/src/Pure/PIDE/document_status.scala Sat Aug 18 14:53:21 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sat Aug 18 14:55:53 2018 +0200
@@ -185,13 +185,13 @@
session_base: Sessions.Base,
state: Document.State,
version: Document.Version,
- restriction: Option[Set[Document.Node.Name]],
+ domain: Option[Set[Document.Node.Name]],
trim: Boolean): Option[(Nodes_Status, List[Document.Node.Name])] =
{
val nodes = version.nodes
val update_iterator =
for {
- name <- restriction.getOrElse(nodes.domain).iterator
+ name <- domain.getOrElse(nodes.domain).iterator
if !Sessions.is_hidden(name) &&
!session_base.loaded_theory(name) &&
!nodes.is_suppressed(name) &&
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 14:53:21 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 14:55:53 2018 +0200
@@ -210,9 +210,7 @@
}
status.renderer = new Node_Renderer
- private def handle_update(
- restriction: Option[Set[Document.Node.Name]] = None,
- trim: Boolean = false)
+ private def handle_update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false)
{
GUI_Thread.require {}
@@ -221,7 +219,7 @@
for {
(nodes_status1, nodes_list) <-
nodes_status.update(
- PIDE.resources.session_base, snapshot.state, snapshot.version, restriction, trim)
+ PIDE.resources.session_base, snapshot.state, snapshot.version, domain, trim)
} {
nodes_status = nodes_status1
status.listData = nodes_list
@@ -245,9 +243,7 @@
}
case changed: Session.Commands_Changed =>
- GUI_Thread.later {
- handle_update(restriction = Some(changed.nodes), trim = changed.assignment)
- }
+ GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
}
override def init()