--- 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";
--- 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
--- 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