209 edits: List[Document.Edit_Command]) |
209 edits: List[Document.Edit_Command]) |
210 { |
210 { |
211 val edits_yxml = |
211 val edits_yxml = |
212 { import XML.Encode._ |
212 { import XML.Encode._ |
213 def id: T[Command] = (cmd => long(cmd.id)) |
213 def id: T[Command] = (cmd => long(cmd.id)) |
|
214 def encode_string: T[String] = (s => string(Symbol.encode(s))) |
214 def encode_edit(name: Document.Node.Name) |
215 def encode_edit(name: Document.Node.Name) |
215 : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = |
216 : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = |
216 variant(List( |
217 variant(List( |
217 { case Document.Node.Clear() => (Nil, Nil) }, |
218 { case Document.Node.Clear() => (Nil, Nil) }, |
218 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
219 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
219 { case Document.Node.Header(Exn.Res(deps)) => |
220 { case Document.Node.Header(Exn.Res(deps)) => |
220 val dir = Isabelle_System.posix_path(name.dir) |
221 val dir = Symbol.encode(Isabelle_System.posix_path(name.dir)) |
221 val imports = deps.imports.map(_.node) |
222 val imports = deps.imports.map(_.node) |
222 val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) |
223 val uses = deps.uses.map(p => (Symbol.encode(Isabelle_System.posix_path(p._1)), p._2)) |
223 (Nil, |
224 (Nil, |
224 triple(pair(string, string), list(string), list(pair(string, bool)))( |
225 triple(pair(string, encode_string), list(encode_string), list(pair(string, bool)))( |
225 (dir, name.theory), imports, uses)) }, |
226 (dir, name.theory), imports, uses)) }, |
226 { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, |
227 { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) }, |
227 { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) |
228 { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) |
228 def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
229 def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
229 { |
230 { |
230 val (name, edit) = node_edit |
231 val (name, edit) = node_edit |
231 pair(string, encode_edit(name))(name.node, edit) |
232 pair(string, encode_edit(name))(name.node, edit) |