tuned signature;
authorwenzelm
Mon Mar 03 10:59:33 2014 +0100 (2014-03-03)
changeset 5587765c9968286d5
parent 55876 142139457653
child 55878 6d092a5166f1
tuned signature;
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Mar 03 10:41:58 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Mar 03 10:59:33 2014 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4                          "Documentation error", GUI.scrollable_text(Exn.message(exn)))
     1.5                    })
     1.6                case Text_File(_, path) =>
     1.7 -                PIDE.editor.goto(view, Isabelle_System.platform_path(path))
     1.8 +                PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
     1.9                case _ =>
    1.10              }
    1.11            case _ =>
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:41:58 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:59:33 2014 +0100
     2.3 @@ -109,9 +109,9 @@
     2.4      synchronized { overlays = overlays.remove(command, fn, args) }
     2.5  
     2.6  
     2.7 -  /* hyperlinks */
     2.8 +  /* navigation */
     2.9  
    2.10 -  def goto(view: View, name: String, line: Int = 0, column: Int = 0)
    2.11 +  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    2.12    {
    2.13      Swing_Thread.require()
    2.14  
    2.15 @@ -142,6 +142,9 @@
    2.16      }
    2.17    }
    2.18  
    2.19 +
    2.20 +  /* hyperlinks */
    2.21 +
    2.22    override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
    2.23      : Option[Hyperlink] =
    2.24    {
    2.25 @@ -156,7 +159,7 @@
    2.26                (if (raw_offset == 0) Iterator.empty
    2.27                 else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
    2.28            val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    2.29 -          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
    2.30 +          Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
    2.31        }
    2.32      }
    2.33    }
    2.34 @@ -173,7 +176,7 @@
    2.35    }
    2.36  
    2.37    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    2.38 -    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
    2.39 +    new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
    2.40  
    2.41    def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] =
    2.42      if (Path.is_ok(name))
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:41:58 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:59:33 2014 +0100
     3.3 @@ -327,6 +327,15 @@
     3.4  
     3.5    /* hyperlinks */
     3.6  
     3.7 +  private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
     3.8 +    props match {
     3.9 +      case Position.Def_Line_File(line, name) =>
    3.10 +        PIDE.editor.hyperlink_source_file(name, line)
    3.11 +      case Position.Def_Id_Offset(id, offset) =>
    3.12 +        PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    3.13 +      case _ => None
    3.14 +    }
    3.15 +
    3.16    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    3.17    {
    3.18      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    3.19 @@ -347,27 +356,12 @@
    3.20              { case (Markup.KIND, Markup.ML_OPEN) => true
    3.21                case (Markup.KIND, Markup.ML_STRUCTURE) => true
    3.22                case _ => false }) =>
    3.23 -
    3.24 -            val opt_link =
    3.25 -              props match {
    3.26 -                case Position.Def_Line_File(line, name) =>
    3.27 -                  PIDE.editor.hyperlink_source_file(name, line)
    3.28 -                case Position.Def_Id_Offset(id, offset) =>
    3.29 -                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    3.30 -                case _ => None
    3.31 -              }
    3.32 -            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    3.33 +            hyperlink_file(props).map(link =>
    3.34 +              (links :+ Text.Info(snapshot.convert(info_range), link)))
    3.35  
    3.36            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    3.37 -            val opt_link =
    3.38 -              props match {
    3.39 -                case Position.Line_File(line, name) =>
    3.40 -                  PIDE.editor.hyperlink_source_file(name, line)
    3.41 -                case Position.Id_Offset(id, offset) =>
    3.42 -                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    3.43 -                case _ => None
    3.44 -              }
    3.45 -            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
    3.46 +            hyperlink_file(props).map(link =>
    3.47 +              (links :+ Text.Info(snapshot.convert(info_range), link)))
    3.48  
    3.49            case _ => None
    3.50          }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
     4.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 03 10:41:58 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 03 10:59:33 2014 +0100
     4.3 @@ -40,7 +40,7 @@
     4.4                } model.node_required = !model.node_required
     4.5              }
     4.6            }
     4.7 -          else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
     4.8 +          else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node)
     4.9          }
    4.10        case MouseMoved(_, point, _) =>
    4.11          val index = peer.locationToIndex(point)
     5.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Mar 03 10:41:58 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Mar 03 10:59:33 2014 +0100
     5.3 @@ -88,7 +88,7 @@
     5.4      extends Entry
     5.5    {
     5.6      def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
     5.7 -    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
     5.8 +    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
     5.9    }
    5.10  
    5.11    private case class Command_Entry(command: Command, timing: Double) extends Entry