added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;

--- a/NEWS	Mon Dec 09 09:44:57 2013 +0100
+++ b/NEWS	Mon Dec 09 12:16:52 2013 +0100
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Document antiquotation @{url} produces markup for the given URL,
+which results in an active hyperlink within the text.
+
+
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.

--- a/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 12:16:52 2013 +0100
@@ -125,6 +125,7 @@
     @{antiquotation_def ML_type} & : & @{text antiquotation} \\
     @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
     @{antiquotation_def "file"} & : & @{text antiquotation} \\
+    @{antiquotation_def "url"} & : & @{text antiquotation} \\
   \end{matharray}
 
   The overall content of an Isabelle/Isar theory may alternate between
@@ -175,7 +176,8 @@
       @@{antiquotation ML_op} options @{syntax name} |
       @@{antiquotation ML_type} options @{syntax name} |
       @@{antiquotation ML_struct} options @{syntax name} |
-      @@{antiquotation \"file\"} options @{syntax name}
+      @@{antiquotation \"file\"} options @{syntax name} |
+      @@{antiquotation url} options @{syntax name}
     ;
     options: '[' (option * ',') ']'
     ;
@@ -267,6 +269,9 @@
   \item @{text "@{file path}"} checks that @{text "path"} refers to a
   file (or directory) and prints it verbatim.
 
+  \item @{text "@{url name}"} produces markup for the given URL, which
+  results in an active hyperlink within the text.
+
   \end{description}
 *}
 

--- a/src/Pure/General/url.ML	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Pure/General/url.ML	Mon Dec 09 12:16:52 2013 +0100
@@ -14,6 +14,8 @@
   val append: T -> T -> T
   val implode: T -> string
   val explode: string -> T
+  val pretty: T -> Pretty.T
+  val print: T -> string
 end;
 
 structure Url: URL =
@@ -75,6 +77,13 @@
 end;
 
 
+(* print *)
+
+val pretty = Pretty.mark_str o `Markup.url o implode_url;
+
+val print = Pretty.str_of o pretty;
+
+
 (*final declarations of this structure!*)
 val implode = implode_url;
 val explode = explode_url;

--- a/src/Pure/PIDE/editor.scala	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Dec 09 12:16:52 2013 +0100
@@ -23,6 +23,7 @@
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
   abstract class Hyperlink { def follow(context: Context): Unit }
+  def hyperlink_url(name: String): Hyperlink
   def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
   def hyperlink_command(
     snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]

--- a/src/Pure/PIDE/markup.ML	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Dec 09 12:16:52 2013 +0100
@@ -34,6 +34,7 @@
   val position_properties: string list
   val positionN: string val position: T
   val pathN: string val path: string -> T
+  val urlN: string val url: string -> T
   val indentN: string
   val blockN: string val block: int -> T
   val widthN: string
@@ -258,9 +259,10 @@
 val (positionN, position) = markup_elem "position";
 
 
-(* path *)
+(* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
+val (urlN, url) = markup_string "url" nameN;
 
 
 (* pretty printing *)

--- a/src/Pure/PIDE/markup.scala	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Dec 09 12:16:52 2013 +0100
@@ -67,7 +67,7 @@
   val POSITION = "position"
 
 
-  /* path */
+  /* external resources */
 
   val PATH = "path"
 
@@ -80,6 +80,17 @@
       }
   }
 
+  val URL = "url"
+
+  object Url
+  {
+    def unapply(markup: Markup): Option[String] =
+      markup match {
+        case Markup(URL, Name(name)) => Some(name)
+        case _ => None
+      }
+  }
+
 
   /* pretty printing */
 

--- 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;

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 12:16:52 2013 +0100
@@ -135,6 +135,17 @@
     }
   }
 
+  override def hyperlink_url(name: String): Hyperlink =
+    new Hyperlink {
+      def follow(view: View) =
+        default_thread_pool.submit(() =>
+          try { Isabelle_System.open(name) }
+          catch {
+            case exn: Throwable =>
+              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+          })
+    }
+
   override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
 

--- a/src/Tools/jEdit/src/rendering.scala	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Dec 09 12:16:52 2013 +0100
@@ -202,8 +202,9 @@
 
   private val highlight_include =
     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
-      Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
-      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
+      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
+      Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
+      Markup.DOCUMENT_SOURCE)
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
@@ -217,7 +218,7 @@
   }
 
 
-  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
+  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL)
 
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
@@ -230,6 +231,10 @@
             val link = PIDE.editor.hyperlink_file(jedit_file)
             Some(Text.Info(snapshot.convert(info_range), link) :: links)
 
+          case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
+            val link = PIDE.editor.hyperlink_url(name)
+            Some(Text.Info(snapshot.convert(info_range), link) :: links)
+
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
           if !props.exists(
             { case (Markup.KIND, Markup.ML_OPEN) => true
@@ -335,7 +340,7 @@
 
   private val tooltip_elements =
     Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
-      Markup.ML_TYPING, Markup.PATH) ++ tooltips.keys
+      Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
 
   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
@@ -371,6 +376,8 @@
           if Path.is_ok(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
+          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
+            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
             Some(add(prev, r, (true, pretty_typing("::", body))))