src/Pure/library.ML

   val forall_string: (string -> bool) -> string -> bool
   val first_field: string -> string -> (string * string) option
   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
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list

 fun unenclose str = String.substring (str, 1, size str - 2);
 
 (*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 ", ";
 val commas_quote = commas o map quote;