# HG changeset patch
# User wenzelm
# Date 1542627579 -3600
# Node ID b367c22c3dd8abadabc90e0ca357b3418a035ec4
# Parent  b021008c5397c4def58be3da5d2023ae9e846199
unused -- left-over from Proof General;

diff -r b021008c5397 -r b367c22c3dd8 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";