# HG changeset patch
# User wenzelm
# Date 1282499741 -7200
# Node ID 881c362d48e41bfa446c1bc32dc5ccfa322d46a2
# Parent  ce46a6f55bce6952fa50a8a0a3ccf3d18c498a95
proper range for hyperlinks and tooltips, using original markup information;

diff -r ce46a6f55bce -r 881c362d48e4 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 19:53:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 19:55:41 2010 +0200
@@ -202,17 +202,13 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          val root = Text.Info[Option[XML.Body]]((Text.Range(offset) - command_start), None)
-          snapshot.state(command).markup.select(root) {
-            case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => Some(body)
-          } match {
-            // FIXME use original node range, not restricted version
-            case Text.Info(range, Some(body)) #:: _ =>
+          val root = Text.Info[String]((Text.Range(offset) - command_start), null)
+          (snapshot.state(command).markup.select(root) {
+            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
               val typing =
                 Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
               Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
-            case _ => null
-          }
+          }).head.info
         case None => null
       }
     }
diff -r ce46a6f55bce -r 881c362d48e4 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 19:53:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 19:55:41 2010 +0200
@@ -49,10 +49,8 @@
           case Some((command, command_start)) =>
             val root = Text.Info[Hyperlink]((Text.Range(offset) - command_start), null)
             (snapshot.state(command).markup.select(root) {
-              case Text.Info(_, XML.Elem(Markup(Markup.ML_REF, _),
+              case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
                   List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
-//{{{
-                val info_range = root.range // FIXME proper range
                 val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
                 val line = buffer.getLineOfOffset(begin)
 
@@ -67,7 +65,7 @@
                             snapshot.node.command_start(ref_cmd) match {
                               case Some(ref_cmd_start) =>
                                 new Internal_Hyperlink(begin, end, line,
-                                  snapshot.convert(ref_cmd_start + ref_offset - 1)) // FIXME Command.decode_range
+                                  snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset)))
                               case None => null
                             }
                           case None => null
@@ -75,7 +73,6 @@
                       case _ => null
                     }
                 }
-//}}}
             }).head.info
           case None => null
         }