--- 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)
--- 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))
}
}
--- 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)
}
}
}
--- 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
}