src/Doc/antiquote_setup.ML
changeset 52408 fa2dc6c6c94f
parent 50239 fb579401dc26
child 53044 be27b6be8027
     1.1 --- a/src/Doc/antiquote_setup.ML	Sat Jun 15 16:55:49 2013 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sat Jun 15 21:01:07 2013 +0200
     1.3 @@ -19,6 +19,8 @@
     1.4  val clean_string = translate
     1.5    (fn "_" => "\\_"
     1.6      | "#" => "\\#"
     1.7 +    | "$" => "\\$"
     1.8 +    | "%" => "\\%"
     1.9      | "<" => "$<$"
    1.10      | ">" => "$>$"
    1.11      | "{" => "\\{"