# HG changeset patch
# User wenzelm
# Date 1209738989 -7200
# Node ID 844068d16ba008d66edb1070339c7d15cbe0a8f6
# Parent  cc127cc0951bf69f37adc3a32968c4da9f221c29
clean_string: handle { };

diff -r cc127cc0951b -r 844068d16ba0 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Fri May 02 16:36:05 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Fri May 02 16:36:29 2008 +0200
@@ -13,8 +13,13 @@
 
 (* misc utils *)
 
-val clean_string =
-  translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c);
+val clean_string = translate_string
+  (fn "_" => "-"
+    | ">" => "$>$"
+    | "#" => "\\#"
+    | "{" => "\\{"
+    | "}" => "\\}"
+    | c => c);
 
 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;