# HG changeset patch
# User wenzelm
# Date 1542628223 -3600
# Node ID fc1a8df3062de3325321438506da83a95892c001
# Parent  b367c22c3dd8abadabc90e0ca357b3418a035ec4
more Haskell operations;

diff -r b367c22c3dd8 -r fc1a8df3062d src/Tools/Haskell/Haskell.thy
--- 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
diff -r b367c22c3dd8 -r fc1a8df3062d src/Tools/Haskell/Markup.hs
--- 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