src/Pure/Thy/thy_output.ML

 
   ml_text (Binding.name "ML_text") (K (K [])));
 
 end;
 
-end;
+
+(* URLs *)
+
+val _ = Theory.setup
+  (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
+    (fn {context = ctxt, ...} => fn (name, pos) =>
+      (Position.report pos (Markup.url name); enclose "\\url{" "}" name)));
+
+end;