--- a/src/Pure/Thy/thy_syntax.scala Fri Sep 29 22:12:32 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Sep 29 22:41:19 2017 +0200
@@ -100,8 +100,10 @@
if (node.is_empty) None
else {
val header = node.header
- val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
- Some((resources.session_base.overall_syntax /: imports_syntax)(_ ++ _) + header)
+ val imports_syntax =
+ Outer_Syntax.merge(
+ header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
+ Some(imports_syntax + header)
}
nodes += (name -> node.update_syntax(syntax))
}
@@ -323,7 +325,9 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
- val syntax = node.syntax getOrElse resources.session_base.overall_syntax
+ val syntax =
+ resources.session_base.node_syntax(nodes, name) getOrElse
+ Thy_Header.bootstrap_syntax
val commands = node.commands
val node1 =