tuned signature -- less cryptic ASCII names;

--- a/src/Pure/General/symbol.ML	Tue Jul 12 15:17:37 2011 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jul 12 15:32:16 2011 +0200
@@ -7,10 +7,7 @@
 signature SYMBOL =
 sig
   type symbol = string
-  val SOH: symbol
   val STX: symbol
-  val ENQ: symbol
-  val ACK: symbol
   val DEL: symbol
   val space: symbol
   val spaces: int -> string
@@ -89,10 +86,7 @@
 
 type symbol = string;
 
-val SOH = chr 1;
 val STX = chr 2;
-val ENQ = chr 5;
-val ACK = chr 6;
 val DEL = chr 127;
 
 val space = chr 32;

--- a/src/Pure/General/yxml.ML	Tue Jul 12 15:17:37 2011 +0200
+++ b/src/Pure/General/yxml.ML	Tue Jul 12 15:32:16 2011 +0200
@@ -15,6 +15,8 @@
 
 signature YXML =
 sig
+  val X: Symbol.symbol
+  val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
   val output_markup: Markup.T -> string * string
@@ -45,8 +47,8 @@
 
 (* markers *)
 
-val X = Symbol.ENQ;
-val Y = Symbol.ACK;
+val X = chr 5;
+val Y = chr 6;
 val XY = X ^ Y;
 val XYX = XY ^ X;
 

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 12 15:17:37 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 12 15:32:16 2011 +0200
@@ -22,7 +22,7 @@
 val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
 val test_markupN = "test_markup";          (*XML markup for everything*)
 
-fun special ch = Symbol.SOH ^ ch;
+fun special ch = chr 1 ^ ch;
 
 
 (* render markup *)