# HG changeset patch
# User berghofe
# Date 1082133722 -7200
# Node ID 2df717e26035faad88f2543ce5058d550c2cc947
# Parent  3ff9cfc5c403644ae2e9a46c5b4d10bff7ae69b6
Added variants of functions quote and commas_quote that allow escaping
of " in error messages etc. This is useful for PGIP output.

diff -r 3ff9cfc5c403 -r 2df717e26035 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Apr 16 18:40:21 2004 +0200
+++ b/src/Pure/General/symbol.ML	Fri Apr 16 18:42:02 2004 +0200
@@ -48,6 +48,8 @@
   val output: string -> string
   val output_width: string -> string * real
   val indent: string * int -> string
+  val quote: string -> string
+  val commas_quote: string list -> string
 end;
 
 structure Symbol: SYMBOL =
@@ -307,9 +309,21 @@
 fun indent x = #2 (get_mode ()) x;
 
 
+(* these variants allow escaping of quotes depending on mode *)
+
+fun quote s = output "\"" ^ s ^ output "\"";
+val commas_quote = space_implode (output ", ") o map quote;
+
+
 (*final declarations of this structure!*)
 val length = sym_length;
 val explode = sym_explode;
 val escape = sym_escape;
 
 end;
+
+
+(* Overwrites versions in Library *)
+
+val quote = Symbol.quote;
+val commas_quote = Symbol.commas_quote;
\ No newline at end of file