even more robust syntax (amending 122df1fde073);
authorwenzelm
Fri Oct 06 21:23:21 2017 +0200 (20 months ago)
changeset 66772a66f11a0b5b1
parent 66771 925d10a7a610
child 66773 0cd29455a5e8
even more robust syntax (amending 122df1fde073);
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Oct 06 21:14:00 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Oct 06 21:23:21 2017 +0200
     1.3 @@ -101,8 +101,11 @@
     1.4          else {
     1.5            val header = node.header
     1.6            val imports_syntax =
     1.7 -            Outer_Syntax.merge(
     1.8 -              header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
     1.9 +            if (header.imports.nonEmpty) {
    1.10 +              Outer_Syntax.merge(
    1.11 +                header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
    1.12 +            }
    1.13 +            else resources.session_base.overall_syntax
    1.14            Some(imports_syntax + header)
    1.15          }
    1.16        nodes += (name -> node.update_syntax(syntax))