# HG changeset patch
# User wenzelm
# Date 1447441168 -3600
# Node ID 78b37164465482a7ecdaa3c1ae5f0dbd685234dd
# Parent  ffee6aea0ff2256b2f4c2d5a332c92866bbc71da
added antiquotation @{doc}, e.g. useful for demonstration purposes;

diff -r ffee6aea0ff2 -r 78b371644654 NEWS
--- a/NEWS	Fri Nov 13 17:48:33 2015 +0100
+++ b/NEWS	Fri Nov 13 19:59:28 2015 +0100
@@ -95,6 +95,9 @@
 (outer syntax with command keywords etc.). This may be used in the short
 form \<^theory_text>\<open>...\<close>.
 
+* Antiquotation @{doc ENTRY} provides a reference to the given
+documentation, with a hyperlink in the Prover IDE.
+
 * Antiquotations @{command}, @{method}, @{attribute} print checked
 entities of the Isar language.
 
diff -r ffee6aea0ff2 -r 78b371644654 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Nov 13 19:59:28 2015 +0100
@@ -62,6 +62,7 @@
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
+  val docN: string val doc: string -> T
   val indentN: string
   val blockN: string val block: int -> T
   val widthN: string
@@ -371,6 +372,7 @@
 
 val (pathN, path) = markup_string "path" nameN;
 val (urlN, url) = markup_string "url" nameN;
+val (docN, doc) = markup_string "doc" nameN;
 
 
 (* pretty printing *)
diff -r ffee6aea0ff2 -r 78b371644654 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Nov 13 19:59:28 2015 +0100
@@ -174,6 +174,9 @@
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 
+  val DOC = "doc"
+  val Doc = new Markup_String(DOC, NAME)
+
 
   /* pretty printing */
 
diff -r ffee6aea0ff2 -r 78b371644654 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Nov 13 19:59:28 2015 +0100
@@ -173,6 +173,15 @@
        enclose "\\url{" "}" name)));
 
 
+(* doc entries *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
+    (fn {context = ctxt, ...} => fn (name, pos) =>
+      (Context_Position.report ctxt pos (Markup.doc name);
+        Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
+
+
 (* formal entities *)
 
 fun entity_antiquotation name check output =
diff -r ffee6aea0ff2 -r 78b371644654 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Nov 13 19:59:28 2015 +0100
@@ -56,18 +56,7 @@
       case Text_File(_, path) =>
         PIDE.editor.goto_file(true, view, File.platform_path(path))
       case Documentation(_, _, path) =>
-        if (path.is_file)
-          PIDE.editor.goto_file(true, view, File.platform_path(path))
-        else {
-          Standard_Thread.fork("documentation") {
-            try { Doc.view(path) }
-            catch {
-              case exn: Throwable =>
-                GUI.error_dialog(view,
-                  "Documentation error", GUI.scrollable_text(Exn.message(exn)))
-            }
-          }
-        }
+        PIDE.editor.goto_doc(view, path)
       case _ =>
     }
   }
diff -r ffee6aea0ff2 -r 78b371644654 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Nov 13 19:59:28 2015 +0100
@@ -187,9 +187,35 @@
     }
   }
 
+  def goto_doc(view: View, path: Path)
+  {
+    if (path.is_file)
+      goto_file(true, view, File.platform_path(path))
+    else {
+      Standard_Thread.fork("documentation") {
+        try { Doc.view(path) }
+        catch {
+          case exn: Throwable =>
+            GUI.error_dialog(view,
+              "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+        }
+      }
+    }
+  }
+
 
   /* hyperlinks */
 
+  def hyperlink_doc(name: String): Option[Hyperlink] =
+    Doc.contents().collectFirst({
+      case doc: Doc.Text_File if doc.name == name => doc.path
+      case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
+        new Hyperlink {
+          val external = !path.is_file
+          def follow(view: View): Unit = goto_doc(view, path)
+          override def toString: String = "doc " + quote(name)
+        })
+
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
       val external = true
diff -r ffee6aea0ff2 -r 78b371644654 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Nov 13 19:59:28 2015 +0100
@@ -159,7 +159,8 @@
       Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
-    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,
+      Markup.CITATION, Markup.URL)
 
   private val active_elements =
     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
@@ -418,6 +419,10 @@
             val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
+          case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
+            PIDE.editor.hyperlink_doc(name).map(link =>
+              (links :+ Text.Info(snapshot.convert(info_range), link)))
+
           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
             val link = PIDE.editor.hyperlink_url(name)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))