src/Pure/PIDE/protocol.scala
changeset 46737 09ab89658a5d
parent 46688 134982ee4ecb
child 46755 f676b5ade7d7
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Feb 29 17:43:41 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Feb 29 23:09:06 2012 +0100
     1.3 @@ -211,22 +211,24 @@
     1.4      val edits_yxml =
     1.5      { import XML.Encode._
     1.6        def id: T[Command] = (cmd => long(cmd.id))
     1.7 -      def encode_edit(dir: String)
     1.8 +      def encode_edit(name: Document.Node.Name)
     1.9            : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
    1.10          variant(List(
    1.11            { case Document.Node.Clear() => (Nil, Nil) },
    1.12            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    1.13 -          { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    1.14 +          { case Document.Node.Header(Exn.Res(deps)) =>
    1.15 +              val dir = Isabelle_System.posix_path(name.dir)
    1.16 +              val imports = deps.imports.map(_.node)
    1.17 +              val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
    1.18                (Nil,
    1.19                  triple(pair(string, string), list(string), list(pair(string, bool)))(
    1.20 -                  (dir, a), b, c)) },
    1.21 +                  (dir, name.theory), imports, uses)) },
    1.22            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
    1.23            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    1.24        def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.25        {
    1.26          val (name, edit) = node_edit
    1.27 -        val dir = Isabelle_System.posix_path(name.dir)
    1.28 -        pair(string, encode_edit(dir))(name.node, edit)
    1.29 +        pair(string, encode_edit(name))(name.node, edit)
    1.30        })
    1.31        YXML.string_of_body(encode(edits)) }
    1.32      input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)