--- a/src/Pure/library.ML Fri Jan 17 20:51:36 2014 +0100
+++ b/src/Pure/library.ML Sat Jan 18 19:15:12 2014 +0100
@@ -139,6 +139,7 @@
val enclose: string -> string -> string -> string
val unenclose: string -> string
val quote: string -> string
+ val cartouche: string -> string
val space_implode: string -> string list -> string
val commas: string list -> string
val commas_quote: string list -> string
@@ -729,6 +730,8 @@
(*simple quoting (does not escape special chars)*)
val quote = enclose "\"" "\"";
+val cartouche = enclose "\\<open>" "\\<close>";
+
fun space_implode a bs = implode (separate a bs);
val commas = space_implode ", ";