unused -- left-over from Proof General;
authorwenzelm
Mon, 19 Nov 2018 12:39:39 +0100
changeset 69314 b367c22c3dd8
parent 69313 b021008c5397
child 69315 fc1a8df3062d
unused -- left-over from Proof General;
src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Nov 18 18:07:51 2018 +0000
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 19 12:39:39 2018 +0100
@@ -42,7 +42,6 @@
   val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
-  val get_entity_kind: T -> string option
   val defN: string
   val refN: string
   val completionN: string val completion: T
@@ -326,10 +325,6 @@
   (entityN,
     (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
-fun get_entity_kind (name, props) =
-  if name = entityN then Properties.get props kindN
-  else NONE;
-
 val defN = "def";
 val refN = "ref";