# HG changeset patch
# User wenzelm
# Date 1583352542 -3600
# Node ID 8a96a11e0cf5ef5efd6d7db1b99d896b2850ff56
# Parent  bae868febc5361f4d8447b44b746c7bde935c9a2
escape some special chars, notably for URL#NAME form;

diff -r bae868febc53 -r 8a96a11e0cf5 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Tue Mar 03 19:26:24 2020 +0000
+++ b/src/Pure/Thy/document_antiquotations.ML	Wed Mar 04 21:09:02 2020 +0100
@@ -304,11 +304,14 @@
 
 (* URLs *)
 
+val escape_url =
+  translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c);
+
 val _ = Theory.setup
   (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
     (fn ctxt => fn (url, pos) =>
-      let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
-      in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
+      let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)];
+      in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end));
 
 
 (* formal entities *)