# HG changeset patch
# User wenzelm
# Date 1282743674 -7200
# Node ID c1ff9234c49cbf25d9f75ddbc878613d171207aa
# Parent  04414091f3b54fcd8deb15a0eb259921db985425
select tangible text ranges here -- more robust against ongoing changes of the markup query model

diff -r 04414091f3b5 -r c1ff9234c49c src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed Aug 25 15:12:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Aug 25 15:41:14 2010 +0200
@@ -199,7 +199,7 @@
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
           // FIXME Isar_Document.Tooltip extractor
-          (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+          (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
             case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
               val typing =
                 Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
diff -r 04414091f3b5 -r c1ff9234c49c src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 25 15:12:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 25 15:41:14 2010 +0200
@@ -49,7 +49,7 @@
         snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
             // FIXME Isar_Document.Hyperlink extractor
-            (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+            (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
               case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
                   List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
                 val Text.Range(begin, end) = snapshot.convert(info_range + command_start)