src/Pure/Thy/thy_syntax.scala
changeset 46749 042c546d2bac
parent 46737 09ab89658a5d
child 46811 03a2dc9e0624
equal deleted inserted replaced
46748:8f3ae4d04a2d 46749:042c546d2bac
   256 
   256 
   257         case (name, Document.Node.Header(header)) =>
   257         case (name, Document.Node.Header(header)) =>
   258           val node = nodes(name)
   258           val node = nodes(name)
   259           val update_header =
   259           val update_header =
   260             (node.header, header) match {
   260             (node.header, header) match {
   261               case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
   261               case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
   262               case _ => true
   262               case _ => true
   263             }
   263             }
   264           if (update_header) {
   264           if (update_header) {
   265             doc_edits += (name -> Document.Node.Header(header))
   265             doc_edits += (name -> Document.Node.Header(header))
   266             nodes += (name -> node.update_header(header))
   266             nodes += (name -> node.update_header(header))