src/Tools/jEdit/src/jedit_editor.scala
changeset 60893 3c8b9b4b577c
parent 60874 7865e03a7fc1
child 60933 6d03e05ef041
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Aug 11 15:24:49 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Aug 11 17:00:16 2015 +0200
     1.3 @@ -133,13 +133,13 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
     1.8 +  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
     1.9    {
    1.10      GUI_Thread.require {}
    1.11  
    1.12      push_position(view)
    1.13  
    1.14 -    view.goToBuffer(buffer)
    1.15 +    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
    1.16      try { view.getTextArea.moveCaretPosition(offset) }
    1.17      catch {
    1.18        case _: ArrayIndexOutOfBoundsException =>
    1.19 @@ -147,7 +147,7 @@
    1.20      }
    1.21    }
    1.22  
    1.23 -  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    1.24 +  def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
    1.25    {
    1.26      GUI_Thread.require {}
    1.27  
    1.28 @@ -155,7 +155,7 @@
    1.29  
    1.30      JEdit_Lib.jedit_buffer(name) match {
    1.31        case Some(buffer) =>
    1.32 -        view.goToBuffer(buffer)
    1.33 +        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
    1.34          val text_area = view.getTextArea
    1.35  
    1.36          try {
    1.37 @@ -197,21 +197,21 @@
    1.38        override def toString: String = "URL " + quote(name)
    1.39      }
    1.40  
    1.41 -  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
    1.42 +  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
    1.43      new Hyperlink {
    1.44        val external = false
    1.45 -      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
    1.46 +      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
    1.47        override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
    1.48      }
    1.49  
    1.50 -  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.51 +  def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.52      new Hyperlink {
    1.53        val external = false
    1.54 -      def follow(view: View): Unit = goto_file(view, name, line, column)
    1.55 +      def follow(view: View): Unit = goto_file(focus, view, name, line, column)
    1.56        override def toString: String = "file " + quote(name)
    1.57      }
    1.58  
    1.59 -  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
    1.60 +  def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
    1.61      : Option[Hyperlink] =
    1.62    {
    1.63      val opt_name =
    1.64 @@ -235,15 +235,16 @@
    1.65                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    1.66                        Symbol.advance_line_column)
    1.67                }
    1.68 -            Some(hyperlink_file(name, line, column))
    1.69 -          case _ => Some(hyperlink_file(name, line))
    1.70 +            Some(hyperlink_file(focus, name, line, column))
    1.71 +          case _ => Some(hyperlink_file(focus, name, line))
    1.72          }
    1.73        case None => None
    1.74      }
    1.75    }
    1.76  
    1.77    override def hyperlink_command(
    1.78 -    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
    1.79 +    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
    1.80 +      : Option[Hyperlink] =
    1.81    {
    1.82      if (snapshot.is_outdated) None
    1.83      else {
    1.84 @@ -256,39 +257,40 @@
    1.85                (if (offset == 0) Iterator.empty
    1.86                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
    1.87            val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    1.88 -          Some(hyperlink_file(file_name, line, column))
    1.89 +          Some(hyperlink_file(focus, file_name, line, column))
    1.90        }
    1.91      }
    1.92    }
    1.93  
    1.94    def hyperlink_command_id(
    1.95 -    snapshot: Document.Snapshot,
    1.96 -    id: Document_ID.Generic,
    1.97 -    offset: Symbol.Offset = 0): Option[Hyperlink] =
    1.98 +    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
    1.99 +      : Option[Hyperlink] =
   1.100    {
   1.101      snapshot.state.find_command(snapshot.version, id) match {
   1.102 -      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
   1.103 +      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
   1.104        case None => None
   1.105      }
   1.106    }
   1.107  
   1.108 -  def hyperlink_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
   1.109 +  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
   1.110 +      : Option[Hyperlink] =
   1.111      pos match {
   1.112        case Position.Line_File(line, name) =>
   1.113          val offset = Position.Offset.unapply(pos) getOrElse 0
   1.114 -        hyperlink_source_file(name, line, offset)
   1.115 +        hyperlink_source_file(focus, name, line, offset)
   1.116        case Position.Id_Offset0(id, offset) =>
   1.117 -        hyperlink_command_id(snapshot, id, offset)
   1.118 +        hyperlink_command_id(focus, snapshot, id, offset)
   1.119        case _ => None
   1.120      }
   1.121  
   1.122 -  def hyperlink_def_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
   1.123 +  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
   1.124 +      : Option[Hyperlink] =
   1.125      pos match {
   1.126        case Position.Def_Line_File(line, name) =>
   1.127          val offset = Position.Def_Offset.unapply(pos) getOrElse 0
   1.128 -        hyperlink_source_file(name, line, offset)
   1.129 +        hyperlink_source_file(focus, name, line, offset)
   1.130        case Position.Def_Id_Offset0(id, offset) =>
   1.131 -        hyperlink_command_id(snapshot, id, offset)
   1.132 +        hyperlink_command_id(focus, snapshot, id, offset)
   1.133        case _ => None
   1.134      }
   1.135  }