--- a/src/Pure/PIDE/document_status.scala Sat Aug 18 15:02:08 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sat Aug 18 17:29:49 2018 +0200
@@ -185,8 +185,8 @@
session_base: Sessions.Base,
state: Document.State,
version: Document.Version,
- domain: Option[Set[Document.Node.Name]],
- trim: Boolean): Option[(Nodes_Status, List[Document.Node.Name])] =
+ domain: Option[Set[Document.Node.Name]] = None,
+ trim: Boolean = false): Option[(Nodes_Status, List[Document.Node.Name])] =
{
val nodes = version.nodes
val update_iterator =
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 15:02:08 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 17:29:49 2018 +0200
@@ -219,7 +219,8 @@
for {
(nodes_status1, nodes_list1) <-
- nodes_status.update(session_base, snapshot.state, snapshot.version, domain, trim)
+ nodes_status.update(
+ session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
} { nodes_status = nodes_status1; status.listData = nodes_list1 }
}