omit unused markup;
authorwenzelm
Fri Dec 23 11:21:38 2016 +0100 (2016-12-23)
changeset 64660ef85bb6491b3
parent 64659 c64b258f6801
child 64661 84aea854dc3c
omit unused markup;
src/Pure/ML/ml_compiler.ML
src/Pure/PIDE/rendering.scala
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Pure/ML/ml_compiler.ML	Fri Dec 23 11:19:28 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_compiler.ML	Fri Dec 23 11:21:38 2016 +0100
     1.3 @@ -109,8 +109,6 @@
     1.4        | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
     1.5        | reported loc (PolyML.PTtype types) = reported_types loc types
     1.6        | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
     1.7 -      | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
     1.8 -      | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
     1.9        | reported loc (PolyML.PTcompletions names) = reported_completions loc names
    1.10        | reported _ _ = I
    1.11      and reported_tree (loc, props) = fold (reported loc) props;
     2.1 --- a/src/Pure/PIDE/rendering.scala	Fri Dec 23 11:19:28 2016 +0100
     2.2 +++ b/src/Pure/PIDE/rendering.scala	Fri Dec 23 11:21:38 2016 +0100
     2.3 @@ -64,10 +64,7 @@
     2.4              Some(Text.Info(r, (t1 + t2, info)))
     2.5  
     2.6            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
     2.7 -          if kind != "" &&
     2.8 -            kind != Markup.ML_DEF &&
     2.9 -            kind != Markup.ML_OPEN &&
    2.10 -            kind != Markup.ML_STRUCTURE =>
    2.11 +          if kind != "" && kind != Markup.ML_DEF =>
    2.12              val kind1 = Word.implode(Word.explode('_', kind))
    2.13              val txt1 =
    2.14                if (name == "") kind1
     3.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Dec 23 11:19:28 2016 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Dec 23 11:21:38 2016 +0100
     3.3 @@ -478,11 +478,7 @@
     3.4              val link = PIDE.editor.hyperlink_url(name)
     3.5              Some(links :+ Text.Info(snapshot.convert(info_range), link))
     3.6  
     3.7 -          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
     3.8 -          if !props.exists(
     3.9 -            { case (Markup.KIND, Markup.ML_OPEN) => true
    3.10 -              case (Markup.KIND, Markup.ML_STRUCTURE) => true
    3.11 -              case _ => false }) =>
    3.12 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    3.13              val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
    3.14              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    3.15