src/Pure/Thy/thy_syntax.scala
changeset 54515 570ba266f5b5
parent 54513 5545aff878b1
child 54517 044bee8c5e69
--- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -33,7 +33,7 @@
 
       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
       var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
-        List((0, node_name.theory, buffer()))
+        List((0, node_name.toString, buffer()))
 
       @tailrec def close(level: Int => Boolean)
       {
@@ -260,7 +260,7 @@
     val files = span_files(syntax, span)
     files.map(file => {
       // FIXME proper thy_load append
-      val file_name = Document.Node.Name(name.dir + file, name.dir, "")
+      val file_name = Document.Node.Name(name.master_dir + file)
       (file_name, all_blobs.get(file_name).map(_.sha1_digest))
     })
   }