--- a/src/Pure/ML/ml_compiler.ML Fri Dec 23 11:19:28 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Fri Dec 23 11:21:38 2016 +0100
@@ -109,8 +109,6 @@
| reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
| reported loc (PolyML.PTtype types) = reported_types loc types
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
- | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
- | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
| reported loc (PolyML.PTcompletions names) = reported_completions loc names
| reported _ _ = I
and reported_tree (loc, props) = fold (reported loc) props;
--- a/src/Pure/PIDE/rendering.scala Fri Dec 23 11:19:28 2016 +0100
+++ b/src/Pure/PIDE/rendering.scala Fri Dec 23 11:21:38 2016 +0100
@@ -64,10 +64,7 @@
Some(Text.Info(r, (t1 + t2, info)))
case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
- if kind != "" &&
- kind != Markup.ML_DEF &&
- kind != Markup.ML_OPEN &&
- kind != Markup.ML_STRUCTURE =>
+ if kind != "" && kind != Markup.ML_DEF =>
val kind1 = Word.implode(Word.explode('_', kind))
val txt1 =
if (name == "") kind1
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Dec 23 11:19:28 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Dec 23 11:21:38 2016 +0100
@@ -478,11 +478,7 @@
val link = PIDE.editor.hyperlink_url(name)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
- case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
- if !props.exists(
- { case (Markup.KIND, Markup.ML_OPEN) => true
- case (Markup.KIND, Markup.ML_STRUCTURE) => true
- case _ => false }) =>
+ case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))