# HG changeset patch
# User wenzelm
# Date 1482488498 -3600
# Node ID ef85bb6491b30cd75758b7d092882235c28bdb86
# Parent  c64b258f6801e94584433f26fd319ac7671e6ad3
omit unused markup;

diff -r c64b258f6801 -r ef85bb6491b3 src/Pure/ML/ml_compiler.ML
--- 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;
diff -r c64b258f6801 -r ef85bb6491b3 src/Pure/PIDE/rendering.scala
--- 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
diff -r c64b258f6801 -r ef85bb6491b3 src/Tools/jEdit/src/jedit_rendering.scala
--- 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))