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(