# HG changeset patch
# User wenzelm
# Date 1542035252 -3600
# Node ID 36d7110082929a9f4477416f1c68454cb8a4530a
# Parent  fb77612d11ebd278af2244820498d6708f807690
more Haskell operations;

diff -r fb77612d11eb -r 36d711008292 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Nov 12 15:36:55 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Mon Nov 12 16:07:32 2018 +0100
@@ -253,6 +253,12 @@
 
   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,
 
@@ -302,6 +308,7 @@
   (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 -}
@@ -349,6 +356,33 @@
 (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
diff -r fb77612d11eb -r 36d711008292 src/Tools/Haskell/Markup.hs
--- a/src/Tools/Haskell/Markup.hs	Mon Nov 12 15:36:55 2018 +0100
+++ b/src/Tools/Haskell/Markup.hs	Mon Nov 12 16:07:32 2018 +0100
@@ -18,6 +18,12 @@
 
   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,
 
@@ -67,6 +73,7 @@
   (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 -}
@@ -114,6 +121,33 @@
 (positionN, position) = markup_elem "position"
 
 
+{- expression -}
+
+expressionN :: String
+expressionN = "expression"
+
+expression :: String -> T
+expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
+
+
+{- citation -}
+
+citationN :: String; citation :: String -> T
+(citationN, citation) = markup_string "citation" nameN
+
+
+{- external resources -}
+
+pathN :: String; path :: String -> T
+(pathN, path) = markup_string "path" nameN
+
+urlN :: String; url :: String -> T
+(urlN, url) = markup_string "url" nameN
+
+docN :: String; doc :: String -> T
+(docN, doc) = markup_string "doc" nameN
+
+
 {- pretty printing -}
 
 markupN, consistentN, unbreakableN, indentN :: String