src/Pure/PIDE/isar_document.scala
changeset 44159 9a35e88d9dc9
parent 44158 fe6d1ae7a065
child 44182 ecb51b457064
equal deleted inserted replaced
44158:fe6d1ae7a065 44159:9a35e88d9dc9
   148         list(pair(string,
   148         list(pair(string,
   149           variant(List(
   149           variant(List(
   150             { case Document.Node.Remove() => (Nil, Nil) },
   150             { case Document.Node.Remove() => (Nil, Nil) },
   151             { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
   151             { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
   152             { case Document.Node.Update_Header(
   152             { case Document.Node.Update_Header(
   153                   Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
   153                   Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
   154                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
   154                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
   155             { case Document.Node.Update_Header(
   155             { case Document.Node.Update_Header(
   156                   Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
   156                   Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
   157       YXML.string_of_body(encode(edits)) }
   157       YXML.string_of_body(encode(edits)) }
   158 
   158