--- a/src/Pure/PIDE/resources.scala Thu Dec 22 11:20:59 2016 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Dec 22 11:38:16 2016 +0100
@@ -53,6 +53,30 @@
+ /* source files of Isabelle/ML bootstrap */
+
+ def source_file(raw_name: String): Option[String] =
+ {
+ if (Path.is_wellformed(raw_name)) {
+ if (Path.is_valid(raw_name)) {
+ def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
+
+ val path = Path.explode(raw_name)
+ val path1 =
+ if (path.is_absolute || path.is_current) check(path)
+ else {
+ check(Path.explode("~~/src/Pure") + path) orElse
+ (if (Isabelle_System.getenv("ML_SOURCES") == "") None
+ else check(Path.explode("$ML_SOURCES") + path))
+ }
+ Some(File.platform_path(path1 getOrElse path))
+ }
+ else None
+ }
+ else Some(raw_name)
+ }
+
+
/* theory files */
def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
--- a/src/Pure/System/isabelle_system.scala Thu Dec 22 11:20:59 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Dec 22 11:38:16 2016 +0100
@@ -161,21 +161,6 @@
/** file-system operations **/
- /* source files of Isabelle/ML bootstrap */
-
- def source_file(path: Path): Option[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 {
- check(Path.explode("~~/src/Pure") + path) orElse
- (if (getenv("ML_SOURCES") == "") None
- else check(Path.explode("$ML_SOURCES") + path))
- }
- }
-
-
/* directories */
def mkdirs(path: Path): Unit =
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Dec 22 11:20:59 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Dec 22 11:38:16 2016 +0100
@@ -265,31 +265,19 @@
def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
: Option[Hyperlink] =
{
- val opt_name =
- if (Path.is_wellformed(source_name)) {
- if (Path.is_valid(source_name)) {
- val path = Path.explode(source_name)
- Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
- }
- else None
+ for (name <- PIDE.resources.source_file(source_name)) yield {
+ JEdit_Lib.jedit_buffer(name) match {
+ case Some(buffer) if offset > 0 =>
+ val pos =
+ JEdit_Lib.buffer_lock(buffer) {
+ (Line.Position.zero /:
+ (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+ zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
+ }
+ hyperlink_file(focus, Line.Node_Position(name, pos))
+ case _ =>
+ hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
}
- else Some(source_name)
-
- opt_name match {
- case Some(name) =>
- JEdit_Lib.jedit_buffer(name) match {
- case Some(buffer) if offset > 0 =>
- val pos =
- JEdit_Lib.buffer_lock(buffer) {
- (Line.Position.zero /:
- (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
- zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
- }
- Some(hyperlink_file(focus, Line.Node_Position(name, pos)))
- case _ =>
- Some(hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0))))
- }
- case None => None
}
}