src/Pure/Thy/thy_syntax.scala
changeset 44182 ecb51b457064
parent 44180 a6dc270d3edb
child 44185 05641edb5d30
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 13:48:26 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 15:59:26 2011 +0200
     1.3 @@ -199,16 +199,15 @@
     1.4            doc_edits += (name -> Document.Node.Edits(cmd_edits))
     1.5            nodes += (name -> node.copy(commands = commands2))
     1.6  
     1.7 -        case (name, Document.Node.Update_Header(header)) =>
     1.8 +        case (name, Document.Node.Header(header)) =>
     1.9            val node = nodes(name)
    1.10            val update_header =
    1.11 -            (node.header.thy_header, header) match {
    1.12 -              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
    1.13 -                thy_header0 != thy_header
    1.14 +            (node.header, header) match {
    1.15 +              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
    1.16                case _ => true
    1.17              }
    1.18            if (update_header) {
    1.19 -            doc_edits += (name -> Document.Node.Update_Header(header))
    1.20 +            doc_edits += (name -> Document.Node.Header(header))
    1.21              nodes += (name -> node.copy(header = header))
    1.22            }
    1.23        }