--- a/src/Pure/Thy/thy_info.scala Wed Apr 30 13:11:24 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala Wed Apr 30 22:34:11 2014 +0200
@@ -95,11 +95,11 @@
}
}
- private def require_thys(initiators: List[Document.Node.Name],
+ private def require_thys(session: String, initiators: List[Document.Node.Name],
required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- (required /: thys)(require_thy(initiators, _, _))
+ (required /: thys)(require_thy(session, initiators, _, _))
- private def require_thy(initiators: List[Document.Node.Name],
+ private def require_thy(session: String, initiators: List[Document.Node.Name],
required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
{
val (name, require_pos) = thy
@@ -116,10 +116,10 @@
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
val header =
- try { resources.check_thy(name).cat_errors(message) }
+ try { resources.check_thy(session, name).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
val imports = header.imports.map((_, Position.File(name.node)))
- Dep(name, header) :: require_thys(name :: initiators, required1, imports)
+ Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
}
catch {
case e: Throwable =>
@@ -128,6 +128,6 @@
}
}
- def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- require_thys(Nil, Dependencies.empty, thys)
+ def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+ require_thys(session, Nil, Dependencies.empty, thys)
}