# HG changeset patch
# User wenzelm
# Date 1345833707 -7200
# Node ID a2df77fcf1ebb630232cf8d202e9f03340942887
# Parent  6f3ccfa7818dcb3c94d3d81a001f70518970333f
prefer jEdit file name representation (potentially via VFS);
tuned;

diff -r 6f3ccfa7818d -r a2df77fcf1eb src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 24 19:35:44 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 24 20:41:47 2012 +0200
@@ -283,6 +283,7 @@
   {
     val state: State
     val version: Version
+    val node_name: Node.Name
     val node: Node
     val is_outdated: Boolean
     def convert(i: Text.Offset): Text.Offset
@@ -493,6 +494,7 @@
       {
         val state = State.this
         val version = stable.version.get_finished
+        val node_name = name
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
 
diff -r 6f3ccfa7818d -r a2df77fcf1eb src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Aug 24 19:35:44 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Aug 24 20:41:47 2012 +0200
@@ -124,19 +124,16 @@
   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
 
 
-  /* source files */
+  /* source files of Isabelle/ML bootstrap */
 
-  private def try_file(file: JFile) = if (file.isFile) Some(file) else None
-
-  def source_file(path: Path): Option[JFile] =
+  def source_file(path: Path): Option[Path] =
   {
-    if (path.is_absolute || path.is_current)
-      try_file(platform_file(path))
+    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
+
+    if (path.is_absolute || path.is_current) check(path)
     else {
-      val pure_file = (Path.explode("~~/src/Pure") + path).file
-      if (pure_file.isFile) Some(pure_file)
-      else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
-      else None
+      check(Path.explode("~~/src/Pure") + path) orElse
+        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
     }
   }
 
diff -r 6f3ccfa7818d -r a2df77fcf1eb src/Tools/jEdit/src/hyperlink.scala
--- a/src/Tools/jEdit/src/hyperlink.scala	Fri Aug 24 19:35:44 2012 +0200
+++ b/src/Tools/jEdit/src/hyperlink.scala	Fri Aug 24 20:41:47 2012 +0200
@@ -10,16 +10,14 @@
 
 import isabelle._
 
-import java.io.{File => JFile}
-
 import org.gjt.sp.jedit.{View, jEdit}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
 object Hyperlink
 {
-  def apply(file: JFile, line: Int, column: Int): Hyperlink =
-    File_Link(file, line, column)
+  def apply(jedit_file: String, line: Int, column: Int): Hyperlink =
+    File_Link(jedit_file, line, column)
 }
 
 abstract class Hyperlink
@@ -27,16 +25,13 @@
   def follow(view: View): Unit
 }
 
-private case class File_Link(file: JFile, line: Int, column: Int) extends Hyperlink
+private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink
 {
   override def follow(view: View)
   {
     Swing_Thread.require()
 
-    val full_name = file.getCanonicalPath
-    val base_name = file.getName
-
-    Isabelle.jedit_buffer(full_name) match {
+    Isabelle.jedit_buffer(jedit_file) match {
       case Some(buffer) =>
         view.setBuffer(buffer)
         val text_area = view.getTextArea
@@ -53,10 +48,10 @@
 
       case None =>
         val args =
-          if (line <= 0) Array(base_name)
-          else if (column <= 0) Array(base_name, "+line:" + line.toInt)
-          else Array(base_name, "+line:" + line.toInt + "," + column.toInt)
-        jEdit.openFiles(view, file.getParent, args)
+          if (line <= 0) Array(jedit_file)
+          else if (column <= 0) Array(jedit_file, "+line:" + line.toInt)
+          else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt)
+        jEdit.openFiles(view, null, args)
     }
   }
 }
diff -r 6f3ccfa7818d -r a2df77fcf1eb src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 24 19:35:44 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 24 20:41:47 2012 +0200
@@ -114,8 +114,8 @@
         {
           case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val file = Path.explode(name).file
-            Text.Info(snapshot.convert(info_range), Hyperlink(file, 0, 0)) :: links
+            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
           if (props.find(
@@ -126,23 +126,21 @@
             props match {
               case Position.Line_File(line, name) if Path.is_ok(name) =>
                 Isabelle_System.source_file(Path.explode(name)) match {
-                  case Some(file) =>
-                    Text.Info(snapshot.convert(info_range), Hyperlink(file, line, 0)) :: links
+                  case Some(path) =>
+                    val jedit_file = Isabelle_System.platform_path(path)
+                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
                   case None => links
                 }
 
               case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
                 snapshot.state.find_command(snapshot.version, id) match {
                   case Some((node, command)) =>
-                    val file = new JFile(command.node_name.node)
-
                     val sources =
                       node.commands.iterator.takeWhile(_ != command).map(_.source) ++
                         Iterator.single(command.source(Text.Range(0, command.decode(offset))))
                     val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-
-                    Text.Info(snapshot.convert(info_range), Hyperlink(file, line, column)) :: links
-
+                    Text.Info(snapshot.convert(info_range),
+                      Hyperlink(command.node_name.node, line, column)) :: links
                   case None => links
                 }