# HG changeset patch
# User berghofe
# Date 1038414049 -3600
# Node ID 09aeb7346d3f7a5acbf76e980fc316ec5af0759f
# Parent  1a8dda49fd866f8f4698b2ccd13d1042f5666db4
default_output now escapes \'s more carefully.

diff -r 1a8dda49fd86 -r 09aeb7346d3f src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Nov 27 17:17:53 2002 +0100
+++ b/src/Pure/General/symbol.ML	Wed Nov 27 17:20:49 2002 +0100
@@ -32,6 +32,7 @@
   val length: symbol list -> int
   val strip_blanks: string -> string
   val beginning: symbol list -> string
+  val scan_id: string list -> string * string list
   val scan: string list -> symbol * string list
   val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
   val source: bool -> (string, 'a) Source.source ->
@@ -208,9 +209,14 @@
 
 fun string_size s = (s, real (size s));
 
+val escape = Scan.repeat
+  ((($$ "\\" >> K "\\\\") ^^ Scan.optional ($$ "\\" >> K "\\\\") "" ^^ $$ "<" ^^
+      Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
+   Scan.one not_eof) >> implode;
+
 fun default_output s =
   if not (exists_string (equal "\\") s) then string_size s
-  else string_size (implode (map (fn "\\" => "\\\\" | c => c) (explode s)));    (*sic!*)
+  else string_size (fst (Scan.finite stopper escape (explode s)));
 
 fun default_indent (_: string, k) = spaces k;