diff -r 560263485988 -r 2dec32c7313f src/Tools/Haskell/Markup.hs
--- a/src/Tools/Haskell/Markup.hs	Sun Nov 04 15:28:51 2018 +0100
+++ b/src/Tools/Haskell/Markup.hs	Sun Nov 04 17:19:56 2018 +0100
@@ -7,12 +7,44 @@
 Quasi-abstract markup elements.
 -}
 
-module Isabelle.Markup (T, empty, is_empty, Output, no_output)
+module Isabelle.Markup (
+  T, empty, is_empty, properties,
+
+  nameN, name, xnameN, xname, kindN,
+
+  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+
+  wordsN, words, no_wordsN, no_words,
+
+  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
+  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
+  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
+  token_rangeN, token_range,
+  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
+
+  antiquotedN, antiquoted, antiquoteN, antiquote,
+
+  paragraphN, paragraph, text_foldN, text_fold,
+
+  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
+  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
+  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
+
+  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
+  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
+
+  intensifyN, intensify,
+  Output, no_output)
 where
 
+import Prelude hiding (words, error)
+
+import Isabelle.Library
 import qualified Isabelle.Properties as Properties
 
 
+{- basic markup -}
+
 type T = (String, Properties.T)
 
 empty :: T
@@ -22,6 +54,199 @@
 is_empty ("", _) = True
 is_empty _ = False
 
+properties :: Properties.T -> T -> T
+properties more_props (elem, props) =
+  (elem, fold_rev Properties.put more_props props)
+
+markup_elem name = (name, (name, []) :: T)
+
+
+{- misc properties -}
+
+nameN :: String
+nameN = "name"
+
+name :: String -> T -> T
+name a = properties [(nameN, a)]
+
+xnameN :: String
+xnameN = "xname"
+
+xname :: String -> T -> T
+xname a = properties [(xnameN, a)]
+
+kindN :: String
+kindN = "kind"
+
+
+{- position -}
+
+lineN, end_lineN :: String
+lineN = "line"
+end_lineN = "end_line"
+
+offsetN, end_offsetN :: String
+offsetN = "offset"
+end_offsetN = "end_offset"
+
+fileN, idN :: String
+fileN = "file"
+idN = "id"
+
+positionN :: String; position :: T
+(positionN, position) = markup_elem "position"
+
+
+{- text properties -}
+
+wordsN :: String; words :: T
+(wordsN, words) = markup_elem "words"
+
+no_wordsN :: String; no_words :: T
+(no_wordsN, no_words) = markup_elem "no_words"
+
+
+{- inner syntax -}
+
+tfreeN :: String; tfree :: T
+(tfreeN, tfree) = markup_elem "tfree"
+
+tvarN :: String; tvar :: T
+(tvarN, tvar) = markup_elem "tvar"
+
+freeN :: String; free :: T
+(freeN, free) = markup_elem "free"
+
+skolemN :: String; skolem :: T
+(skolemN, skolem) = markup_elem "skolem"
+
+boundN :: String; bound :: T
+(boundN, bound) = markup_elem "bound"
+
+varN :: String; var :: T
+(varN, var) = markup_elem "var"
+
+numeralN :: String; numeral :: T
+(numeralN, numeral) = markup_elem "numeral"
+
+literalN :: String; literal :: T
+(literalN, literal) = markup_elem "literal"
+
+delimiterN :: String; delimiter :: T
+(delimiterN, delimiter) = markup_elem "delimiter"
+
+inner_stringN :: String; inner_string :: T
+(inner_stringN, inner_string) = markup_elem "inner_string"
+
+inner_cartoucheN :: String; inner_cartouche :: T
+(inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"
+
+inner_commentN :: String; inner_comment :: T
+(inner_commentN, inner_comment) = markup_elem "inner_comment"
+
+
+token_rangeN :: String; token_range :: T
+(token_rangeN, token_range) = markup_elem "token_range"
+
+
+sortingN :: String; sorting :: T
+(sortingN, sorting) = markup_elem "sorting"
+
+typingN :: String; typing :: T
+(typingN, typing) = markup_elem "typing"
+
+class_parameterN :: String; class_parameter :: T
+(class_parameterN, class_parameter) = markup_elem "class_parameter"
+
+
+{- antiquotations -}
+
+antiquotedN :: String; antiquoted :: T
+(antiquotedN, antiquoted) = markup_elem "antiquoted"
+
+antiquoteN :: String; antiquote :: T
+(antiquoteN, antiquote) = markup_elem "antiquote"
+
+
+{- text structure -}
+
+paragraphN :: String; paragraph :: T
+(paragraphN, paragraph) = markup_elem "paragraph"
+
+text_foldN :: String; text_fold :: T
+(text_foldN, text_fold) = markup_elem "text_fold"
+
+
+{- outer syntax -}
+
+keyword1N :: String; keyword1 :: T
+(keyword1N, keyword1) = markup_elem "keyword1"
+
+keyword2N :: String; keyword2 :: T
+(keyword2N, keyword2) = markup_elem "keyword2"
+
+keyword3N :: String; keyword3 :: T
+(keyword3N, keyword3) = markup_elem "keyword3"
+
+quasi_keywordN :: String; quasi_keyword :: T
+(quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"
+
+improperN :: String; improper :: T
+(improperN, improper) = markup_elem "improper"
+
+operatorN :: String; operator :: T
+(operatorN, operator) = markup_elem "operator"
+
+stringN :: String; string :: T
+(stringN, string) = markup_elem "string"
+
+alt_stringN :: String; alt_string :: T
+(alt_stringN, alt_string) = markup_elem "alt_string"
+
+verbatimN :: String; verbatim :: T
+(verbatimN, verbatim) = markup_elem "verbatim"
+
+cartoucheN :: String; cartouche :: T
+(cartoucheN, cartouche) = markup_elem "cartouche"
+
+commentN :: String; comment :: T
+(commentN, comment) = markup_elem "comment"
+
+
+{- messages -}
+
+writelnN :: String; writeln :: T
+(writelnN, writeln) = markup_elem "writeln"
+
+stateN :: String; state :: T
+(stateN, state) = markup_elem "state"
+
+informationN :: String; information :: T
+(informationN, information) = markup_elem "information"
+
+tracingN :: String; tracing :: T
+(tracingN, tracing) = markup_elem "tracing"
+
+warningN :: String; warning :: T
+(warningN, warning) = markup_elem "warning"
+
+legacyN :: String; legacy :: T
+(legacyN, legacy) = markup_elem "legacy"
+
+errorN :: String; error :: T
+(errorN, error) = markup_elem "error"
+
+reportN :: String; report :: T
+(reportN, report) = markup_elem "report"
+
+no_reportN :: String; no_report :: T
+(no_reportN, no_report) = markup_elem "no_report"
+
+intensifyN :: String; intensify :: T
+(intensifyN, intensify) = markup_elem "intensify"
+
+
+{- output -}
 
 type Output = (String, String)