clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
authorwenzelm
Fri Oct 06 17:13:57 2017 +0200 (18 months ago)
changeset 66770122df1fde073
parent 66769 97f16ada519c
child 66771 925d10a7a610
clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Oct 05 17:39:36 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Oct 06 17:13:57 2017 +0200
     1.3 @@ -131,8 +131,8 @@
     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 +    def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
    1.10 +      nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
    1.11  
    1.12      def known_theory(name: String): Option[Document.Node.Name] =
    1.13        known.theories.get(name)
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Oct 05 17:39:36 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Oct 06 17:13:57 2017 +0200
     2.3 @@ -102,7 +102,7 @@
     2.4            val header = node.header
     2.5            val imports_syntax =
     2.6              Outer_Syntax.merge(
     2.7 -              header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
     2.8 +              header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
     2.9            Some(imports_syntax + header)
    2.10          }
    2.11        nodes += (name -> node.update_syntax(syntax))
    2.12 @@ -325,9 +325,7 @@
    2.13          node_edits foreach {
    2.14            case (name, edits) =>
    2.15              val node = nodes(name)
    2.16 -            val syntax =
    2.17 -              resources.session_base.node_syntax(nodes, name) getOrElse
    2.18 -              Thy_Header.bootstrap_syntax
    2.19 +            val syntax = resources.session_base.node_syntax(nodes, name)
    2.20              val commands = node.commands
    2.21  
    2.22              val node1 =