escape some special chars, notably for URL#NAME form;

--- 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 *)