--- a/src/Pure/PIDE/protocol.scala Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Feb 29 23:09:06 2012 +0100
@@ -211,22 +211,24 @@
val edits_yxml =
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
- def encode_edit(dir: String)
+ def encode_edit(name: Document.Node.Name)
: T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) },
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
- { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+ { case Document.Node.Header(Exn.Res(deps)) =>
+ val dir = Isabelle_System.posix_path(name.dir)
+ val imports = deps.imports.map(_.node)
+ val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
(Nil,
triple(pair(string, string), list(string), list(pair(string, bool)))(
- (dir, a), b, c)) },
+ (dir, name.theory), imports, uses)) },
{ case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
val (name, edit) = node_edit
- val dir = Isabelle_System.posix_path(name.dir)
- pair(string, encode_edit(dir))(name.node, edit)
+ pair(string, encode_edit(name))(name.node, edit)
})
YXML.string_of_body(encode(edits)) }
input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)