# HG changeset patch
# User wenzelm
# Date 1507302837 -7200
# Node ID 122df1fde073861ce27a5aa9df2d907f214b1793
# Parent  97f16ada519c26205f989b3158b695c736191749
clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;

diff -r 97f16ada519c -r 122df1fde073 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Oct 05 17:39:36 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Oct 06 17:13:57 2017 +0200
@@ -131,8 +131,8 @@
     def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
       loaded_theory_syntax(name.theory)
 
-    def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] =
-      nodes(name).syntax orElse loaded_theory_syntax(name)
+    def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
+      nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
 
     def known_theory(name: String): Option[Document.Node.Name] =
       known.theories.get(name)
diff -r 97f16ada519c -r 122df1fde073 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Oct 05 17:39:36 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Oct 06 17:13:57 2017 +0200
@@ -102,7 +102,7 @@
           val header = node.header
           val imports_syntax =
             Outer_Syntax.merge(
-              header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
+              header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
           Some(imports_syntax + header)
         }
       nodes += (name -> node.update_syntax(syntax))
@@ -325,9 +325,7 @@
         node_edits foreach {
           case (name, edits) =>
             val node = nodes(name)
-            val syntax =
-              resources.session_base.node_syntax(nodes, name) getOrElse
-              Thy_Header.bootstrap_syntax
+            val syntax = resources.session_base.node_syntax(nodes, name)
             val commands = node.commands
 
             val node1 =