clarified links to external files, e.g. .pdf within .thy source document;

--- a/NEWS	Mon Feb 01 18:12:44 2021 +0100
+++ b/NEWS	Wed Feb 03 20:18:34 2021 +0100
@@ -73,6 +73,9 @@
 Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
 .ftl.tex extension.
 
+* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
+viewer, instead of re-using the jEdit text editor.
+
 
 *** Document preparation ***
 

--- a/etc/settings	Mon Feb 01 18:12:44 2021 +0100
+++ b/etc/settings	Wed Feb 03 20:18:34 2021 +0100
@@ -112,7 +112,7 @@
 
 
 ###
-### Docs
+### Docs and external files
 ###
 
 # Where to look for docs (multiple dirs separated by ':').
@@ -136,6 +136,8 @@
 
 PDF_VIEWER="$ISABELLE_OPEN"
 
+ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp"
+
 
 ###
 ### Symbol rendering

--- a/src/Pure/System/isabelle_system.scala	Mon Feb 01 18:12:44 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Wed Feb 03 20:18:34 2021 +0100
@@ -404,12 +404,24 @@
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
+  def open_external_file(name: String): Boolean =
+  {
+    val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
+    val external =
+      ext.nonEmpty &&
+      Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
+    if (external) {
+      if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
+      else open(name)
+    }
+    external
+  }
+
   def export_isabelle_identifier(isabelle_identifier: String): String =
     if (isabelle_identifier == "") ""
     else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
 
 
-
   /** Isabelle resources **/
 
   /* repository clone with Admin */

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 01 18:12:44 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Feb 03 20:18:34 2021 +0100
@@ -166,7 +166,7 @@
           catch { case ERROR(_) => false }
 
         if (is_dir) VFSBrowser.browseDirectory(view, name)
-        else {
+        else if (!Isabelle_System.open_external_file(name)) {
           val args =
             if (line <= 0) Array(name)
             else if (column <= 0) Array(name, "+line:" + (line + 1))