# HG changeset patch
# User wenzelm
# Date 1344335724 -7200
# Node ID dd32321d6eefce1a98ccbbdc1a5bb1beff99c45f
# Parent  85a3de10567de1d6d24b484665afe4859e257f04
tuned signature -- slightly more abstract text representation of prover process;

diff -r 85a3de10567d -r dd32321d6eef src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 07 12:10:26 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 07 12:35:24 2012 +0200
@@ -195,7 +195,7 @@
 
   def define_command(command: Command): Unit =
     input("Document.define_command",
-      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
+      Document.ID(command.id), encode(command.name), encode(command.source))
 
 
   /* document versions */
@@ -210,7 +210,6 @@
     val edits_yxml =
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
-      def symbol_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(
@@ -222,18 +221,18 @@
               // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
               val uses = deps.uses
               (Nil,
-                pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
-                  list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
-                    list(pair(symbol_string, bool)))(
+                pair(pair(pair(pair(Encode.string, Encode.string), list(Encode.string)),
+                  list(pair(Encode.string, option(pair(Encode.string, list(Encode.string)))))),
+                    list(pair(Encode.string, bool)))(
                 (((dir, name.theory), imports), deps.keywords), uses)) },
-          { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
+          { case Document.Node.Header(Exn.Exn(e)) => (List(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) =>
+      def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
         pair(string, encode_edit(name))(name.node, edit)
       })
-      YXML.string_of_body(encode(edits)) }
+      YXML.string_of_body(encode_edits(edits)) }
     input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   }
 
diff -r 85a3de10567d -r dd32321d6eef src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Aug 07 12:10:26 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Aug 07 12:35:24 2012 +0200
@@ -83,6 +83,17 @@
   import Isabelle_Process._
 
 
+  /* text representation */
+
+  def encode(s: String): String = Symbol.encode(s)
+  def decode(s: String): String = Symbol.decode(s)
+
+  object Encode
+  {
+    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+  }
+
+
   /* output */
 
   private def system_output(text: String)
@@ -264,7 +275,7 @@
             else done = true
           }
           if (result.length > 0) {
-            output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
+            output_message(markup, Nil, List(XML.Text(decode(result.toString))))
             result.length = 0
           }
           else {
@@ -323,7 +334,7 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(decode: Boolean): XML.Body =
+      def read_chunk(do_decode: Boolean): XML.Body =
       {
         //{{{
         // chunk size
@@ -350,8 +361,8 @@
 
         if (i != n) throw new Protocol_Error("bad message chunk content")
 
-        if (decode)
-          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
+        if (do_decode)
+          YXML.parse_body_failsafe(Standard_System.decode_chars(decode, buf, 0, n))
         else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
         //}}}
       }