more PIDE markup and hyperlinks;

--- a/src/Pure/PIDE/markup.ML	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Mar 30 22:51:38 2019 +0100
@@ -65,6 +65,7 @@
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
+  val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
   val markupN: string
@@ -397,6 +398,7 @@
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
+val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
 

--- a/src/Pure/PIDE/markup.scala	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Mar 30 22:51:38 2019 +0100
@@ -200,6 +200,9 @@
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
+  val EXPORT_PATH = "export_path"
+  val Export_Path = new Markup_String(EXPORT_PATH, NAME)
+
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 

--- a/src/Pure/Thy/export.ML	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Pure/Thy/export.ML	Sat Mar 30 22:51:38 2019 +0100
@@ -23,14 +23,23 @@
 
 type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool};
 
-fun export_params ({theory, binding, executable, compress}: params) blob =
-  (Output.try_protocol_message o Markup.export)
-   {id = Position.get_id (Position.thread_data ()),
-    serial = serial (),
-    theory_name = Context.theory_long_name theory,
-    name = Path.implode_binding binding,
-    executable = executable,
-    compress = compress} blob;
+fun export_params ({theory = thy, binding, executable, compress}: params) blob =
+  let
+    val theory_name = Context.theory_long_name thy;
+    val name = Path.implode_binding binding;
+    val (path, pos) = Path.dest_binding binding;
+    val _ =
+      Context_Position.report_generic (Context.Theory thy) pos
+        (Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)));
+  in
+    (Output.try_protocol_message o Markup.export)
+     {id = Position.get_id (Position.thread_data ()),
+      serial = serial (),
+      theory_name = theory_name,
+      name = name,
+      executable = executable,
+      compress = compress} blob
+  end;
 
 fun export thy binding blob =
   export_params {theory = thy, binding = binding, executable = false, compress = true} blob;

--- a/src/Tools/jEdit/src/active.scala	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Tools/jEdit/src/active.scala	Sat Mar 30 22:51:38 2019 +0100
@@ -47,7 +47,7 @@
               case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
                 GUI_Thread.later {
                   val name = Markup.Name.unapply(props) getOrElse ""
-                  VFSBrowser.browseDirectory(view, Isabelle_Export.vfs_prefix + name)
+                  PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
                 }
 
               case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 30 22:51:38 2019 +0100
@@ -14,6 +14,7 @@
 
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.browser.VFSBrowser
+import org.gjt.sp.jedit.io.{VFSManager, VFSFile}
 
 
 class JEdit_Editor extends Editor[View]
@@ -155,15 +156,23 @@
           case _: IllegalArgumentException =>
         }
 
-      case None if (new JFile(name)).isDirectory =>
-        VFSBrowser.browseDirectory(view, name)
+      case None =>
+        val is_file =
+          try {
+            val vfs = VFSManager.getVFSForPath(name)
+            val vfs_file = vfs._getFile((), name, view)
+            vfs_file != null && vfs_file.getType == VFSFile.FILE
+          }
+          catch { case ERROR(_) => false }
 
-      case None =>
-        val args =
-          if (line <= 0) Array(name)
-          else if (column <= 0) Array(name, "+line:" + (line + 1))
-          else Array(name, "+line:" + (line + 1) + "," + (column + 1))
-        jEdit.openFiles(view, null, args)
+        if (is_file) {
+          val args =
+            if (line <= 0) Array(name)
+            else if (column <= 0) Array(name, "+line:" + (line + 1))
+            else Array(name, "+line:" + (line + 1) + "," + (column + 1))
+          jEdit.openFiles(view, null, args)
+        }
+        else VFSBrowser.browseDirectory(view, name)
     }
   }
 

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Mar 30 22:51:38 2019 +0100
@@ -124,8 +124,8 @@
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
-    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.POSITION,
-      Markup.CITATION)
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL,
+      Markup.POSITION, Markup.CITATION)
 
   private val gutter_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
@@ -242,6 +242,10 @@
             val link = PIDE.editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
+          case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) =>
+            val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + 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)))