--- a/src/Pure/PIDE/document.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/PIDE/document.scala Mon Apr 03 12:41:06 2017 +0200
@@ -503,7 +503,7 @@
case None =>
List(
Document.Node.Deps(
- if (session.resources.base.loaded_theories(node_name.theory))
+ if (session.resources.base.loaded_theory(node_name))
node_header.error("Cannot update finished theory " + quote(node_name.theory))
else node_header),
Document.Node.Edits(text_edits), perspective)
--- a/src/Pure/PIDE/resources.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 03 12:41:06 2017 +0200
@@ -88,7 +88,7 @@
(base.known_theories.get(thy1) orElse
base.known_theories.get(thy2) orElse
base.known_theories.get(Long_Name.base_name(thy1))) match {
- case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
+ case Some(name) if base.loaded_theory(name) => dummy_name(name.theory)
case Some(name) => name
case None =>
val path = Path.explode(s)
@@ -155,7 +155,7 @@
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
(for {
(node_name, node) <- nodes.iterator
- if !base.loaded_theories(node_name.theory)
+ if !base.loaded_theory(node_name)
cmd <- node.load_commands.iterator
name <- cmd.blobs_undefined.iterator
} yield name).toList
--- a/src/Pure/Thy/sessions.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 03 12:41:06 2017 +0200
@@ -47,6 +47,10 @@
syntax: Outer_Syntax = Outer_Syntax.empty,
sources: List[(Path, SHA1.Digest)] = Nil,
session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+ {
+ def loaded_theory(name: Document.Node.Name): Boolean =
+ loaded_theories.contains(name.theory)
+ }
sealed case class Deps(deps: Map[String, Base])
{
--- a/src/Pure/Thy/thy_info.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Mon Apr 03 12:41:06 2017 +0200
@@ -118,7 +118,7 @@
required_by(initiators) + Position.here(require_pos)
val required1 = required + thy
- if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
+ if (required.seen(name) || resources.base.loaded_theory(name)) required1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
--- a/src/Pure/Thy/thy_syntax.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Apr 03 12:41:06 2017 +0200
@@ -300,7 +300,7 @@
doc_blobs.get(name) orElse previous.nodes(name).get_blob
def can_import(name: Document.Node.Name): Boolean =
- resources.base.loaded_theories(name.theory) || nodes0(name).has_header
+ resources.base.loaded_theory(name) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 03 12:41:06 2017 +0200
@@ -192,7 +192,7 @@
}
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
+ if (!name.is_theory || PIDE.resources.base.loaded_theory(name) || node.is_empty)
status
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
--- a/src/Tools/jEdit/src/timing_dockable.scala Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 12:41:06 2017 +0200
@@ -187,7 +187,7 @@
}
val nodes_timing1 =
(nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.resources.base.loaded_theories(name.theory)) timing1
+ if (PIDE.resources.base.loaded_theory(name)) timing1
else {
val node_timing =
Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)