# HG changeset patch
# User wenzelm
# Date 1282677721 -7200
# Node ID 049fdf15144fb214f60a02e30bdbd27569a68525
# Parent  afac51977705e25b49886938a790a156d345bcd3
tuned;

diff -r afac51977705 -r 049fdf15144f src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 24 21:20:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 24 21:22:01 2010 +0200
@@ -198,6 +198,7 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       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) {
             case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
               val typing =
diff -r afac51977705 -r 049fdf15144f src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Aug 24 21:20:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Aug 24 21:22:01 2010 +0200
@@ -48,6 +48,7 @@
         val offset = snapshot.revert(buffer_offset)
         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) {
               case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
                   List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>