# HG changeset patch
# User wenzelm
# Date 1384814819 -3600
# Node ID 6428dfab652096c665b37ee3a4d32e4e219d2b52
# Parent  5545aff878b17070fab853c13068d4aad632fd68
clarified Thy_Load.node_name;

diff -r 5545aff878b1 -r 6428dfab6520 src/Pure/Thy/thy_load.scala
--- 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 =
diff -r 5545aff878b1 -r 6428dfab6520 src/Pure/Tools/build.scala
--- 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