some derived operations on Text.Range;
authorwenzelm
Sun Aug 15 23:07:22 2010 +0200 (2010-08-15)
changeset 384277066fbd315ae
parent 38426 2858ec7b6dd8
child 38428 c13c95c97e89
some derived operations on Text.Range;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 15 22:48:56 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 15 23:07:22 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5      def type_at(pos: Text.Offset): Option[String] =
     1.6      {
     1.7 -      types.find(t => t.range.start <= pos && pos < t.range.stop) match {
     1.8 +      types.find(_.range.contains(pos)) match {
     1.9          case Some(t) =>
    1.10            t.info match {
    1.11              case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    1.12 @@ -82,7 +82,7 @@
    1.13          case _ => false }).flatten
    1.14  
    1.15      def ref_at(pos: Text.Offset): Option[Markup_Node] =
    1.16 -      refs.find(t => t.range.start <= pos && pos < t.range.stop)
    1.17 +      refs.find(_.range.contains(pos))
    1.18  
    1.19  
    1.20      /* message dispatch */
     2.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 15 22:48:56 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 15 23:07:22 2010 +0200
     2.3 @@ -123,10 +123,12 @@
     2.4      val version: Version
     2.5      val node: Node
     2.6      val is_outdated: Boolean
     2.7 -    def convert(i: Text.Offset): Text.Offset
     2.8 -    def revert(i: Text.Offset): Text.Offset
     2.9      def lookup_command(id: Command_ID): Option[Command]
    2.10      def state(command: Command): Command.State
    2.11 +    def convert(i: Text.Offset): Text.Offset
    2.12 +    def convert(range: Text.Range): Text.Range = range.map(convert(_))
    2.13 +    def revert(i: Text.Offset): Text.Offset
    2.14 +    def revert(range: Text.Range): Text.Range = range.map(revert(_))
    2.15    }
    2.16  
    2.17    object History
    2.18 @@ -160,14 +162,13 @@
    2.19          val version = stable.current.join
    2.20          val node = version.nodes(name)
    2.21          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    2.22 -
    2.23 -        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    2.24 -        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.25 -
    2.26          def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
    2.27          def state(command: Command): Command.State =
    2.28            try { state_snapshot.command_state(version, command) }
    2.29            catch { case _: State.Fail => command.empty_state }
    2.30 +
    2.31 +        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    2.32 +        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.33        }
    2.34      }
    2.35    }
     3.1 --- a/src/Pure/PIDE/text.scala	Sun Aug 15 22:48:56 2010 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 15 23:07:22 2010 +0200
     3.3 @@ -15,6 +15,11 @@
     3.4    type Offset = Int
     3.5  
     3.6    sealed case class Range(val start: Offset, val stop: Offset)
     3.7 +  {
     3.8 +    def contains(i: Offset): Boolean = start <= i && i < stop
     3.9 +    def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    3.10 +    def +(i: Offset): Range = map(_ + i)
    3.11 +  }
    3.12  
    3.13  
    3.14    /* editing */
     4.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 22:48:56 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 23:07:22 2010 +0200
     4.3 @@ -280,8 +280,7 @@
     4.4          (command, command_start) <-
     4.5            snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
     4.6          markup <- snapshot.state(command).highlight.flatten
     4.7 -        val abs_start = snapshot.convert(command_start + markup.range.start)
     4.8 -        val abs_stop = snapshot.convert(command_start + markup.range.stop)
     4.9 +        val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
    4.10          if (abs_stop > start)
    4.11          if (abs_start < stop)
    4.12          val token_start = (abs_start - start) max 0
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 22:48:56 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 23:07:22 2010 +0200
     5.3 @@ -49,9 +49,8 @@
     5.4            case Some((command, command_start)) =>
     5.5              snapshot.state(command).ref_at(offset - command_start) match {
     5.6                case Some(ref) =>
     5.7 -                val begin = snapshot.convert(command_start + ref.range.start)
     5.8 +                val Text.Range(begin, end) = snapshot.convert(ref.range + command_start)
     5.9                  val line = buffer.getLineOfOffset(begin)
    5.10 -                val end = snapshot.convert(command_start + ref.range.stop)
    5.11                  ref.info match {
    5.12                    case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    5.13                      new External_Hyperlink(begin, end, line, ref_file, ref_line)