src/Pure/PIDE/isar_document.scala
changeset 44182 ecb51b457064
parent 44159 9a35e88d9dc9
child 44185 05641edb5d30
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Aug 13 13:48:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Sat Aug 13 15:59:26 2011 +0200
     1.3 @@ -149,11 +149,9 @@
     1.4            variant(List(
     1.5              { case Document.Node.Remove() => (Nil, Nil) },
     1.6              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
     1.7 -            { case Document.Node.Update_Header(
     1.8 -                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
     1.9 +            { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    1.10                  (Nil, triple(string, list(string), list(string))(a, b, c)) },
    1.11 -            { case Document.Node.Update_Header(
    1.12 -                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
    1.13 +            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
    1.14        YXML.string_of_body(encode(edits)) }
    1.15  
    1.16      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)