src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Dec 09 12:16:52 2013 +0100
@@ -661,4 +661,12 @@
 
 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;