clarified modules;
authorwenzelm
Thu Dec 22 11:38:16 2016 +0100 (2016-12-22)
changeset 646576209e0f7a4e8
parent 64656 65c8a7780538
child 64658 fb42c780d903
clarified modules;
src/Pure/PIDE/resources.scala
src/Pure/System/isabelle_system.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Dec 22 11:20:59 2016 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Dec 22 11:38:16 2016 +0100
     1.3 @@ -53,6 +53,30 @@
     1.4  
     1.5  
     1.6  
     1.7 +  /* source files of Isabelle/ML bootstrap */
     1.8 +
     1.9 +  def source_file(raw_name: String): Option[String] =
    1.10 +  {
    1.11 +    if (Path.is_wellformed(raw_name)) {
    1.12 +      if (Path.is_valid(raw_name)) {
    1.13 +        def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
    1.14 +
    1.15 +        val path = Path.explode(raw_name)
    1.16 +        val path1 =
    1.17 +          if (path.is_absolute || path.is_current) check(path)
    1.18 +          else {
    1.19 +            check(Path.explode("~~/src/Pure") + path) orElse
    1.20 +              (if (Isabelle_System.getenv("ML_SOURCES") == "") None
    1.21 +               else check(Path.explode("$ML_SOURCES") + path))
    1.22 +          }
    1.23 +        Some(File.platform_path(path1 getOrElse path))
    1.24 +      }
    1.25 +      else None
    1.26 +    }
    1.27 +    else Some(raw_name)
    1.28 +  }
    1.29 +
    1.30 +
    1.31    /* theory files */
    1.32  
    1.33    def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
     2.1 --- a/src/Pure/System/isabelle_system.scala	Thu Dec 22 11:20:59 2016 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Dec 22 11:38:16 2016 +0100
     2.3 @@ -161,21 +161,6 @@
     2.4  
     2.5    /** file-system operations **/
     2.6  
     2.7 -  /* source files of Isabelle/ML bootstrap */
     2.8 -
     2.9 -  def source_file(path: Path): Option[Path] =
    2.10 -  {
    2.11 -    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
    2.12 -
    2.13 -    if (path.is_absolute || path.is_current) check(path)
    2.14 -    else {
    2.15 -      check(Path.explode("~~/src/Pure") + path) orElse
    2.16 -        (if (getenv("ML_SOURCES") == "") None
    2.17 -         else check(Path.explode("$ML_SOURCES") + path))
    2.18 -    }
    2.19 -  }
    2.20 -
    2.21 -
    2.22    /* directories */
    2.23  
    2.24    def mkdirs(path: Path): Unit =
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Dec 22 11:20:59 2016 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Dec 22 11:38:16 2016 +0100
     3.3 @@ -265,31 +265,19 @@
     3.4    def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
     3.5      : Option[Hyperlink] =
     3.6    {
     3.7 -    val opt_name =
     3.8 -      if (Path.is_wellformed(source_name)) {
     3.9 -        if (Path.is_valid(source_name)) {
    3.10 -          val path = Path.explode(source_name)
    3.11 -          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
    3.12 -        }
    3.13 -        else None
    3.14 +    for (name <- PIDE.resources.source_file(source_name)) yield {
    3.15 +      JEdit_Lib.jedit_buffer(name) match {
    3.16 +        case Some(buffer) if offset > 0 =>
    3.17 +          val pos =
    3.18 +            JEdit_Lib.buffer_lock(buffer) {
    3.19 +              (Line.Position.zero /:
    3.20 +                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    3.21 +                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
    3.22 +            }
    3.23 +          hyperlink_file(focus, Line.Node_Position(name, pos))
    3.24 +        case _ =>
    3.25 +          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
    3.26        }
    3.27 -      else Some(source_name)
    3.28 -
    3.29 -    opt_name match {
    3.30 -      case Some(name) =>
    3.31 -        JEdit_Lib.jedit_buffer(name) match {
    3.32 -          case Some(buffer) if offset > 0 =>
    3.33 -            val pos =
    3.34 -              JEdit_Lib.buffer_lock(buffer) {
    3.35 -                (Line.Position.zero /:
    3.36 -                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    3.37 -                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
    3.38 -              }
    3.39 -            Some(hyperlink_file(focus, Line.Node_Position(name, pos)))
    3.40 -          case _ =>
    3.41 -            Some(hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0))))
    3.42 -        }
    3.43 -      case None => None
    3.44      }
    3.45    }
    3.46