# HG changeset patch # User wenzelm # Date 1183760099 -7200 # Node ID 32ee8cac5c0283ec5b5695d7e8a5dc6d5632df82 # Parent 840904fc1eb1d6dd56a9b09407f93e2c0022a7a1 simplified output mode setup; removed unused symbol_output; tuned; diff -r 840904fc1eb1 -r 32ee8cac5c02 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;