# HG changeset patch
# User wenzelm
# Date 1396904549 -7200
# Node ID a8d960baa5c28ed1ae873324716a3912e198736d
# Parent  eea4bbe157455dc1f0296435398790e5efc90d5d
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;

diff -r eea4bbe15745 -r a8d960baa5c2 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Apr 07 21:23:02 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Apr 07 23:02:29 2014 +0200
@@ -6,7 +6,7 @@
 
 signature COMMAND =
 sig
-  type blob = (string * string * (SHA1.digest * string list) option) Exn.result
+  type blob = (string * (SHA1.digest * string list) option) Exn.result
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
   val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
   type eval
@@ -87,7 +87,7 @@
 (* read *)
 
 type blob =
-  (string * string * (SHA1.digest * string list) option) Exn.result;  (*file, path, digest, lines*)
+  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
 
 fun read_file master_dir pos src_path =
   let
@@ -115,16 +115,16 @@
     [span] => span
       |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
         let
-          fun make_file src_path (Exn.Res (_, _, NONE)) =
+          fun make_file src_path (Exn.Res (_, NONE)) =
                 Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
-            | make_file src_path (Exn.Res (file_node, file_path, SOME (digest, lines))) =
-               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_path)];
+            | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
+               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
                 Exn.Res (blob_file src_path lines digest file_node))
             | make_file _ (Exn.Exn e) = Exn.Exn e;
           val src_paths = Keyword.command_files cmd path;
         in
           if null blobs then
-            map2 make_file src_paths (map (K (Exn.Res ("", "", NONE))) src_paths)
+            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
           else if length src_paths = length blobs then
             map2 make_file src_paths blobs
           else error ("Misalignment of inlined files" ^ Position.here pos)
diff -r eea4bbe15745 -r a8d960baa5c2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Apr 07 21:23:02 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 07 23:02:29 2014 +0200
@@ -18,7 +18,7 @@
   type state
   val init_state: state
   val define_blob: string -> string -> state -> state
-  type blob_digest = (string * string * string option) Exn.result
+  type blob_digest = (string * string option) Exn.result
   val define_command: Document_ID.command -> string -> blob_digest list -> string ->
     state -> state
   val remove_versions: Document_ID.version list -> state -> state
@@ -219,8 +219,7 @@
 
 (** main state -- document structure and execution process **)
 
-type blob_digest =
-  (string * string * string option) Exn.result;  (* file node name, path, raw digest*)
+type blob_digest = (string * string option) Exn.result;  (*file node name, raw digest*)
 
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
@@ -293,8 +292,8 @@
   | SOME content => content);
 
 fun resolve_blob state (blob_digest: blob_digest) =
-  blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
-    (file, path, Option.map (the_blob state) raw_digest));
+  blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
+    (file_node, Option.map (the_blob state) raw_digest));
 
 
 (* commands *)
@@ -343,7 +342,7 @@
     val blobs' =
       (commands', Symtab.empty) |->
         Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
-          fold (fn Exn.Res (_, _, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
+          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
 
   in (versions', blobs', commands', execution) end);
 
diff -r eea4bbe15745 -r a8d960baa5c2 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Apr 07 21:23:02 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Apr 07 23:02:29 2014 +0200
@@ -34,7 +34,7 @@
           YXML.parse_body blobs_yxml |>
             let open XML.Decode in
               list (variant
-               [fn ([], a) => Exn.Res (triple string string (option string) a),
+               [fn ([], a) => Exn.Res (pair string (option string) a),
                 fn ([], a) => Exn.Exn (ERROR (string a))])
             end;
       in
diff -r eea4bbe15745 -r a8d960baa5c2 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Apr 07 21:23:02 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Apr 07 23:02:29 2014 +0200
@@ -352,8 +352,7 @@
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
-              (Nil, triple(string, string, option(string))(
-                (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
+              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
       YXML.string_of_body(list(encode_blob)(command.blobs))
     }
diff -r eea4bbe15745 -r a8d960baa5c2 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 21:23:02 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 23:02:29 2014 +0200
@@ -195,26 +195,32 @@
   def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
     : Option[Hyperlink] =
   {
-    if (Path.is_valid(source_name)) {
-      Isabelle_System.source_file(Path.explode(source_name)) match {
-        case Some(path) =>
-          val name = Isabelle_System.platform_path(path)
-          JEdit_Lib.jedit_buffer(name) match {
-            case Some(buffer) if offset > 0 =>
-              val (line, column) =
-                JEdit_Lib.buffer_lock(buffer) {
-                  ((1, 1) /:
-                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
-                        Symbol.advance_line_column)
-                }
-              Some(hyperlink_file(name, line, column))
-            case _ => Some(hyperlink_file(name, line))
-          }
-        case None => None
+    val opt_name =
+      if (Path.is_wellformed(source_name)) {
+        if (Path.is_valid(source_name)) {
+          val path = Path.explode(source_name)
+          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
+        }
+        else None
       }
+      else Some(source_name)
+
+    opt_name match {
+      case Some(name) =>
+        JEdit_Lib.jedit_buffer(name) match {
+          case Some(buffer) if offset > 0 =>
+            val (line, column) =
+              JEdit_Lib.buffer_lock(buffer) {
+                ((1, 1) /:
+                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
+                      Symbol.advance_line_column)
+              }
+            Some(hyperlink_file(name, line, column))
+          case _ => Some(hyperlink_file(name, line))
+        }
+      case None => None
     }
-    else None
   }
 
   def hyperlink_url(name: String): Hyperlink =
diff -r eea4bbe15745 -r a8d960baa5c2 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Apr 07 21:23:02 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Apr 07 23:02:29 2014 +0200
@@ -321,15 +321,18 @@
 
   /* hyperlinks */
 
+  private def jedit_file(name: String): String =
+    if (Path.is_valid(name))
+      PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
+    else name
+
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
       range, Vector.empty, Rendering.hyperlink_elements, _ =>
         {
-          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
-          if Path.is_valid(name) =>
-            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
-            val link = PIDE.editor.hyperlink_file(jedit_file)
+          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
+            val link = PIDE.editor.hyperlink_file(jedit_file(name))
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
@@ -457,10 +460,11 @@
                 "\n" + t.message
               else ""
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
-          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
-          if Path.is_valid(name) =>
-            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
-            val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
+          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
+            val file = jedit_file(name)
+            val text =
+              if (name == file) "file " + quote(file)
+              else "path " + quote(name) + "\nfile " + quote(file)
             Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))