1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 07 12:10:26 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 07 12:35:24 2012 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4  
     1.5    def define_command(command: Command): Unit =
     1.6      input("Document.define_command",
     1.7 -      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
     1.8 +      Document.ID(command.id), encode(command.name), encode(command.source))
     1.9  
    1.10  
    1.11    /* document versions */
    1.12 @@ -210,7 +210,6 @@
    1.13      val edits_yxml =
    1.14      { import XML.Encode._
    1.15        def id: T[Command] = (cmd => long(cmd.id))
    1.16 -      def symbol_string: T[String] = (s => string(Symbol.encode(s)))
    1.17        def encode_edit(name: Document.Node.Name)
    1.18            : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
    1.19          variant(List(
    1.20 @@ -222,18 +221,18 @@
    1.21                // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
    1.22                val uses = deps.uses
    1.23                (Nil,
    1.24 -                pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
    1.25 -                  list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
    1.26 -                    list(pair(symbol_string, bool)))(
    1.27 +                pair(pair(pair(pair(Encode.string, Encode.string), list(Encode.string)),
    1.28 +                  list(pair(Encode.string, option(pair(Encode.string, list(Encode.string)))))),
    1.29 +                    list(pair(Encode.string, bool)))(
    1.30                  (((dir, name.theory), imports), deps.keywords), uses)) },
    1.31 -          { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
    1.32 +          { case Document.Node.Header(Exn.Exn(e)) => (List(encode(Exn.message(e))), Nil) },
    1.33            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    1.34 -      def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.35 +      def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.36        {
    1.37          val (name, edit) = node_edit
    1.38          pair(string, encode_edit(name))(name.node, edit)
    1.39        })
    1.40 -      YXML.string_of_body(encode(edits)) }
    1.41 +      YXML.string_of_body(encode_edits(edits)) }
    1.42      input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
    1.43    }
    1.44  

     2.1 --- a/src/Pure/System/isabelle_process.scala	Tue Aug 07 12:10:26 2012 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Aug 07 12:35:24 2012 +0200
     2.3 @@ -83,6 +83,17 @@
     2.4    import Isabelle_Process._
     2.5  
     2.6  
     2.7 +  /* text representation */
     2.8 +
     2.9 +  def encode(s: String): String = Symbol.encode(s)
    2.10 +  def decode(s: String): String = Symbol.decode(s)
    2.11 +
    2.12 +  object Encode
    2.13 +  {
    2.14 +    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
    2.15 +  }
    2.16 +
    2.17 +
    2.18    /* output */
    2.19  
    2.20    private def system_output(text: String)
    2.21 @@ -264,7 +275,7 @@
    2.22              else done = true
    2.23            }
    2.24            if (result.length > 0) {
    2.25 -            output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
    2.26 +            output_message(markup, Nil, List(XML.Text(decode(result.toString))))
    2.27              result.length = 0
    2.28            }
    2.29            else {
    2.30 @@ -323,7 +334,7 @@
    2.31        val default_buffer = new Array[Byte](65536)
    2.32        var c = -1
    2.33  
    2.34 -      def read_chunk(decode: Boolean): XML.Body =
    2.35 +      def read_chunk(do_decode: Boolean): XML.Body =
    2.36        {
    2.37          //{{{
    2.38          // chunk size
    2.39 @@ -350,8 +361,8 @@
    2.40  
    2.41          if (i != n) throw new Protocol_Error("bad message chunk content")
    2.42  
    2.43 -        if (decode)
    2.44 -          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
    2.45 +        if (do_decode)
    2.46 +          YXML.parse_body_failsafe(Standard_System.decode_chars(decode, buf, 0, n))
    2.47          else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
    2.48          //}}}
    2.49        }