more accurate node_syntax: avoid overall_syntax for PIDE edits;
authorwenzelm
Fri Sep 29 22:41:19 2017 +0200 (21 months ago)
changeset 66721ae38b8c0fdd9
parent 66720 b07192253605
child 66722 9c661b74ce92
more accurate node_syntax: avoid overall_syntax for PIDE edits;
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 22:12:32 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:41:19 2017 +0200
     1.3 @@ -132,6 +132,9 @@
     1.4      def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
     1.5        loaded_theory_syntax(name.theory)
     1.6  
     1.7 +    def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] =
     1.8 +      nodes(name).syntax orElse loaded_theory_syntax(name)
     1.9 +
    1.10      def known_theory(name: String): Option[Document.Node.Name] =
    1.11        known.theories.get(name)
    1.12  
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 22:12:32 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 22:41:19 2017 +0200
     2.3 @@ -100,8 +100,10 @@
     2.4          if (node.is_empty) None
     2.5          else {
     2.6            val header = node.header
     2.7 -          val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
     2.8 -          Some((resources.session_base.overall_syntax /: imports_syntax)(_ ++ _) + header)
     2.9 +          val imports_syntax =
    2.10 +            Outer_Syntax.merge(
    2.11 +              header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
    2.12 +          Some(imports_syntax + header)
    2.13          }
    2.14        nodes += (name -> node.update_syntax(syntax))
    2.15      }
    2.16 @@ -323,7 +325,9 @@
    2.17          node_edits foreach {
    2.18            case (name, edits) =>
    2.19              val node = nodes(name)
    2.20 -            val syntax = node.syntax getOrElse resources.session_base.overall_syntax
    2.21 +            val syntax =
    2.22 +              resources.session_base.node_syntax(nodes, name) getOrElse
    2.23 +              Thy_Header.bootstrap_syntax
    2.24              val commands = node.commands
    2.25  
    2.26              val node1 =