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

     2.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 09:44:57 2013 +0100
     2.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 12:16:52 2013 +0100
     2.3 @@ -125,6 +125,7 @@
     2.4      @{antiquotation_def ML_type} & : & @{text antiquotation} \\
     2.5      @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
     2.6      @{antiquotation_def "file"} & : & @{text antiquotation} \\
     2.7 +    @{antiquotation_def "url"} & : & @{text antiquotation} \\
     2.8    \end{matharray}
     2.9  
    2.10    The overall content of an Isabelle/Isar theory may alternate between
    2.11 @@ -175,7 +176,8 @@
    2.12        @@{antiquotation ML_op} options @{syntax name} |
    2.13        @@{antiquotation ML_type} options @{syntax name} |
    2.14        @@{antiquotation ML_struct} options @{syntax name} |
    2.15 -      @@{antiquotation \"file\"} options @{syntax name}
    2.16 +      @@{antiquotation \"file\"} options @{syntax name} |
    2.17 +      @@{antiquotation url} options @{syntax name}
    2.18      ;
    2.19      options: '[' (option * ',') ']'
    2.20      ;
    2.21 @@ -267,6 +269,9 @@
    2.22    \item @{text "@{file path}"} checks that @{text "path"} refers to a
    2.23    file (or directory) and prints it verbatim.
    2.24  
    2.25 +  \item @{text "@{url name}"} produces markup for the given URL, which
    2.26 +  results in an active hyperlink within the text.
    2.27 +
    2.28    \end{description}
    2.29  *}
    2.30  

     3.1 --- a/src/Pure/General/url.ML	Mon Dec 09 09:44:57 2013 +0100
     3.2 +++ b/src/Pure/General/url.ML	Mon Dec 09 12:16:52 2013 +0100
     3.3 @@ -14,6 +14,8 @@
     3.4    val append: T -> T -> T
     3.5    val implode: T -> string
     3.6    val explode: string -> T
     3.7 +  val pretty: T -> Pretty.T
     3.8 +  val print: T -> string
     3.9  end;
    3.10  
    3.11  structure Url: URL =
    3.12 @@ -75,6 +77,13 @@
    3.13  end;
    3.14  
    3.15  
    3.16 +(* print *)
    3.17 +
    3.18 +val pretty = Pretty.mark_str o `Markup.url o implode_url;
    3.19 +
    3.20 +val print = Pretty.str_of o pretty;
    3.21 +
    3.22 +
    3.23  (*final declarations of this structure!*)
    3.24  val implode = implode_url;
    3.25  val explode = explode_url;

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

     5.1 --- a/src/Pure/PIDE/markup.ML	Mon Dec 09 09:44:57 2013 +0100
     5.2 +++ b/src/Pure/PIDE/markup.ML	Mon Dec 09 12:16:52 2013 +0100
     5.3 @@ -34,6 +34,7 @@
     5.4    val position_properties: string list
     5.5    val positionN: string val position: T
     5.6    val pathN: string val path: string -> T
     5.7 +  val urlN: string val url: string -> T
     5.8    val indentN: string
     5.9    val blockN: string val block: int -> T
    5.10    val widthN: string
    5.11 @@ -258,9 +259,10 @@
    5.12  val (positionN, position) = markup_elem "position";
    5.13  
    5.14  
    5.15 -(* path *)
    5.16 +(* external resources *)
    5.17  
    5.18  val (pathN, path) = markup_string "path" nameN;
    5.19 +val (urlN, url) = markup_string "url" nameN;
    5.20  
    5.21  
    5.22  (* pretty printing *)

     6.1 --- a/src/Pure/PIDE/markup.scala	Mon Dec 09 09:44:57 2013 +0100
     6.2 +++ b/src/Pure/PIDE/markup.scala	Mon Dec 09 12:16:52 2013 +0100
     6.3 @@ -67,7 +67,7 @@
     6.4    val POSITION = "position"
     6.5  
     6.6  
     6.7 -  /* path */
     6.8 +  /* external resources */
     6.9  
    6.10    val PATH = "path"
    6.11  
    6.12 @@ -80,6 +80,17 @@
    6.13        }
    6.14    }
    6.15  
    6.16 +  val URL = "url"
    6.17 +
    6.18 +  object Url
    6.19 +  {
    6.20 +    def unapply(markup: Markup): Option[String] =
    6.21 +      markup match {
    6.22 +        case Markup(URL, Name(name)) => Some(name)
    6.23 +        case _ => None
    6.24 +      }
    6.25 +  }
    6.26 +
    6.27  
    6.28    /* pretty printing */
    6.29  

     7.1 --- a/src/Pure/Thy/thy_output.ML	Mon Dec 09 09:44:57 2013 +0100
     7.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Dec 09 12:16:52 2013 +0100
     7.3 @@ -661,4 +661,12 @@
     7.4  
     7.5  end;
     7.6  
     7.7 +
     7.8 +(* URLs *)
     7.9 +
    7.10 +val _ = Theory.setup
    7.11 +  (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
    7.12 +    (fn {context = ctxt, ...} => fn (name, pos) =>
    7.13 +      (Position.report pos (Markup.url name); enclose "\\url{" "}" name)));
    7.14 +
    7.15  end;

     8.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 09:44:57 2013 +0100
     8.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 12:16:52 2013 +0100
     8.3 @@ -135,6 +135,17 @@
     8.4      }
     8.5    }
     8.6  
     8.7 +  override def hyperlink_url(name: String): Hyperlink =
     8.8 +    new Hyperlink {
     8.9 +      def follow(view: View) =
    8.10 +        default_thread_pool.submit(() =>
    8.11 +          try { Isabelle_System.open(name) }
    8.12 +          catch {
    8.13 +            case exn: Throwable =>
    8.14 +              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    8.15 +          })
    8.16 +    }
    8.17 +
    8.18    override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
    8.19      new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
    8.20  

     9.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Dec 09 09:44:57 2013 +0100
     9.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Dec 09 12:16:52 2013 +0100
     9.3 @@ -202,8 +202,9 @@
     9.4  
     9.5    private val highlight_include =
     9.6      Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
     9.7 -      Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
     9.8 -      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
     9.9 +      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
    9.10 +      Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
    9.11 +      Markup.DOCUMENT_SOURCE)
    9.12  
    9.13    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    9.14    {
    9.15 @@ -217,7 +218,7 @@
    9.16    }
    9.17  
    9.18  
    9.19 -  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
    9.20 +  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL)
    9.21  
    9.22    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    9.23    {
    9.24 @@ -230,6 +231,10 @@
    9.25              val link = PIDE.editor.hyperlink_file(jedit_file)
    9.26              Some(Text.Info(snapshot.convert(info_range), link) :: links)
    9.27  
    9.28 +          case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    9.29 +            val link = PIDE.editor.hyperlink_url(name)
    9.30 +            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    9.31 +
    9.32            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    9.33            if !props.exists(
    9.34              { case (Markup.KIND, Markup.ML_OPEN) => true
    9.35 @@ -335,7 +340,7 @@
    9.36  
    9.37    private val tooltip_elements =
    9.38      Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
    9.39 -      Markup.ML_TYPING, Markup.PATH) ++ tooltips.keys
    9.40 +      Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
    9.41  
    9.42    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    9.43      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    9.44 @@ -371,6 +376,8 @@
    9.45            if Path.is_ok(name) =>
    9.46              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    9.47              Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
    9.48 +          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
    9.49 +            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
    9.50            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    9.51            if name == Markup.SORTING || name == Markup.TYPING =>
    9.52              Some(add(prev, r, (true, pretty_typing("::", body))))