--- a/src/Pure/Thy/thy_syntax.scala Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Sat Mar 29 09:34:51 2014 +0100
@@ -245,7 +245,7 @@
}
def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
- syntax.thy_load(span) match {
+ syntax.load(span) match {
case Some(exts) =>
find_file(span) match {
case Some(file) =>
@@ -448,7 +448,7 @@
val reparse =
(reparse0 /: nodes0.entries)({
case (reparse, (name, node)) =>
- if (node.thy_load_commands.exists(_.blobs_changed(doc_blobs)))
+ if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
name :: reparse
else reparse
})