src/Pure/Thy/thy_syntax.scala
changeset 63579 73939a9b70a3
parent 60215 5fb4990dfc73
child 63584 68751fe1c036
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 11:49:30 2016 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 17:35:18 2016 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4            val node1 = node.update_header(header)
     1.5            if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
     1.6                node.header.keywords != node1.header.keywords ||
     1.7 +              node.header.abbrevs != node1.header.abbrevs ||
     1.8                node.header.errors != node1.header.errors) syntax_changed0 += name
     1.9            nodes += (name -> node1)
    1.10            doc_edits += (name -> Document.Node.Deps(header))
    1.11 @@ -100,7 +101,8 @@
    1.12          else {
    1.13            val header = node.header
    1.14            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
    1.15 -          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
    1.16 +          Some((resources.base_syntax /: imports_syntax)(_ ++ _)
    1.17 +            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
    1.18          }
    1.19        nodes += (name -> node.update_syntax(syntax))
    1.20      }