# HG changeset patch
# User wenzelm
# Date 1607354924 -3600
# Node ID dd56ba1974e6ab019cc2def1e223ec5ab407197a
# Parent  6aae62f55c2b5cb5cc03d4d416d04f3874f3c9ad
clarified markup (refining 1c59b555ac4a);

diff -r 6aae62f55c2b -r dd56ba1974e6 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Dec 07 16:24:39 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Dec 07 16:28:44 2020 +0100
@@ -45,6 +45,7 @@
   val language_latex: bool -> T
   val language_rail: T
   val language_path: bool -> T
+  val language_url: bool -> T
   val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
@@ -345,6 +346,7 @@
 val language_latex = language' {name = "latex", symbols = false, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language' {name = "path", symbols = false, antiquotes = false};
+val language_url = language' {name = "url", symbols = false, antiquotes = false};
 val language_mixfix =
   language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
diff -r 6aae62f55c2b -r dd56ba1974e6 src/Pure/Thy/document_antiquotations.ML
--- 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));