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 = Long_Name.base_name(name.theory) |
362 val theory = name.theory_base_name // FIXME |
363 val imports = header.imports.map({ case (a, _) => a.node }) |
363 val imports = header.imports.map({ case (a, _) => a.node }) |
364 val keywords = |
364 val keywords = |
365 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) |
365 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) |
366 (Nil, |
366 (Nil, |
367 pair(string, pair(string, pair(list(string), pair(list(pair(string, |
367 pair(string, pair(string, pair(list(string), pair(list(pair(string, |