src/Pure/PIDE/protocol.scala
changeset 65445 e9e7f5f5794c
parent 65439 862bfd2b4fd4
child 65470 a0f49174dbeb
equal deleted inserted replaced
65444:1f5821b19741 65445:e9e7f5f5794c
   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       {