# HG changeset patch
# User oheimb
# Date 917626334 -3600
# Node ID a56aaad7ff2d9d96325921f26edc9f45aa5052e4
# Parent  a7d74bf9da52e3a427e02878a7214fecd18c3256
renamed space2 to spacespace
prepared switch for escaped output of symbols (used for
ProofGeneral in connection with the x-symbol package)

diff -r a7d74bf9da52 -r a56aaad7ff2d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Jan 29 17:11:40 1999 +0100
+++ b/src/Pure/General/symbol.ML	Fri Jan 29 17:12:14 1999 +0100
@@ -43,7 +43,7 @@
 val enc_vector =
 [
 (* GENERATED TEXT FOLLOWS - Do not edit! *)
-  "\\<space2>",
+  "\\<spacespace>",
   "\\<Gamma>",
   "\\<Delta>",
   "\\<Theta>",
@@ -194,7 +194,7 @@
 
 val is_blank =
   fn " " => true | "\t" => true | "\n" => true | "\^L" => true
-    | "\160" => true | "\\<space2>" => true
+    | "\160" => true | "\\<spacespace>" => true
     | _ => false;
 
 val is_letdig = is_quasi_letter orf is_digit;
@@ -262,7 +262,11 @@
     else implode (map symbol' chs)
   end;
 
-val output = implode o map char o sym_explode;
+fun char' s = if size s > 1 then "\\" ^ s else s;
+fun output s = let val chr = (* if "isabelle_font" mem_string !print_mode *)
+(* FIXME: does not work yet, because of static calls to output in printer.ML *)
+			     (* then *) char (* else char'*)
+		in (implode o map chr o sym_explode) s end;
 
 
 (*final declarations of this structure!*)