support hyperlinks with optional focus change;
authorwenzelm
Tue Aug 11 17:00:16 2015 +0200 (2015-08-11)
changeset 608933c8b9b4b577c
parent 60892 cc7a1285693f
child 60894 bd743ec40334
support hyperlinks with optional focus change;
no change of focus for debuffer position, to avoid visual glitches and keep panel active;
src/Pure/PIDE/editor.scala
src/Pure/PIDE/query_operation.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/debugger_dockable.scala
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/Pure/PIDE/editor.scala	Tue Aug 11 15:24:49 2015 +0200
     1.2 +++ b/src/Pure/PIDE/editor.scala	Tue Aug 11 17:00:16 2015 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4      def follow(context: Context): Unit
     1.5    }
     1.6    def hyperlink_command(
     1.7 -    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
     1.8 +    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
     1.9 +      : Option[Hyperlink]
    1.10  }
    1.11  
     2.1 --- a/src/Pure/PIDE/query_operation.scala	Tue Aug 11 15:24:49 2015 +0200
     2.2 +++ b/src/Pure/PIDE/query_operation.scala	Tue Aug 11 17:00:16 2015 +0200
     2.3 @@ -201,7 +201,7 @@
     2.4      for {
     2.5        command <- current_location
     2.6        snapshot = editor.node_snapshot(command.node_name)
     2.7 -      link <- editor.hyperlink_command(snapshot, command)
     2.8 +      link <- editor.hyperlink_command(true, snapshot, command)
     2.9      } link.follow(editor_context)
    2.10    }
    2.11  
     3.1 --- a/src/Tools/jEdit/src/active.scala	Tue Aug 11 15:24:49 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Aug 11 17:00:16 2015 +0200
     3.3 @@ -48,7 +48,7 @@
     3.4                case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
     3.5                  val link =
     3.6                    props match {
     3.7 -                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(snapshot, id)
     3.8 +                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(true, snapshot, id)
     3.9                      case _ => None
    3.10                    }
    3.11                  GUI_Thread.later {
     4.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
     4.3 @@ -321,7 +321,7 @@
     4.4    private def update_focus(focus: Option[Position.T])
     4.5    {
     4.6      if (Debugger.focus(focus) && focus.isDefined)
     4.7 -      PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view))
     4.8 +      PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view))
     4.9    }
    4.10  
    4.11  
     5.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
     5.3 @@ -54,10 +54,10 @@
     5.4    {
     5.5      node.getUserObject match {
     5.6        case Text_File(_, path) =>
     5.7 -        PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
     5.8 +        PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
     5.9        case Documentation(_, _, path) =>
    5.10          if (path.is_file)
    5.11 -          PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    5.12 +          PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
    5.13          else {
    5.14            Future.fork {
    5.15              try { Doc.view(path) }
     6.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Aug 11 15:24:49 2015 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Aug 11 17:00:16 2015 +0200
     6.3 @@ -133,13 +133,13 @@
     6.4      }
     6.5    }
     6.6  
     6.7 -  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
     6.8 +  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
     6.9    {
    6.10      GUI_Thread.require {}
    6.11  
    6.12      push_position(view)
    6.13  
    6.14 -    view.goToBuffer(buffer)
    6.15 +    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
    6.16      try { view.getTextArea.moveCaretPosition(offset) }
    6.17      catch {
    6.18        case _: ArrayIndexOutOfBoundsException =>
    6.19 @@ -147,7 +147,7 @@
    6.20      }
    6.21    }
    6.22  
    6.23 -  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    6.24 +  def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
    6.25    {
    6.26      GUI_Thread.require {}
    6.27  
    6.28 @@ -155,7 +155,7 @@
    6.29  
    6.30      JEdit_Lib.jedit_buffer(name) match {
    6.31        case Some(buffer) =>
    6.32 -        view.goToBuffer(buffer)
    6.33 +        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
    6.34          val text_area = view.getTextArea
    6.35  
    6.36          try {
    6.37 @@ -197,21 +197,21 @@
    6.38        override def toString: String = "URL " + quote(name)
    6.39      }
    6.40  
    6.41 -  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
    6.42 +  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
    6.43      new Hyperlink {
    6.44        val external = false
    6.45 -      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
    6.46 +      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
    6.47        override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
    6.48      }
    6.49  
    6.50 -  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    6.51 +  def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
    6.52      new Hyperlink {
    6.53        val external = false
    6.54 -      def follow(view: View): Unit = goto_file(view, name, line, column)
    6.55 +      def follow(view: View): Unit = goto_file(focus, view, name, line, column)
    6.56        override def toString: String = "file " + quote(name)
    6.57      }
    6.58  
    6.59 -  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
    6.60 +  def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
    6.61      : Option[Hyperlink] =
    6.62    {
    6.63      val opt_name =
    6.64 @@ -235,15 +235,16 @@
    6.65                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    6.66                        Symbol.advance_line_column)
    6.67                }
    6.68 -            Some(hyperlink_file(name, line, column))
    6.69 -          case _ => Some(hyperlink_file(name, line))
    6.70 +            Some(hyperlink_file(focus, name, line, column))
    6.71 +          case _ => Some(hyperlink_file(focus, name, line))
    6.72          }
    6.73        case None => None
    6.74      }
    6.75    }
    6.76  
    6.77    override def hyperlink_command(
    6.78 -    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
    6.79 +    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
    6.80 +      : Option[Hyperlink] =
    6.81    {
    6.82      if (snapshot.is_outdated) None
    6.83      else {
    6.84 @@ -256,39 +257,40 @@
    6.85                (if (offset == 0) Iterator.empty
    6.86                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
    6.87            val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    6.88 -          Some(hyperlink_file(file_name, line, column))
    6.89 +          Some(hyperlink_file(focus, file_name, line, column))
    6.90        }
    6.91      }
    6.92    }
    6.93  
    6.94    def hyperlink_command_id(
    6.95 -    snapshot: Document.Snapshot,
    6.96 -    id: Document_ID.Generic,
    6.97 -    offset: Symbol.Offset = 0): Option[Hyperlink] =
    6.98 +    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
    6.99 +      : Option[Hyperlink] =
   6.100    {
   6.101      snapshot.state.find_command(snapshot.version, id) match {
   6.102 -      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
   6.103 +      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
   6.104        case None => None
   6.105      }
   6.106    }
   6.107  
   6.108 -  def hyperlink_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
   6.109 +  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
   6.110 +      : Option[Hyperlink] =
   6.111      pos match {
   6.112        case Position.Line_File(line, name) =>
   6.113          val offset = Position.Offset.unapply(pos) getOrElse 0
   6.114 -        hyperlink_source_file(name, line, offset)
   6.115 +        hyperlink_source_file(focus, name, line, offset)
   6.116        case Position.Id_Offset0(id, offset) =>
   6.117 -        hyperlink_command_id(snapshot, id, offset)
   6.118 +        hyperlink_command_id(focus, snapshot, id, offset)
   6.119        case _ => None
   6.120      }
   6.121  
   6.122 -  def hyperlink_def_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
   6.123 +  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
   6.124 +      : Option[Hyperlink] =
   6.125      pos match {
   6.126        case Position.Def_Line_File(line, name) =>
   6.127          val offset = Position.Def_Offset.unapply(pos) getOrElse 0
   6.128 -        hyperlink_source_file(name, line, offset)
   6.129 +        hyperlink_source_file(focus, name, line, offset)
   6.130        case Position.Def_Id_Offset0(id, offset) =>
   6.131 -        hyperlink_command_id(snapshot, id, offset)
   6.132 +        hyperlink_command_id(focus, snapshot, id, offset)
   6.133        case _ => None
   6.134      }
   6.135  }
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Aug 11 15:24:49 2015 +0200
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Aug 11 17:00:16 2015 +0200
     7.3 @@ -406,7 +406,7 @@
     7.4        range, Vector.empty, Rendering.hyperlink_elements, _ =>
     7.5          {
     7.6            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
     7.7 -            val link = PIDE.editor.hyperlink_file(jedit_file(name))
     7.8 +            val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
     7.9              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    7.10  
    7.11            case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    7.12 @@ -418,18 +418,18 @@
    7.13              { case (Markup.KIND, Markup.ML_OPEN) => true
    7.14                case (Markup.KIND, Markup.ML_STRUCTURE) => true
    7.15                case _ => false }) =>
    7.16 -            val opt_link = PIDE.editor.hyperlink_def_position(snapshot, props)
    7.17 +            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
    7.18              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    7.19  
    7.20            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    7.21 -            val opt_link = PIDE.editor.hyperlink_position(snapshot, props)
    7.22 +            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
    7.23              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    7.24  
    7.25            case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
    7.26              val opt_link =
    7.27                Bibtex_JEdit.entries_iterator.collectFirst(
    7.28                  { case (a, buffer, offset) if a == name =>
    7.29 -                    PIDE.editor.hyperlink_buffer(buffer, offset) })
    7.30 +                    PIDE.editor.hyperlink_buffer(true, buffer, offset) })
    7.31              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    7.32  
    7.33            case _ => None
     8.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
     8.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
     8.3 @@ -45,7 +45,7 @@
     8.4                } model.node_required = !model.node_required
     8.5              }
     8.6            }
     8.7 -          else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node)
     8.8 +          else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
     8.9          }
    8.10        case MouseMoved(_, point, _) =>
    8.11          val index = peer.locationToIndex(point)
     9.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
     9.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
     9.3 @@ -88,7 +88,7 @@
     9.4    {
     9.5      def print: String =
     9.6        Time.print_seconds(timing) + "s theory " + quote(name.theory)
     9.7 -    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
     9.8 +    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
     9.9    }
    9.10  
    9.11    private case class Command_Entry(command: Command, timing: Double) extends Entry
    9.12 @@ -96,7 +96,7 @@
    9.13      def print: String =
    9.14        "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
    9.15      def follow(snapshot: Document.Snapshot)
    9.16 -    { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
    9.17 +    { PIDE.editor.hyperlink_command(true, snapshot, command).foreach(_.follow(view)) }
    9.18    }
    9.19  
    9.20