src/Tools/jEdit/src/isabelle_hyperlinks.scala
changeset 45709 87017fcbad83
parent 45672 a497c5d4a523
child 46178 1c5c88f6feb5
     1.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Dec 01 13:34:16 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Dec 01 14:29:14 2011 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4              snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
     1.5                Markup_Tree.Select[Hyperlink](
     1.6                  {
     1.7 -                  // FIXME Isabelle_Document.Hyperlink extractor
     1.8 +                  // FIXME Protocol.Hyperlink extractor
     1.9                    case Text.Info(info_range,
    1.10                        XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    1.11                      if (props.find(