357 : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = |
357 : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = |
358 variant(List( |
358 variant(List( |
359 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
359 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
360 { case Document.Node.Deps(header) => |
360 { case Document.Node.Deps(header) => |
361 val master_dir = File.standard_url(name.master_dir) |
361 val master_dir = File.standard_url(name.master_dir) |
362 val theory = name.theory_base_name // FIXME |
|
363 val imports = header.imports.map({ case (a, _) => a.node }) |
362 val imports = header.imports.map({ case (a, _) => a.node }) |
364 val keywords = |
363 val keywords = |
365 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) |
364 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) |
366 (Nil, |
365 (Nil, |
367 pair(string, pair(string, pair(list(string), pair(list(pair(string, |
366 pair(string, pair(string, pair(list(string), pair(list(pair(string, |
368 pair(pair(string, list(string)), list(string)))), list(string)))))( |
367 pair(pair(string, list(string)), list(string)))), list(string)))))( |
369 (master_dir, (theory, (imports, (keywords, header.errors)))))) }, |
368 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, |
370 { case Document.Node.Perspective(a, b, c) => |
369 { case Document.Node.Perspective(a, b, c) => |
371 (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), |
370 (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), |
372 list(pair(id, pair(string, list(string))))(c.dest)) })) |
371 list(pair(id, pair(string, list(string))))(c.dest)) })) |
373 def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
372 def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
374 { |
373 { |