# HG changeset patch # User wenzelm # Date 1606663287 -3600 # Node ID 1cc74982d03882e58f42938d838c3b4883e8b349 # Parent 83e581c9a5f1f8be3c2a468bc65052c6633c36b7 clarified parser; diff -r 83e581c9a5f1 -r 1cc74982d038 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sun Nov 29 16:11:52 2020 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Nov 29 16:21:27 2020 +0100 @@ -162,7 +162,7 @@ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(ABBREVS) ~! abbrevs) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ - $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d).map(Symbol.decode) } + $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d) } val heading = (command(CHAPTER) | @@ -225,7 +225,7 @@ if (command) Token.Pos.command else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _) - Parser.parse_header(tokens, pos).check(node_name) + Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name) } }