# HG changeset patch
# User wenzelm
# Date 1506717679 -7200
# Node ID ae38b8c0fdd9c46bdd1cf366080ceef238f114f6
# Parent  b071922536050340f4a3cf7fc568579f8e96dd2d
more accurate node_syntax: avoid overall_syntax for PIDE edits;

diff -r b07192253605 -r ae38b8c0fdd9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 22:12:32 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:41:19 2017 +0200
@@ -132,6 +132,9 @@
     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 known_theory(name: String): Option[Document.Node.Name] =
       known.theories.get(name)
 
diff -r b07192253605 -r ae38b8c0fdd9 src/Pure/Thy/thy_syntax.scala
--- 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 =