src/Tools/Haskell/Markup.hs
changeset 69234 2dec32c7313f
parent 69227 71b48b749836
child 69248 9f21381600e3
     1.1 --- a/src/Tools/Haskell/Markup.hs	Sun Nov 04 15:28:51 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Markup.hs	Sun Nov 04 17:19:56 2018 +0100
     1.3 @@ -7,12 +7,44 @@
     1.4  Quasi-abstract markup elements.
     1.5  -}
     1.6  
     1.7 -module Isabelle.Markup (T, empty, is_empty, Output, no_output)
     1.8 +module Isabelle.Markup (
     1.9 +  T, empty, is_empty, properties,
    1.10 +
    1.11 +  nameN, name, xnameN, xname, kindN,
    1.12 +
    1.13 +  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
    1.14 +
    1.15 +  wordsN, words, no_wordsN, no_words,
    1.16 +
    1.17 +  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    1.18 +  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
    1.19 +  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
    1.20 +  token_rangeN, token_range,
    1.21 +  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
    1.22 +
    1.23 +  antiquotedN, antiquoted, antiquoteN, antiquote,
    1.24 +
    1.25 +  paragraphN, paragraph, text_foldN, text_fold,
    1.26 +
    1.27 +  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
    1.28 +  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
    1.29 +  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
    1.30 +
    1.31 +  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
    1.32 +  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
    1.33 +
    1.34 +  intensifyN, intensify,
    1.35 +  Output, no_output)
    1.36  where
    1.37  
    1.38 +import Prelude hiding (words, error)
    1.39 +
    1.40 +import Isabelle.Library
    1.41  import qualified Isabelle.Properties as Properties
    1.42  
    1.43  
    1.44 +{- basic markup -}
    1.45 +
    1.46  type T = (String, Properties.T)
    1.47  
    1.48  empty :: T
    1.49 @@ -22,6 +54,199 @@
    1.50  is_empty ("", _) = True
    1.51  is_empty _ = False
    1.52  
    1.53 +properties :: Properties.T -> T -> T
    1.54 +properties more_props (elem, props) =
    1.55 +  (elem, fold_rev Properties.put more_props props)
    1.56 +
    1.57 +markup_elem name = (name, (name, []) :: T)
    1.58 +
    1.59 +
    1.60 +{- misc properties -}
    1.61 +
    1.62 +nameN :: String
    1.63 +nameN = "name"
    1.64 +
    1.65 +name :: String -> T -> T
    1.66 +name a = properties [(nameN, a)]
    1.67 +
    1.68 +xnameN :: String
    1.69 +xnameN = "xname"
    1.70 +
    1.71 +xname :: String -> T -> T
    1.72 +xname a = properties [(xnameN, a)]
    1.73 +
    1.74 +kindN :: String
    1.75 +kindN = "kind"
    1.76 +
    1.77 +
    1.78 +{- position -}
    1.79 +
    1.80 +lineN, end_lineN :: String
    1.81 +lineN = "line"
    1.82 +end_lineN = "end_line"
    1.83 +
    1.84 +offsetN, end_offsetN :: String
    1.85 +offsetN = "offset"
    1.86 +end_offsetN = "end_offset"
    1.87 +
    1.88 +fileN, idN :: String
    1.89 +fileN = "file"
    1.90 +idN = "id"
    1.91 +
    1.92 +positionN :: String; position :: T
    1.93 +(positionN, position) = markup_elem "position"
    1.94 +
    1.95 +
    1.96 +{- text properties -}
    1.97 +
    1.98 +wordsN :: String; words :: T
    1.99 +(wordsN, words) = markup_elem "words"
   1.100 +
   1.101 +no_wordsN :: String; no_words :: T
   1.102 +(no_wordsN, no_words) = markup_elem "no_words"
   1.103 +
   1.104 +
   1.105 +{- inner syntax -}
   1.106 +
   1.107 +tfreeN :: String; tfree :: T
   1.108 +(tfreeN, tfree) = markup_elem "tfree"
   1.109 +
   1.110 +tvarN :: String; tvar :: T
   1.111 +(tvarN, tvar) = markup_elem "tvar"
   1.112 +
   1.113 +freeN :: String; free :: T
   1.114 +(freeN, free) = markup_elem "free"
   1.115 +
   1.116 +skolemN :: String; skolem :: T
   1.117 +(skolemN, skolem) = markup_elem "skolem"
   1.118 +
   1.119 +boundN :: String; bound :: T
   1.120 +(boundN, bound) = markup_elem "bound"
   1.121 +
   1.122 +varN :: String; var :: T
   1.123 +(varN, var) = markup_elem "var"
   1.124 +
   1.125 +numeralN :: String; numeral :: T
   1.126 +(numeralN, numeral) = markup_elem "numeral"
   1.127 +
   1.128 +literalN :: String; literal :: T
   1.129 +(literalN, literal) = markup_elem "literal"
   1.130 +
   1.131 +delimiterN :: String; delimiter :: T
   1.132 +(delimiterN, delimiter) = markup_elem "delimiter"
   1.133 +
   1.134 +inner_stringN :: String; inner_string :: T
   1.135 +(inner_stringN, inner_string) = markup_elem "inner_string"
   1.136 +
   1.137 +inner_cartoucheN :: String; inner_cartouche :: T
   1.138 +(inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"
   1.139 +
   1.140 +inner_commentN :: String; inner_comment :: T
   1.141 +(inner_commentN, inner_comment) = markup_elem "inner_comment"
   1.142 +
   1.143 +
   1.144 +token_rangeN :: String; token_range :: T
   1.145 +(token_rangeN, token_range) = markup_elem "token_range"
   1.146 +
   1.147 +
   1.148 +sortingN :: String; sorting :: T
   1.149 +(sortingN, sorting) = markup_elem "sorting"
   1.150 +
   1.151 +typingN :: String; typing :: T
   1.152 +(typingN, typing) = markup_elem "typing"
   1.153 +
   1.154 +class_parameterN :: String; class_parameter :: T
   1.155 +(class_parameterN, class_parameter) = markup_elem "class_parameter"
   1.156 +
   1.157 +
   1.158 +{- antiquotations -}
   1.159 +
   1.160 +antiquotedN :: String; antiquoted :: T
   1.161 +(antiquotedN, antiquoted) = markup_elem "antiquoted"
   1.162 +
   1.163 +antiquoteN :: String; antiquote :: T
   1.164 +(antiquoteN, antiquote) = markup_elem "antiquote"
   1.165 +
   1.166 +
   1.167 +{- text structure -}
   1.168 +
   1.169 +paragraphN :: String; paragraph :: T
   1.170 +(paragraphN, paragraph) = markup_elem "paragraph"
   1.171 +
   1.172 +text_foldN :: String; text_fold :: T
   1.173 +(text_foldN, text_fold) = markup_elem "text_fold"
   1.174 +
   1.175 +
   1.176 +{- outer syntax -}
   1.177 +
   1.178 +keyword1N :: String; keyword1 :: T
   1.179 +(keyword1N, keyword1) = markup_elem "keyword1"
   1.180 +
   1.181 +keyword2N :: String; keyword2 :: T
   1.182 +(keyword2N, keyword2) = markup_elem "keyword2"
   1.183 +
   1.184 +keyword3N :: String; keyword3 :: T
   1.185 +(keyword3N, keyword3) = markup_elem "keyword3"
   1.186 +
   1.187 +quasi_keywordN :: String; quasi_keyword :: T
   1.188 +(quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"
   1.189 +
   1.190 +improperN :: String; improper :: T
   1.191 +(improperN, improper) = markup_elem "improper"
   1.192 +
   1.193 +operatorN :: String; operator :: T
   1.194 +(operatorN, operator) = markup_elem "operator"
   1.195 +
   1.196 +stringN :: String; string :: T
   1.197 +(stringN, string) = markup_elem "string"
   1.198 +
   1.199 +alt_stringN :: String; alt_string :: T
   1.200 +(alt_stringN, alt_string) = markup_elem "alt_string"
   1.201 +
   1.202 +verbatimN :: String; verbatim :: T
   1.203 +(verbatimN, verbatim) = markup_elem "verbatim"
   1.204 +
   1.205 +cartoucheN :: String; cartouche :: T
   1.206 +(cartoucheN, cartouche) = markup_elem "cartouche"
   1.207 +
   1.208 +commentN :: String; comment :: T
   1.209 +(commentN, comment) = markup_elem "comment"
   1.210 +
   1.211 +
   1.212 +{- messages -}
   1.213 +
   1.214 +writelnN :: String; writeln :: T
   1.215 +(writelnN, writeln) = markup_elem "writeln"
   1.216 +
   1.217 +stateN :: String; state :: T
   1.218 +(stateN, state) = markup_elem "state"
   1.219 +
   1.220 +informationN :: String; information :: T
   1.221 +(informationN, information) = markup_elem "information"
   1.222 +
   1.223 +tracingN :: String; tracing :: T
   1.224 +(tracingN, tracing) = markup_elem "tracing"
   1.225 +
   1.226 +warningN :: String; warning :: T
   1.227 +(warningN, warning) = markup_elem "warning"
   1.228 +
   1.229 +legacyN :: String; legacy :: T
   1.230 +(legacyN, legacy) = markup_elem "legacy"
   1.231 +
   1.232 +errorN :: String; error :: T
   1.233 +(errorN, error) = markup_elem "error"
   1.234 +
   1.235 +reportN :: String; report :: T
   1.236 +(reportN, report) = markup_elem "report"
   1.237 +
   1.238 +no_reportN :: String; no_report :: T
   1.239 +(no_reportN, no_report) = markup_elem "no_report"
   1.240 +
   1.241 +intensifyN :: String; intensify :: T
   1.242 +(intensifyN, intensify) = markup_elem "intensify"
   1.243 +
   1.244 +
   1.245 +{- output -}
   1.246  
   1.247  type Output = (String, String)
   1.248