# HG changeset patch
# User wenzelm
# Date 952984869 -3600
# Node ID 86e99f86393201d5bf1a770fd96c7c88fb75803d
# Parent  8f8eb220d9aafebedc236ae3b69b122d0195beb8
proper symbol_output for "xsymbols" mode;

diff -r 8f8eb220d9aa -r 86e99f863932 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Mon Mar 13 16:24:52 2000 +0100
+++ b/src/Pure/Interface/proof_general.ML	Mon Mar 13 23:01:09 2000 +0100
@@ -71,6 +71,17 @@
 
 (** run-time operations **)
 
+(* symbol output *)
+
+fun xsymbols_output s =
+  if not (exists_string (equal "\\") s) then (s, real (size s))
+  else
+    let val syms = Symbol.explode s
+    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end;
+
+fun setup_xsymbols_output () = Symbol.add_mode "xsymbols" xsymbols_output;
+
+
 (* messages *)
 
 val plain_output = std_output o suffix "\n";
@@ -229,7 +240,8 @@
 (* init *)
 
 fun init isar =
- (setup_messages ();
+ (setup_xsymbols_output ();
+  setup_messages ();
   setup_state ();
   setup_thy_loader ();
   print_mode := [proof_generalN];