# HG changeset patch
# User nipkow
# Date 1542637932 -3600
# Node ID e8dea06456b4129dcf0626d267ff6b4b4253d03f
# Parent  fc1a8df3062de3325321438506da83a95892c001# Parent  248696d0a05f08ea74f2330bdc2e9ee40a32e057
merged

diff -r 248696d0a05f -r e8dea06456b4 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Nov 19 13:40:04 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 19 15:32:12 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";
 
diff -r 248696d0a05f -r e8dea06456b4 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Nov 19 13:40:04 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Mon Nov 19 15:32:12 2018 +0100
@@ -249,6 +249,8 @@
 
   nameN, name, xnameN, xname, kindN,
 
+  bindingN, binding, entityN, entity, defN, refN,
+
   completionN, completion, no_completionN, no_completion,
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
@@ -329,6 +331,24 @@
 kindN = \<open>Markup.kindN\<close>
 
 
+{- formal entities -}
+
+bindingN :: String; binding :: T
+(bindingN, binding) = markup_elem \<open>Markup.bindingN\<close>
+
+entityN :: String; entity :: String -> String -> T
+entityN = \<open>Markup.entityN\<close>
+entity kind name =
+  (entityN,
+    (if null name then [] else [(nameN, name)]) ++ (if null kind then [] else [(kindN, kind)]))
+
+defN :: String
+defN = \<open>Markup.defN\<close>
+
+refN :: String
+refN = \<open>Markup.refN\<close>
+
+
 {- completion -}
 
 completionN :: String; completion :: T
diff -r 248696d0a05f -r e8dea06456b4 src/Tools/Haskell/Markup.hs
--- a/src/Tools/Haskell/Markup.hs	Mon Nov 19 13:40:04 2018 +0100
+++ b/src/Tools/Haskell/Markup.hs	Mon Nov 19 15:32:12 2018 +0100
@@ -14,6 +14,8 @@
 
   nameN, name, xnameN, xname, kindN,
 
+  bindingN, binding, entityN, entity, defN, refN,
+
   completionN, completion, no_completionN, no_completion,
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
@@ -94,6 +96,24 @@
 kindN = "kind"
 
 
+{- formal entities -}
+
+bindingN :: String; binding :: T
+(bindingN, binding) = markup_elem "binding"
+
+entityN :: String; entity :: String -> String -> T
+entityN = "entity"
+entity kind name =
+  (entityN,
+    (if null name then [] else [(nameN, name)]) ++ (if null kind then [] else [(kindN, kind)]))
+
+defN :: String
+defN = "def"
+
+refN :: String
+refN = "ref"
+
+
 {- completion -}
 
 completionN :: String; completion :: T