changeset 72843 | dd56ba1974e6 |
parent 72841 | fd8d82c4433b |
child 73752 | eeb076fc569f |
--- a/src/Pure/Thy/document_antiquotations.ML Mon Dec 07 16:24:39 2020 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Mon Dec 07 16:28:44 2020 +0100 @@ -323,7 +323,7 @@ val delimited = Input.is_delimited source; val _ = Context_Position.reports ctxt - [(pos, Markup.language_path delimited), (pos, Markup.url url)]; + [(pos, Markup.language_url delimited), (pos, Markup.url url)]; in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end));