--- a/src/Pure/Thy/thy_syntax.scala Mon Apr 03 16:50:44 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Apr 03 17:00:36 2017 +0200
@@ -101,7 +101,7 @@
else {
val header = node.header
val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
- Some((resources.base.syntax /: imports_syntax)(_ ++ _)
+ Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
.add_keywords(header.keywords).add_abbrevs(header.abbrevs))
}
nodes += (name -> node.update_syntax(syntax))
@@ -300,7 +300,7 @@
doc_blobs.get(name) orElse previous.nodes(name).get_blob
def can_import(name: Document.Node.Name): Boolean =
- resources.base.loaded_theory(name) || nodes0(name).has_header
+ resources.session_base.loaded_theory(name) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -324,7 +324,7 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
- val syntax = node.syntax getOrElse resources.base.syntax
+ val syntax = node.syntax getOrElse resources.session_base.syntax
val commands = node.commands
val node1 =