src/Pure/General/symbol.ML

--- a/src/Pure/General/symbol.ML	Sat Jul 07 00:14:58 2007 +0200
+++ b/src/Pure/General/symbol.ML	Sat Jul 07 00:14:59 2007 +0200
@@ -9,7 +9,7 @@
 sig
   type symbol
   val space: symbol
-  val spaces: int -> symbol
+  val spaces: int -> string
   val is_char: symbol -> bool
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
@@ -58,12 +58,7 @@
   val bump_init: string -> string
   val bump_string: string -> string
   val length: symbol list -> int
-  val default_output: string -> string * real
-  val default_keyword: bool -> string -> string * real
-  val default_indent: string * int -> string
-  val default_raw: string -> string
   val xsymbolsN: string
-  val symbol_output: string -> string * real
 end;
 
 structure Symbol: SYMBOL =
@@ -190,7 +185,7 @@
 
 (*raw encoding avoids looping errors!*)
 fun malformed_symbol s =
-  "Malformed symbolic character specification: " ^ quote (Output.raw s);
+  "Malformed symbolic character specification: " ^ quote (Output.escape s);
 
 
 (* decode_raw *)
@@ -493,19 +488,7 @@
 
 
 
-(** print modes **)
-
-(* default *)
-
-fun default_output s = (s, real (size s));
-fun default_keyword (_: bool) = default_output;
-fun default_indent (_: string, k) = spaces k;
-fun default_raw (s: string) = s;
-
-val _ = Output.add_mode "" (default_output, default_keyword, default_indent, default_raw);
-
-
-(* xsymbols *)
+(** xsymbols **)
 
 val xsymbolsN = "xsymbols";
 
@@ -518,15 +501,6 @@
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
-fun symbol_output str =
-  if chars_only str then default_output str
-  else
-    let
-      fun out s = if is_raw s then decode_raw s else s;
-      val syms = sym_explode str;
-    in (implode (map out syms), real (sym_length syms)) end;
-
-
 (*final declarations of this structure!*)
 val length = sym_length;
 val explode = sym_explode;