Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 24 Aug 2010 21:22:01 +0200
changeset 38660 049fdf15144f
parent 38659 afac51977705
child 38661 f1ba2ae8e58a
tuned;
src/Tools/jEdit/src/jedit/document_view.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala file | annotate | diff | comparison | revisions 
--- 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 =
--- 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), _)))) =>
isabelle