# HG changeset patch
# User wenzelm
# Date 1087890711 -7200
# Node ID 7d8501843146ae8f73804d6d3e8b3bc45f719183
# Parent  802f3732a54e457487ffc38bcc4b982db39c3def
added chars_only, symbol_output;

diff -r 802f3732a54e -r 7d8501843146 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Jun 22 09:51:39 2004 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jun 22 09:51:51 2004 +0200
@@ -46,6 +46,7 @@
   val source: bool -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
+  val chars_only: string -> bool
   val escape: string -> string
   val strip_blanks: string -> string
   val bump_init: string -> string
@@ -56,6 +57,7 @@
   val default_raw: string -> string
   val symbolsN: string
   val xsymbolsN: string
+  val symbol_output: string -> string * real
 end;
 
 structure Symbol: SYMBOL =
@@ -418,6 +420,8 @@
     else the (Scan.read stopper (Scan.repeat scan) chs)
   end;
 
+val chars_only = not o exists_string (equal "\\");
+
 
 (* escape *)
 
@@ -484,6 +488,14 @@
 
 fun sym_length ss = foldl (fn (n, s) => sym_len s + n) (0, ss);
 
+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;