# HG changeset patch
# User wenzelm
# Date 1330711513 -3600
# Node ID 3c4e327070e567d72dffceae47a21b2f2b7e0f50
# Parent  a6ea1c68fa529b6d4c9fff2d50ead3edf4bd57b2# Parent  f676b5ade7d7896f53c4c131bf435167acaab8b7
merged

diff -r a6ea1c68fa52 -r 3c4e327070e5 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Mar 02 09:35:39 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Mar 02 19:05:13 2012 +0100
@@ -211,19 +211,20 @@
     val edits_yxml =
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
+      def encode_string: T[String] = (s => string(Symbol.encode(s)))
       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(deps)) =>
-              val dir = Isabelle_System.posix_path(name.dir)
+              val dir = Symbol.encode(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))
+              val uses = deps.uses.map(p => (Symbol.encode(Isabelle_System.posix_path(p._1)), p._2))
               (Nil,
-                triple(pair(string, string), list(string), list(pair(string, bool)))(
+                triple(pair(string, encode_string), list(encode_string), list(pair(string, bool)))(
                   (dir, name.theory), imports, uses)) },
-          { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
+          { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(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) =>
       {