--- a/src/Pure/Thy/thy_load.scala Mon Nov 18 23:26:15 2013 +0100
+++ b/src/Pure/Thy/thy_load.scala Mon Nov 18 23:46:59 2013 +0100
@@ -21,23 +21,23 @@
def is_ok(str: String): Boolean =
try { thy_path(Path.explode(str)); true }
catch { case ERROR(_) => false }
-
-
- /* document node names */
-
- def path_node_name(raw_path: Path): Document.Node.Name =
- {
- val path = raw_path.expand
- val node = path.implode
- val dir = path.dir.implode
- val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
- Document.Node.Name(node, dir, theory)
- }
}
class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
{
+ /* document node names */
+
+ def node_name(raw_path: Path): Document.Node.Name =
+ {
+ val path = raw_path.expand
+ val node = path.implode
+ val dir = path.dir.implode
+ val theory = Thy_Header.thy_name(node).getOrElse("")
+ Document.Node.Name(node, dir, theory)
+ }
+
+
/* file-system operations */
def append(dir: String, source_path: Path): String =
--- a/src/Pure/Tools/build.scala Mon Nov 18 23:26:15 2013 +0100
+++ b/src/Pure/Tools/build.scala Mon Nov 18 23:46:59 2013 +0100
@@ -417,7 +417,8 @@
val parent = deps(parent_name)
(parent.loaded_theories, parent.syntax)
}
- val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
+ val thy_load = new Thy_Load(preloaded, parent_syntax)
+ val thy_info = new Thy_Info(thy_load)
if (verbose || list_files) {
val groups =
@@ -429,7 +430,7 @@
val thy_deps =
thy_info.dependencies(
info.theories.map(_._2).flatten.
- map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
+ map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
val loaded_theories = thy_deps.loaded_theories
val keywords = thy_deps.keywords