added antiquotation @{doc}, e.g. useful for demonstration purposes;
authorwenzelm
Fri Nov 13 19:59:28 2015 +0100 (2015-11-13)
changeset 6166078b371644654
parent 61659 ffee6aea0ff2
child 61661 0932dc251248
added antiquotation @{doc}, e.g. useful for demonstration purposes;
NEWS
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/document_antiquotations.ML
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/NEWS	Fri Nov 13 17:48:33 2015 +0100
     1.2 +++ b/NEWS	Fri Nov 13 19:59:28 2015 +0100
     1.3 @@ -95,6 +95,9 @@
     1.4  (outer syntax with command keywords etc.). This may be used in the short
     1.5  form \<^theory_text>\<open>...\<close>.
     1.6  
     1.7 +* Antiquotation @{doc ENTRY} provides a reference to the given
     1.8 +documentation, with a hyperlink in the Prover IDE.
     1.9 +
    1.10  * Antiquotations @{command}, @{method}, @{attribute} print checked
    1.11  entities of the Isar language.
    1.12  
     2.1 --- a/src/Pure/PIDE/markup.ML	Fri Nov 13 17:48:33 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Fri Nov 13 19:59:28 2015 +0100
     2.3 @@ -62,6 +62,7 @@
     2.4    val citationN: string val citation: string -> T
     2.5    val pathN: string val path: string -> T
     2.6    val urlN: string val url: string -> T
     2.7 +  val docN: string val doc: string -> T
     2.8    val indentN: string
     2.9    val blockN: string val block: int -> T
    2.10    val widthN: string
    2.11 @@ -371,6 +372,7 @@
    2.12  
    2.13  val (pathN, path) = markup_string "path" nameN;
    2.14  val (urlN, url) = markup_string "url" nameN;
    2.15 +val (docN, doc) = markup_string "doc" nameN;
    2.16  
    2.17  
    2.18  (* pretty printing *)
     3.1 --- a/src/Pure/PIDE/markup.scala	Fri Nov 13 17:48:33 2015 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Fri Nov 13 19:59:28 2015 +0100
     3.3 @@ -174,6 +174,9 @@
     3.4    val URL = "url"
     3.5    val Url = new Markup_String(URL, NAME)
     3.6  
     3.7 +  val DOC = "doc"
     3.8 +  val Doc = new Markup_String(DOC, NAME)
     3.9 +
    3.10  
    3.11    /* pretty printing */
    3.12  
     4.1 --- a/src/Pure/Thy/document_antiquotations.ML	Fri Nov 13 17:48:33 2015 +0100
     4.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Fri Nov 13 19:59:28 2015 +0100
     4.3 @@ -173,6 +173,15 @@
     4.4         enclose "\\url{" "}" name)));
     4.5  
     4.6  
     4.7 +(* doc entries *)
     4.8 +
     4.9 +val _ = Theory.setup
    4.10 +  (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
    4.11 +    (fn {context = ctxt, ...} => fn (name, pos) =>
    4.12 +      (Context_Position.report ctxt pos (Markup.doc name);
    4.13 +        Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
    4.14 +
    4.15 +
    4.16  (* formal entities *)
    4.17  
    4.18  fun entity_antiquotation name check output =
     5.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Nov 13 17:48:33 2015 +0100
     5.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Nov 13 19:59:28 2015 +0100
     5.3 @@ -56,18 +56,7 @@
     5.4        case Text_File(_, path) =>
     5.5          PIDE.editor.goto_file(true, view, File.platform_path(path))
     5.6        case Documentation(_, _, path) =>
     5.7 -        if (path.is_file)
     5.8 -          PIDE.editor.goto_file(true, view, File.platform_path(path))
     5.9 -        else {
    5.10 -          Standard_Thread.fork("documentation") {
    5.11 -            try { Doc.view(path) }
    5.12 -            catch {
    5.13 -              case exn: Throwable =>
    5.14 -                GUI.error_dialog(view,
    5.15 -                  "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    5.16 -            }
    5.17 -          }
    5.18 -        }
    5.19 +        PIDE.editor.goto_doc(view, path)
    5.20        case _ =>
    5.21      }
    5.22    }
     6.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Nov 13 17:48:33 2015 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Nov 13 19:59:28 2015 +0100
     6.3 @@ -187,9 +187,35 @@
     6.4      }
     6.5    }
     6.6  
     6.7 +  def goto_doc(view: View, path: Path)
     6.8 +  {
     6.9 +    if (path.is_file)
    6.10 +      goto_file(true, view, File.platform_path(path))
    6.11 +    else {
    6.12 +      Standard_Thread.fork("documentation") {
    6.13 +        try { Doc.view(path) }
    6.14 +        catch {
    6.15 +          case exn: Throwable =>
    6.16 +            GUI.error_dialog(view,
    6.17 +              "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    6.18 +        }
    6.19 +      }
    6.20 +    }
    6.21 +  }
    6.22 +
    6.23  
    6.24    /* hyperlinks */
    6.25  
    6.26 +  def hyperlink_doc(name: String): Option[Hyperlink] =
    6.27 +    Doc.contents().collectFirst({
    6.28 +      case doc: Doc.Text_File if doc.name == name => doc.path
    6.29 +      case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
    6.30 +        new Hyperlink {
    6.31 +          val external = !path.is_file
    6.32 +          def follow(view: View): Unit = goto_doc(view, path)
    6.33 +          override def toString: String = "doc " + quote(name)
    6.34 +        })
    6.35 +
    6.36    def hyperlink_url(name: String): Hyperlink =
    6.37      new Hyperlink {
    6.38        val external = true
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Nov 13 17:48:33 2015 +0100
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Nov 13 19:59:28 2015 +0100
     7.3 @@ -159,7 +159,8 @@
     7.4        Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
     7.5  
     7.6    private val hyperlink_elements =
     7.7 -    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
     7.8 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,
     7.9 +      Markup.CITATION, Markup.URL)
    7.10  
    7.11    private val active_elements =
    7.12      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    7.13 @@ -418,6 +419,10 @@
    7.14              val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
    7.15              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    7.16  
    7.17 +          case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
    7.18 +            PIDE.editor.hyperlink_doc(name).map(link =>
    7.19 +              (links :+ Text.Info(snapshot.convert(info_range), link)))
    7.20 +
    7.21            case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    7.22              val link = PIDE.editor.hyperlink_url(name)
    7.23              Some(links :+ Text.Info(snapshot.convert(info_range), link))