changeset 48873 | 18b17f15bc62 |
parent 48755 | 393a37003851 |
child 49414 | d7b5fb2e9ca2 |
--- a/src/Pure/Thy/thy_syntax.scala Tue Aug 21 14:54:29 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 21 16:56:18 2012 +0200 @@ -150,7 +150,9 @@ val syntax = if (previous.is_init || updated_keywords) - (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) } + (base_syntax /: nodes.entries) { + case (syn, (_, node)) => syn.add_keywords(node.header.keywords) + } else previous.syntax val reparse =