src/Tools/Haskell/Markup.hs

 
 module Isabelle.Markup (
   T, empty, is_empty, properties,
 
   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,
 

 xname :: String -> T -> T
 xname a = properties [(xnameN, a)]
 
 kindN :: String
 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