tuned;
authorwenzelm
Tue Apr 08 10:24:42 2014 +0200 (2014-04-08)
changeset 56461ae33d153f6cc
parent 56460 af28fdd50690
child 56462 b64b0cb845fe
tuned;
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 09:48:38 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 10:24:42 2014 +0200
     1.3 @@ -159,38 +159,23 @@
     1.4  
     1.5    /* hyperlinks */
     1.6  
     1.7 -  override def hyperlink_command(
     1.8 -    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
     1.9 -  {
    1.10 -    if (snapshot.is_outdated) None
    1.11 -    else {
    1.12 -      snapshot.state.find_command(snapshot.version, command.id) match {
    1.13 -        case None => None
    1.14 -        case Some((node, _)) =>
    1.15 -          val file_name = command.node_name.node
    1.16 -          val sources_iterator =
    1.17 -            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.18 -              (if (offset == 0) Iterator.empty
    1.19 -               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
    1.20 -          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    1.21 -          Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
    1.22 -      }
    1.23 +  def hyperlink_url(name: String): Hyperlink =
    1.24 +    new Hyperlink {
    1.25 +      def follow(view: View) =
    1.26 +        default_thread_pool.submit(() =>
    1.27 +          try { Isabelle_System.open(name) }
    1.28 +          catch {
    1.29 +            case exn: Throwable =>
    1.30 +              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    1.31 +          })
    1.32 +      override def toString: String = "URL " + quote(name)
    1.33      }
    1.34 -  }
    1.35 -
    1.36 -  def hyperlink_command_id(
    1.37 -    snapshot: Document.Snapshot,
    1.38 -    id: Document_ID.Generic,
    1.39 -    offset: Symbol.Offset): Option[Hyperlink] =
    1.40 -  {
    1.41 -    snapshot.state.find_command(snapshot.version, id) match {
    1.42 -      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
    1.43 -      case None => None
    1.44 -    }
    1.45 -  }
    1.46  
    1.47    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.48 -    new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
    1.49 +    new Hyperlink {
    1.50 +      def follow(view: View) = goto_file(view, name, line, column)
    1.51 +      override def toString: String = "file " + quote(name)
    1.52 +    }
    1.53  
    1.54    def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
    1.55      : Option[Hyperlink] =
    1.56 @@ -223,14 +208,33 @@
    1.57      }
    1.58    }
    1.59  
    1.60 -  def hyperlink_url(name: String): Hyperlink =
    1.61 -    new Hyperlink {
    1.62 -      def follow(view: View) =
    1.63 -        default_thread_pool.submit(() =>
    1.64 -          try { Isabelle_System.open(name) }
    1.65 -          catch {
    1.66 -            case exn: Throwable =>
    1.67 -              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    1.68 -          })
    1.69 +  override def hyperlink_command(
    1.70 +    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
    1.71 +  {
    1.72 +    if (snapshot.is_outdated) None
    1.73 +    else {
    1.74 +      snapshot.state.find_command(snapshot.version, command.id) match {
    1.75 +        case None => None
    1.76 +        case Some((node, _)) =>
    1.77 +          val file_name = command.node_name.node
    1.78 +          val sources_iterator =
    1.79 +            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.80 +              (if (offset == 0) Iterator.empty
    1.81 +               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
    1.82 +          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    1.83 +          Some(hyperlink_file(file_name, line, column))
    1.84 +      }
    1.85      }
    1.86 +  }
    1.87 +
    1.88 +  def hyperlink_command_id(
    1.89 +    snapshot: Document.Snapshot,
    1.90 +    id: Document_ID.Generic,
    1.91 +    offset: Symbol.Offset): Option[Hyperlink] =
    1.92 +  {
    1.93 +    snapshot.state.find_command(snapshot.version, id) match {
    1.94 +      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
    1.95 +      case None => None
    1.96 +    }
    1.97 +  }
    1.98  }