# HG changeset patch # User wenzelm # Date 1506697413 -7200 # Node ID afba7ffd64926d19aa28d3f6ccd99e4bdb99af11 # Parent 4c98c929a12a0aae8787e7fa2872192ca4a58e33 tuned; diff -r 4c98c929a12a -r afba7ffd6492 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Thu Sep 28 15:11:32 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Fri Sep 29 17:03:33 2017 +0200 @@ -127,7 +127,7 @@ { if (node_name.is_theory && reader.source.length > 0) { try { - val header = Thy_Header.read(reader, start, strict).decode_symbols + val header = Thy_Header.read(reader, start, strict) val base_name = node_name.theory_base_name val (name, pos) = header.name diff -r 4c98c929a12a -r afba7ffd6492 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Thu Sep 28 15:11:32 2017 +0200 +++ b/src/Pure/Thy/thy_header.scala Fri Sep 29 17:03:33 2017 +0200 @@ -138,7 +138,14 @@ (opt($$$(ABBREVS) ~! abbrevs) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ $$$(BEGIN) ^^ - { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) } + { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ => + val f = Symbol.decode _ + Thy_Header((f(name), pos), + imports.map({ case (a, b) => (f(a), b) }), + keywords.map({ case (a, Keyword.Spec(b, c, d)) => + (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }), + abbrevs.map({ case (a, b) => (f(a), f(b)) })) + } val heading = (command(CHAPTER) | @@ -197,20 +204,8 @@ } } - sealed case class Thy_Header( name: (String, Position.T), imports: List[(String, Position.T)], keywords: Thy_Header.Keywords, abbrevs: Thy_Header.Abbrevs) -{ - def decode_symbols: Thy_Header = - { - val f = Symbol.decode _ - Thy_Header((f(name._1), name._2), - imports.map({ case (a, b) => (f(a), b) }), - keywords.map({ case (a, Keyword.Spec(b, c, d)) => - (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }), - abbrevs.map({ case (a, b) => (f(a), f(b)) })) - } -}