tuned;
authorwenzelm
Fri Sep 29 17:03:33 2017 +0200 (20 months ago)
changeset 66713afba7ffd6492
parent 66712 4c98c929a12a
child 66714 9fc4e144693c
tuned;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Sep 28 15:11:32 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 17:03:33 2017 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    {
     1.5      if (node_name.is_theory && reader.source.length > 0) {
     1.6        try {
     1.7 -        val header = Thy_Header.read(reader, start, strict).decode_symbols
     1.8 +        val header = Thy_Header.read(reader, start, strict)
     1.9  
    1.10          val base_name = node_name.theory_base_name
    1.11          val (name, pos) = header.name
     2.1 --- a/src/Pure/Thy/thy_header.scala	Thu Sep 28 15:11:32 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Sep 29 17:03:33 2017 +0200
     2.3 @@ -138,7 +138,14 @@
     2.4        (opt($$$(ABBREVS) ~! abbrevs) ^^
     2.5          { case None => Nil case Some(_ ~ xs) => xs }) ~
     2.6        $$$(BEGIN) ^^
     2.7 -      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
     2.8 +      { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
     2.9 +          val f = Symbol.decode _
    2.10 +          Thy_Header((f(name), pos),
    2.11 +            imports.map({ case (a, b) => (f(a), b) }),
    2.12 +            keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
    2.13 +              (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
    2.14 +            abbrevs.map({ case (a, b) => (f(a), f(b)) }))
    2.15 +      }
    2.16  
    2.17      val heading =
    2.18        (command(CHAPTER) |
    2.19 @@ -197,20 +204,8 @@
    2.20    }
    2.21  }
    2.22  
    2.23 -
    2.24  sealed case class Thy_Header(
    2.25    name: (String, Position.T),
    2.26    imports: List[(String, Position.T)],
    2.27    keywords: Thy_Header.Keywords,
    2.28    abbrevs: Thy_Header.Abbrevs)
    2.29 -{
    2.30 -  def decode_symbols: Thy_Header =
    2.31 -  {
    2.32 -    val f = Symbol.decode _
    2.33 -    Thy_Header((f(name._1), name._2),
    2.34 -      imports.map({ case (a, b) => (f(a), b) }),
    2.35 -      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
    2.36 -        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
    2.37 -      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
    2.38 -  }
    2.39 -}