# HG changeset patch
# User wenzelm
# Date 1281906442 -7200
# Node ID 7066fbd315ae510f1976fbf788e37e3eb2b32e69
# Parent  2858ec7b6dd847e9c60ed2aff9a5bc5268a2af53
some derived operations on Text.Range;

diff -r 2858ec7b6dd8 -r 7066fbd315ae src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Aug 15 22:48:56 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Aug 15 23:07:22 2010 +0200
@@ -66,7 +66,7 @@
 
     def type_at(pos: Text.Offset): Option[String] =
     {
-      types.find(t => t.range.start <= pos && pos < t.range.stop) match {
+      types.find(_.range.contains(pos)) match {
         case Some(t) =>
           t.info match {
             case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
@@ -82,7 +82,7 @@
         case _ => false }).flatten
 
     def ref_at(pos: Text.Offset): Option[Markup_Node] =
-      refs.find(t => t.range.start <= pos && pos < t.range.stop)
+      refs.find(_.range.contains(pos))
 
 
     /* message dispatch */
diff -r 2858ec7b6dd8 -r 7066fbd315ae src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Aug 15 22:48:56 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Aug 15 23:07:22 2010 +0200
@@ -123,10 +123,12 @@
     val version: Version
     val node: Node
     val is_outdated: Boolean
-    def convert(i: Text.Offset): Text.Offset
-    def revert(i: Text.Offset): Text.Offset
     def lookup_command(id: Command_ID): Option[Command]
     def state(command: Command): Command.State
+    def convert(i: Text.Offset): Text.Offset
+    def convert(range: Text.Range): Text.Range = range.map(convert(_))
+    def revert(i: Text.Offset): Text.Offset
+    def revert(range: Text.Range): Text.Range = range.map(revert(_))
   }
 
   object History
@@ -160,14 +162,13 @@
         val version = stable.current.join
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
-
-        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
-
         def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
         def state(command: Command): Command.State =
           try { state_snapshot.command_state(version, command) }
           catch { case _: State.Fail => command.empty_state }
+
+        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
       }
     }
   }
diff -r 2858ec7b6dd8 -r 7066fbd315ae src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sun Aug 15 22:48:56 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Sun Aug 15 23:07:22 2010 +0200
@@ -15,6 +15,11 @@
   type Offset = Int
 
   sealed case class Range(val start: Offset, val stop: Offset)
+  {
+    def contains(i: Offset): Boolean = start <= i && i < stop
+    def map(f: Offset => Offset): Range = Range(f(start), f(stop))
+    def +(i: Offset): Range = map(_ + i)
+  }
 
 
   /* editing */
diff -r 2858ec7b6dd8 -r 7066fbd315ae src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 22:48:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 23:07:22 2010 +0200
@@ -280,8 +280,7 @@
         (command, command_start) <-
           snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
         markup <- snapshot.state(command).highlight.flatten
-        val abs_start = snapshot.convert(command_start + markup.range.start)
-        val abs_stop = snapshot.convert(command_start + markup.range.stop)
+        val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
         if (abs_stop > start)
         if (abs_start < stop)
         val token_start = (abs_start - start) max 0
diff -r 2858ec7b6dd8 -r 7066fbd315ae src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 22:48:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 23:07:22 2010 +0200
@@ -49,9 +49,8 @@
           case Some((command, command_start)) =>
             snapshot.state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
-                val begin = snapshot.convert(command_start + ref.range.start)
+                val Text.Range(begin, end) = snapshot.convert(ref.range + command_start)
                 val line = buffer.getLineOfOffset(begin)
-                val end = snapshot.convert(command_start + ref.range.stop)
                 ref.info match {
                   case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)