tuned signature;
authorwenzelm
Mon Mar 03 10:41:58 2014 +0100 (2014-03-03)
changeset 55876142139457653
parent 55850 7f229b0212fe
child 55877 65c9968286d5
tuned signature;
src/Pure/PIDE/editor.scala
src/Pure/System/isabelle_system.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/editor.scala	Mon Mar 03 03:13:45 2014 +0100
     1.2 +++ b/src/Pure/PIDE/editor.scala	Mon Mar 03 10:41:58 2014 +0100
     1.3 @@ -23,9 +23,7 @@
     1.4    def remove_overlay(command: Command, fn: String, args: List[String]): Unit
     1.5  
     1.6    abstract class Hyperlink { def follow(context: Context): Unit }
     1.7 -  def hyperlink_url(name: String): Hyperlink
     1.8 -  def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
     1.9    def hyperlink_command(
    1.10 -    snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
    1.11 +    snapshot: Document.Snapshot, command: Command, raw_offset: Text.Offset = 0): Option[Hyperlink]
    1.12  }
    1.13  
     2.1 --- a/src/Pure/System/isabelle_system.scala	Mon Mar 03 03:13:45 2014 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Mar 03 10:41:58 2014 +0100
     2.3 @@ -212,7 +212,8 @@
     2.4      if (path.is_absolute || path.is_current) check(path)
     2.5      else {
     2.6        check(Path.explode("~~/src/Pure") + path) orElse
     2.7 -        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
     2.8 +        (if (getenv("ML_SOURCES") == "") None
     2.9 +         else check(Path.explode("$ML_SOURCES") + path))
    2.10      }
    2.11    }
    2.12  
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 03:13:45 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:41:58 2014 +0100
     3.3 @@ -142,20 +142,6 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  override def hyperlink_url(name: String): Hyperlink =
     3.8 -    new Hyperlink {
     3.9 -      def follow(view: View) =
    3.10 -        default_thread_pool.submit(() =>
    3.11 -          try { Isabelle_System.open(name) }
    3.12 -          catch {
    3.13 -            case exn: Throwable =>
    3.14 -              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    3.15 -          })
    3.16 -    }
    3.17 -
    3.18 -  override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    3.19 -    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
    3.20 -
    3.21    override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
    3.22      : Option[Hyperlink] =
    3.23    {
    3.24 @@ -174,4 +160,35 @@
    3.25        }
    3.26      }
    3.27    }
    3.28 +
    3.29 +  def hyperlink_command_id(
    3.30 +    snapshot: Document.Snapshot,
    3.31 +    id: Document_ID.Generic,
    3.32 +    raw_offset: Text.Offset): Option[Hyperlink] =
    3.33 +  {
    3.34 +    snapshot.state.find_command(snapshot.version, id) match {
    3.35 +      case Some((node, command)) => hyperlink_command(snapshot, command, raw_offset)
    3.36 +      case None => None
    3.37 +    }
    3.38 +  }
    3.39 +
    3.40 +  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    3.41 +    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
    3.42 +
    3.43 +  def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] =
    3.44 +    if (Path.is_ok(name))
    3.45 +      Isabelle_System.source_file(Path.explode(name)).map(path =>
    3.46 +        hyperlink_file(Isabelle_System.platform_path(path), line))
    3.47 +    else None
    3.48 +
    3.49 +  def hyperlink_url(name: String): Hyperlink =
    3.50 +    new Hyperlink {
    3.51 +      def follow(view: View) =
    3.52 +        default_thread_pool.submit(() =>
    3.53 +          try { Isabelle_System.open(name) }
    3.54 +          catch {
    3.55 +            case exn: Throwable =>
    3.56 +              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    3.57 +          })
    3.58 +    }
    3.59  }
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 03:13:45 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:41:58 2014 +0100
     4.3 @@ -327,20 +327,6 @@
     4.4  
     4.5    /* hyperlinks */
     4.6  
     4.7 -  private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
     4.8 -    if (Path.is_ok(name))
     4.9 -      Isabelle_System.source_file(Path.explode(name)).map(path =>
    4.10 -        PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
    4.11 -    else None
    4.12 -
    4.13 -  private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
    4.14 -      : Option[PIDE.editor.Hyperlink] =
    4.15 -    snapshot.state.find_command(snapshot.version, id) match {
    4.16 -      case Some((node, command)) =>
    4.17 -        PIDE.editor.hyperlink_command(snapshot, command, offset)
    4.18 -      case None => None
    4.19 -    }
    4.20 -
    4.21    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    4.22    {
    4.23      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    4.24 @@ -364,8 +350,10 @@
    4.25  
    4.26              val opt_link =
    4.27                props match {
    4.28 -                case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
    4.29 -                case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
    4.30 +                case Position.Def_Line_File(line, name) =>
    4.31 +                  PIDE.editor.hyperlink_source_file(name, line)
    4.32 +                case Position.Def_Id_Offset(id, offset) =>
    4.33 +                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    4.34                  case _ => None
    4.35                }
    4.36              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    4.37 @@ -373,8 +361,10 @@
    4.38            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    4.39              val opt_link =
    4.40                props match {
    4.41 -                case Position.Line_File(line, name) => hyperlink_file(line, name)
    4.42 -                case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
    4.43 +                case Position.Line_File(line, name) =>
    4.44 +                  PIDE.editor.hyperlink_source_file(name, line)
    4.45 +                case Position.Id_Offset(id, offset) =>
    4.46 +                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    4.47                  case _ => None
    4.48                }
    4.49              opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))