src/Tools/Haskell/Haskell.thy

 
   completionN, completion, no_completionN, no_completion,
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
 
+  expressionN, expression,
+
+  citationN, citation,
+
+  pathN, urlN, docN,
+
   markupN, consistentN, unbreakableN, indentN, widthN,
   blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
 
   wordsN, words, no_wordsN, no_words,
 

 properties :: Properties.T -> T -> T
 properties more_props (elem, props) =
   (elem, fold_rev Properties.put more_props props)
 
 markup_elem name = (name, (name, []) :: T)
+markup_string name prop = (name, \s -> (name, [(prop, s)]) :: T)
 
 
 {- misc properties -}
 
 nameN :: String

 fileN = \<open>Markup.fileN\<close>
 idN = \<open>Markup.idN\<close>
 
 positionN :: String; position :: T
 (positionN, position) = markup_elem \<open>Markup.positionN\<close>
+
+
+{- expression -}
+
+expressionN :: String
+expressionN = \<open>Markup.expressionN\<close>
+
+expression :: String -> T
+expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
+
+
+{- citation -}
+
+citationN :: String; citation :: String -> T
+(citationN, citation) = markup_string \<open>Markup.citationN\<close> nameN
+
+
+{- external resources -}
+
+pathN :: String; path :: String -> T
+(pathN, path) = markup_string \<open>Markup.pathN\<close> nameN
+
+urlN :: String; url :: String -> T
+(urlN, url) = markup_string \<open>Markup.urlN\<close> nameN
+
+docN :: String; doc :: String -> T
+(docN, doc) = markup_string \<open>Markup.docN\<close> nameN
 
 
 {- pretty printing -}
 
 markupN, consistentN, unbreakableN, indentN :: String