# 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