--- a/src/Tools/Haskell/Haskell.thy Mon Nov 19 12:39:39 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Mon Nov 19 12:50:23 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 12:39:39 2018 +0100
+++ b/src/Tools/Haskell/Markup.hs Mon Nov 19 12:50:23 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