src/Pure/PIDE/protocol.scala
changeset 46755 f676b5ade7d7
parent 46737 09ab89658a5d
child 46770 44c28a33c461
     1.1 --- a/src/Pure/PIDE/protocol.scala	Thu Mar 01 21:35:49 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 01 22:26:29 2012 +0100
     1.3 @@ -211,19 +211,20 @@
     1.4      val edits_yxml =
     1.5      { import XML.Encode._
     1.6        def id: T[Command] = (cmd => long(cmd.id))
     1.7 +      def encode_string: T[String] = (s => string(Symbol.encode(s)))
     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(deps)) =>
    1.14 -              val dir = Isabelle_System.posix_path(name.dir)
    1.15 +              val dir = Symbol.encode(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 +              val uses = deps.uses.map(p => (Symbol.encode(Isabelle_System.posix_path(p._1)), p._2))
    1.19                (Nil,
    1.20 -                triple(pair(string, string), list(string), list(pair(string, bool)))(
    1.21 +                triple(pair(string, encode_string), list(encode_string), list(pair(string, bool)))(
    1.22                    (dir, name.theory), imports, uses)) },
    1.23 -          { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
    1.24 +          { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
    1.25            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    1.26        def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.27        {