src/Tools/Haskell/Haskell.thy
author wenzelm
Thu, 20 Dec 2018 16:34:23 +0100
changeset 69486 59ada9f63cc5
parent 69482 186b03abb764
child 69490 ce85542368b9
permissions -rw-r--r--
proper trim_line according to ML/Scala versions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/Haskell/Haskell.thy
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
     3
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
     4
Support for Isabelle tools in Haskell.
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     5
*)
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     6
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     7
theory Haskell
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     8
  imports Pure
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     9
begin
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
    10
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
    11
generate_file "Isabelle/Library.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
    12
{-  Title:      Isabelle/Library.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    13
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    14
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    15
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    16
Basic library of Isabelle idioms.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
    17
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
    18
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>, \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    19
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    20
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    21
module Isabelle.Library (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    22
  (|>), (|->), (#>), (#->),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    23
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    24
  the, the_default,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    25
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    26
  fold, fold_rev, single, map_index, get_index,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    27
69477
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
    28
  proper_string, quote, space_implode, commas, commas_quote, cat_lines,
69453
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
    29
  space_explode, split_lines, trim_line, clean_name)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    30
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    31
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    32
import Data.Maybe
69453
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
    33
import qualified Data.List as List
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
    34
import qualified Data.List.Split as Split
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    35
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    36
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    37
{- functions -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    38
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    39
(|>) :: a -> (a -> b) -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    40
x |> f = f x
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    41
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    42
(|->) :: (a, b) -> (a -> b -> c) -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    43
(x, y) |-> f = f x y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    44
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    45
(#>) :: (a -> b) -> (b -> c) -> a -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    46
(f #> g) x = x |> f |> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    47
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    48
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    49
(f #-> g) x  = x |> f |-> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    50
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    51
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    52
{- options -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    53
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    54
the :: Maybe a -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    55
the (Just x) = x
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    56
the Nothing = error "the Nothing"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    57
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    58
the_default :: a -> Maybe a -> a
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    59
the_default x Nothing = x
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    60
the_default _ (Just y) = y
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    61
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    62
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    63
{- lists -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    64
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    65
fold :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    66
fold _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    67
fold f (x : xs) y = fold f xs (f x y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    68
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    69
fold_rev :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    70
fold_rev _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    71
fold_rev f (x : xs) y = f x (fold_rev f xs y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    72
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    73
single :: a -> [a]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    74
single x = [x]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    75
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    76
map_index :: ((Int, a) -> b) -> [a] -> [b]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    77
map_index f = map_aux 0
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    78
  where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    79
    map_aux _ [] = []
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    80
    map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    81
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    82
get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    83
get_index f = get_aux 0
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    84
  where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    85
    get_aux _ [] = Nothing
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    86
    get_aux i (x : xs) =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    87
      case f x of
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    88
        Nothing -> get_aux (i + 1) xs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    89
        Just y -> Just (i, y)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    90
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    91
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    92
{- strings -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    93
69477
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
    94
proper_string :: String -> Maybe String
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
    95
proper_string s = if null s then Nothing else Just s
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
    96
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    97
quote :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    98
quote s = "\"" ++ s ++ "\""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    99
69453
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   100
space_implode :: String -> [String] -> String
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   101
space_implode = List.intercalate
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   102
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   103
commas, commas_quote :: [String] -> String
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   104
commas = space_implode ", "
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   105
commas_quote = commas . map quote
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   106
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   107
cat_lines :: [String] -> String
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   108
cat_lines = space_implode "\n"
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   109
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   110
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   111
space_explode :: Char -> String -> [String]
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   112
space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   113
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   114
split_lines :: String -> [String]
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   115
split_lines = space_explode '\n'
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
   116
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   117
trim_line :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   118
trim_line line =
69486
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   119
  if not (null line) && (last line == '\r' || last line == '\n') then
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   120
    case reverse line of
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   121
      '\n' : '\r' : rest -> reverse rest
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   122
      '\r' : rest -> reverse rest
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   123
      '\n' : rest -> reverse rest
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   124
      _ -> line
59ada9f63cc5 proper trim_line according to ML/Scala versions;
wenzelm
parents: 69482
diff changeset
   125
  else line
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   126
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   127
clean_name :: String -> String
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   128
clean_name = reverse #> dropWhile (== '_') #> reverse
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   129
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   130
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   131
generate_file "Isabelle/Value.hs" = \<open>
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   132
{-  Title:      Haskell/Tools/Value.hs
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   133
    Author:     Makarius
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   134
    LICENSE:    BSD 3-clause (Isabelle)
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   135
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   136
Plain values, represented as string.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   137
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   138
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   139
-}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   140
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   141
module Isabelle.Value
69452
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   142
  (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   143
where
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   144
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   145
import Data.Maybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   146
import qualified Data.List as List
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   147
import qualified Text.Read as Read
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   148
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   149
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   150
{- bool -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   151
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   152
print_bool :: Bool -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   153
print_bool True = "true"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   154
print_bool False = "false"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   155
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   156
parse_bool :: String -> Maybe Bool
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   157
parse_bool "true" = Just True
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   158
parse_bool "false" = Just False
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   159
parse_bool _ = Nothing
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   160
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   161
69452
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   162
{- nat -}
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   163
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   164
parse_nat :: String -> Maybe Int
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   165
parse_nat s =
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   166
  case Read.readMaybe s of
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   167
    Just n | n >= 0 -> Just n
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   168
    _ -> Nothing
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   169
704915cf59fa more uniform multi-language operations;
wenzelm
parents: 69449
diff changeset
   170
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   171
{- int -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   172
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   173
print_int :: Int -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   174
print_int = show
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   175
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   176
parse_int :: String -> Maybe Int
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   177
parse_int = Read.readMaybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   178
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   179
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   180
{- real -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   181
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   182
print_real :: Double -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   183
print_real x =
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   184
  let s = show x in
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   185
    case span (/= '.') s of
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   186
      (a, '.' : b) | List.all (== '0') b -> a
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   187
      _ -> s
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   188
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   189
parse_real :: String -> Maybe Double
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   190
parse_real = Read.readMaybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   191
\<close>
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   192
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   193
generate_file "Isabelle/Buffer.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   194
{-  Title:      Isabelle/Buffer.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   195
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   196
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   197
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   198
Efficient text buffers.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   199
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   200
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   201
-}
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   202
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   203
module Isabelle.Buffer (T, empty, add, content)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   204
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   205
69474
2633cf136335 tuned -- more compact;
wenzelm
parents: 69473
diff changeset
   206
import Isabelle.Library
2633cf136335 tuned -- more compact;
wenzelm
parents: 69473
diff changeset
   207
2633cf136335 tuned -- more compact;
wenzelm
parents: 69473
diff changeset
   208
2633cf136335 tuned -- more compact;
wenzelm
parents: 69473
diff changeset
   209
newtype T = Buffer [Char]
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   210
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   211
empty :: T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   212
empty = Buffer []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   213
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   214
add :: String -> T -> T
69474
2633cf136335 tuned -- more compact;
wenzelm
parents: 69473
diff changeset
   215
add s (Buffer cs) = Buffer (fold (:) s cs)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   216
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   217
content :: T -> String
69474
2633cf136335 tuned -- more compact;
wenzelm
parents: 69473
diff changeset
   218
content (Buffer cs) = reverse cs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   219
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   220
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   221
generate_file "Isabelle/Properties.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   222
{-  Title:      Isabelle/Properties.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   223
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   224
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   226
Property lists.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   227
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   228
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   229
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   230
69477
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   231
module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   232
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   233
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   234
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   235
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   236
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   237
type Entry = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   238
type T = [Entry]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   239
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   240
defined :: T -> String -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   241
defined props name = any (\(a, _) -> a == name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   242
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   243
get :: T -> String -> Maybe String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   244
get props name = List.lookup name props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   245
69477
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   246
get_value :: (String -> Maybe a) -> T -> String -> Maybe a
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   247
get_value parse props name =
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   248
  case get props name of
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   249
    Nothing -> Nothing
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   250
    Just s -> parse s
1690ba936016 more Isabelle/Haskell operations;
wenzelm
parents: 69476
diff changeset
   251
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   252
put :: Entry -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   253
put entry props = entry : remove (fst entry) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   254
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   255
remove :: String -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   256
remove name props =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   257
  if defined props name then filter (\(a, _) -> a /= name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   258
  else props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   259
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   260
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   261
generate_file "Isabelle/Markup.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
   262
{-  Title:      Haskell/Tools/Markup.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   263
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   264
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   265
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   266
Quasi-abstract markup elements.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   267
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   268
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   269
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   270
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   271
module Isabelle.Markup (
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   272
  T, empty, is_empty, properties,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   273
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   274
  nameN, name, xnameN, xname, kindN,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   275
69315
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   276
  bindingN, binding, entityN, entity, defN, refN,
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   277
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   278
  completionN, completion, no_completionN, no_completion,
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   279
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   280
  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   281
69291
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   282
  expressionN, expression,
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   283
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   284
  citationN, citation,
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   285
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   286
  pathN, urlN, docN,
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   287
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   288
  markupN, consistentN, unbreakableN, indentN, widthN,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   289
  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   290
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   291
  wordsN, words, no_wordsN, no_words,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   292
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   293
  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   294
  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
69320
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   295
  inner_cartoucheN, inner_cartouche,
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   296
  token_rangeN, token_range,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   297
  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   298
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   299
  antiquotedN, antiquoted, antiquoteN, antiquote,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   300
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   301
  paragraphN, paragraph, text_foldN, text_fold,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   302
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   303
  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   304
  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
69320
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   305
  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   306
  comment2N, comment2, comment3N, comment3,
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   307
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   308
  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   309
  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   310
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   311
  intensifyN, intensify,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   312
  Output, no_output)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   313
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   314
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   315
import Prelude hiding (words, error, break)
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   316
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   317
import Isabelle.Library
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   318
import qualified Isabelle.Properties as Properties
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   319
import qualified Isabelle.Value as Value
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   320
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   321
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   322
{- basic markup -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   323
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   324
type T = (String, Properties.T)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   325
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   326
empty :: T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   327
empty = ("", [])
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   328
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   329
is_empty :: T -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   330
is_empty ("", _) = True
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   331
is_empty _ = False
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   332
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   333
properties :: Properties.T -> T -> T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   334
properties more_props (elem, props) =
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   335
  (elem, fold_rev Properties.put more_props props)
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   336
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   337
markup_elem name = (name, (name, []) :: T)
69291
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   338
markup_string name prop = (name, \s -> (name, [(prop, s)]) :: T)
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   339
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   340
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   341
{- misc properties -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   342
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   343
nameN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   344
nameN = \<open>Markup.nameN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   345
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   346
name :: String -> T -> T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   347
name a = properties [(nameN, a)]
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   348
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   349
xnameN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   350
xnameN = \<open>Markup.xnameN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   351
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   352
xname :: String -> T -> T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   353
xname a = properties [(xnameN, a)]
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   354
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   355
kindN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   356
kindN = \<open>Markup.kindN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   357
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   358
69315
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   359
{- formal entities -}
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   360
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   361
bindingN :: String; binding :: T
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   362
(bindingN, binding) = markup_elem \<open>Markup.bindingN\<close>
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   363
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   364
entityN :: String; entity :: String -> String -> T
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   365
entityN = \<open>Markup.entityN\<close>
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   366
entity kind name =
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   367
  (entityN,
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   368
    (if null name then [] else [(nameN, name)]) ++ (if null kind then [] else [(kindN, kind)]))
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   369
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   370
defN :: String
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   371
defN = \<open>Markup.defN\<close>
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   372
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   373
refN :: String
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   374
refN = \<open>Markup.refN\<close>
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   375
fc1a8df3062d more Haskell operations;
wenzelm
parents: 69291
diff changeset
   376
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   377
{- completion -}
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   378
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   379
completionN :: String; completion :: T
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   380
(completionN, completion) = markup_elem \<open>Markup.completionN\<close>
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   381
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   382
no_completionN :: String; no_completion :: T
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   383
(no_completionN, no_completion) = markup_elem \<open>Markup.no_completionN\<close>
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   384
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   385
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   386
{- position -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   387
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   388
lineN, end_lineN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   389
lineN = \<open>Markup.lineN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   390
end_lineN = \<open>Markup.end_lineN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   391
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   392
offsetN, end_offsetN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   393
offsetN = \<open>Markup.offsetN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   394
end_offsetN = \<open>Markup.end_offsetN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   395
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   396
fileN, idN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   397
fileN = \<open>Markup.fileN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   398
idN = \<open>Markup.idN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   399
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   400
positionN :: String; position :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   401
(positionN, position) = markup_elem \<open>Markup.positionN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   402
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   403
69291
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   404
{- expression -}
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   405
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   406
expressionN :: String
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   407
expressionN = \<open>Markup.expressionN\<close>
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   408
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   409
expression :: String -> T
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   410
expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   411
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   412
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   413
{- citation -}
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   414
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   415
citationN :: String; citation :: String -> T
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   416
(citationN, citation) = markup_string \<open>Markup.citationN\<close> nameN
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   417
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   418
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   419
{- external resources -}
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   420
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   421
pathN :: String; path :: String -> T
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   422
(pathN, path) = markup_string \<open>Markup.pathN\<close> nameN
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   423
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   424
urlN :: String; url :: String -> T
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   425
(urlN, url) = markup_string \<open>Markup.urlN\<close> nameN
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   426
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   427
docN :: String; doc :: String -> T
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   428
(docN, doc) = markup_string \<open>Markup.docN\<close> nameN
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   429
36d711008292 more Haskell operations;
wenzelm
parents: 69290
diff changeset
   430
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   431
{- pretty printing -}
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   432
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   433
markupN, consistentN, unbreakableN, indentN :: String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   434
markupN = \<open>Markup.markupN\<close>;
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   435
consistentN = \<open>Markup.consistentN\<close>;
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   436
unbreakableN = \<open>Markup.unbreakableN\<close>;
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   437
indentN = \<open>Markup.indentN\<close>;
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   438
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   439
widthN :: String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   440
widthN = \<open>Markup.widthN\<close>
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   441
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   442
blockN :: String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   443
blockN = \<open>Markup.blockN\<close>
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   444
block :: Bool -> Int -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   445
block c i =
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   446
  (blockN,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   447
    (if c then [(consistentN, Value.print_bool c)] else []) ++
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   448
    (if i /= 0 then [(indentN, Value.print_int i)] else []))
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   449
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   450
breakN :: String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   451
breakN = \<open>Markup.breakN\<close>
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   452
break :: Int -> Int -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   453
break w i =
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   454
  (breakN,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   455
    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   456
    (if i /= 0 then [(indentN, Value.print_int i)] else []))
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   457
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   458
fbreakN :: String; fbreak :: T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   459
(fbreakN, fbreak) = markup_elem \<open>Markup.fbreakN\<close>
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   460
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   461
itemN :: String; item :: T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   462
(itemN, item) = markup_elem \<open>Markup.itemN\<close>
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   463
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
   464
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   465
{- text properties -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   466
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   467
wordsN :: String; words :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   468
(wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   469
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   470
no_wordsN :: String; no_words :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   471
(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   472
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   473
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   474
{- inner syntax -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   475
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   476
tfreeN :: String; tfree :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   477
(tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   478
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   479
tvarN :: String; tvar :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   480
(tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   481
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   482
freeN :: String; free :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   483
(freeN, free) = markup_elem \<open>Markup.freeN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   484
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   485
skolemN :: String; skolem :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   486
(skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   487
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   488
boundN :: String; bound :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   489
(boundN, bound) = markup_elem \<open>Markup.boundN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   490
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   491
varN :: String; var :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   492
(varN, var) = markup_elem \<open>Markup.varN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   493
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   494
numeralN :: String; numeral :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   495
(numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   496
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   497
literalN :: String; literal :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   498
(literalN, literal) = markup_elem \<open>Markup.literalN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   499
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   500
delimiterN :: String; delimiter :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   501
(delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   502
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   503
inner_stringN :: String; inner_string :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   504
(inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   505
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   506
inner_cartoucheN :: String; inner_cartouche :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   507
(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   508
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   509
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   510
token_rangeN :: String; token_range :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   511
(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   512
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   513
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   514
sortingN :: String; sorting :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   515
(sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   516
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   517
typingN :: String; typing :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   518
(typingN, typing) = markup_elem \<open>Markup.typingN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   519
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   520
class_parameterN :: String; class_parameter :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   521
(class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   522
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   523
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   524
{- antiquotations -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   525
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   526
antiquotedN :: String; antiquoted :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   527
(antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   528
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   529
antiquoteN :: String; antiquote :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   530
(antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   531
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   532
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   533
{- text structure -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   534
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   535
paragraphN :: String; paragraph :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   536
(paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   537
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   538
text_foldN :: String; text_fold :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   539
(text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   540
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   541
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   542
{- outer syntax -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   543
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   544
keyword1N :: String; keyword1 :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   545
(keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   546
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   547
keyword2N :: String; keyword2 :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   548
(keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   549
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   550
keyword3N :: String; keyword3 :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   551
(keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   552
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   553
quasi_keywordN :: String; quasi_keyword :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   554
(quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   555
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   556
improperN :: String; improper :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   557
(improperN, improper) = markup_elem \<open>Markup.improperN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   558
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   559
operatorN :: String; operator :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   560
(operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   561
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   562
stringN :: String; string :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   563
(stringN, string) = markup_elem \<open>Markup.stringN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   564
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   565
alt_stringN :: String; alt_string :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   566
(alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   567
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   568
verbatimN :: String; verbatim :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   569
(verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   570
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   571
cartoucheN :: String; cartouche :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   572
(cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   573
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   574
commentN :: String; comment :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   575
(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   576
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   577
69320
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   578
{- comments -}
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   579
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   580
comment1N :: String; comment1 :: T
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   581
(comment1N, comment1) = markup_elem \<open>Markup.comment1N\<close>
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   582
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   583
comment2N :: String; comment2 :: T
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   584
(comment2N, comment2) = markup_elem \<open>Markup.comment2N\<close>
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   585
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   586
comment3N :: String; comment3 :: T
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   587
(comment3N, comment3) = markup_elem \<open>Markup.comment3N\<close>
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   588
fc221fa79741 more comment markup;
wenzelm
parents: 69315
diff changeset
   589
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   590
{- messages -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   591
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   592
writelnN :: String; writeln :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   593
(writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   594
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   595
stateN :: String; state :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   596
(stateN, state) = markup_elem \<open>Markup.stateN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   597
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   598
informationN :: String; information :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   599
(informationN, information) = markup_elem \<open>Markup.informationN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   600
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   601
tracingN :: String; tracing :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   602
(tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   603
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   604
warningN :: String; warning :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   605
(warningN, warning) = markup_elem \<open>Markup.warningN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   606
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   607
legacyN :: String; legacy :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   608
(legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   609
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   610
errorN :: String; error :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   611
(errorN, error) = markup_elem \<open>Markup.errorN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   612
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   613
reportN :: String; report :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   614
(reportN, report) = markup_elem \<open>Markup.reportN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   615
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   616
no_reportN :: String; no_report :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   617
(no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   618
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   619
intensifyN :: String; intensify :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   620
(intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   621
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   622
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   623
{- output -}
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   624
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   625
type Output = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   626
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   627
no_output :: Output
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   628
no_output = ("", "")
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   629
\<close>
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   630
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   631
generate_file "Isabelle/Completion.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   632
{-  Title:      Isabelle/Completion.hs
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   633
    Author:     Makarius
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   634
    LICENSE:    BSD 3-clause (Isabelle)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   635
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   636
Completion of names.
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   637
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   638
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   639
-}
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   640
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   641
module Isabelle.Completion (
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   642
    Name, T, names, none, make, markup_element, markup_report, make_report
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   643
  ) where
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   644
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   645
import qualified Data.List as List
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   646
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   647
import Isabelle.Library
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   648
import qualified Isabelle.Properties as Properties
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   649
import qualified Isabelle.Markup as Markup
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   650
import qualified Isabelle.XML.Encode as Encode
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   651
import qualified Isabelle.XML as XML
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   652
import qualified Isabelle.YXML as YXML
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   653
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   654
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   655
type Name = (String, (String, String))  -- external name, kind, internal name
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   656
data T = Completion Properties.T Int [Name]  -- position, total length, names
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   657
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   658
names :: Int -> Properties.T -> [Name] -> T
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   659
names limit props names = Completion props (length names) (take limit names)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   660
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   661
none :: T
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   662
none = names 0 [] []
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   663
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   664
make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   665
make limit (name, props) make_names =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   666
  if name /= "" && name /= "_"
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   667
  then names limit props (make_names $ List.isPrefixOf $ clean_name name)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   668
  else none
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   669
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   670
markup_element :: T -> (Markup.T, XML.Body)
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   671
markup_element (Completion props total names) =
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   672
  if not (null names) then
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   673
    let
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   674
      markup = Markup.properties props Markup.completion
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   675
      body =
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   676
        Encode.pair Encode.int
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   677
          (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   678
          (total, names)
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   679
    in (markup, body)
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   680
  else (Markup.empty, [])
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   681
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   682
markup_report :: [T] -> String
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   683
markup_report [] = ""
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   684
markup_report elems =
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   685
  YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   686
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   687
make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   688
make_report limit name_props make_names =
bf6937af7fe8 clarified signature;
wenzelm
parents: 69288
diff changeset
   689
  markup_report [make limit name_props make_names]
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   690
\<close>
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
   691
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   692
generate_file "Isabelle/File.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   693
{-  Title:      Isabelle/File.hs
69278
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   694
    Author:     Makarius
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   695
    LICENSE:    BSD 3-clause (Isabelle)
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   696
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   697
File-system operations.
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   698
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   699
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
69278
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   700
-}
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   701
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   702
module Isabelle.File (setup, read, write, append) where
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   703
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   704
import Prelude hiding (read)
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   705
import System.IO (IO)
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   706
import qualified System.IO as IO
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   707
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   708
setup :: IO.Handle -> IO ()
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   709
setup h = do
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   710
  IO.hSetEncoding h IO.utf8
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   711
  IO.hSetNewlineMode h IO.noNewlineTranslation
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   712
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   713
read :: IO.FilePath -> IO String
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   714
read path =
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   715
  IO.withFile path IO.ReadMode (\h ->
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   716
    do setup h; IO.hGetContents h >>= \s -> length s `seq` return s)
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   717
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   718
write :: IO.FilePath -> String -> IO ()
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   719
write path s =
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   720
  IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s)
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   721
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   722
append :: IO.FilePath -> String -> IO ()
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   723
append path s =
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   724
  IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   725
\<close>
30f6e8d2cd96 more Haskell operations;
wenzelm
parents: 69248
diff changeset
   726
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   727
generate_file "Isabelle/XML.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   728
{-  Title:      Isabelle/XML.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   729
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   730
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   731
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   732
Untyped XML trees and representation of ML values.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   733
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   734
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   735
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   736
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   737
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   738
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   739
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   740
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   741
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   742
import Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   743
import qualified Isabelle.Properties as Properties
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   744
import qualified Isabelle.Markup as Markup
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   745
import qualified Isabelle.Buffer as Buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   746
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   747
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   748
{- types -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   749
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   750
type Attributes = Properties.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   751
type Body = [Tree]
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   752
data Tree = Elem (Markup.T, Body) | Text String
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   753
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   754
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   755
{- wrapped elements -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   756
69482
186b03abb764 tuned signature;
wenzelm
parents: 69480
diff changeset
   757
wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
69236
wenzelm
parents: 69234
diff changeset
   758
wrap_elem (((a, atts), body1), body2) =
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   759
  Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   760
69482
186b03abb764 tuned signature;
wenzelm
parents: 69480
diff changeset
   761
unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
69236
wenzelm
parents: 69234
diff changeset
   762
unwrap_elem
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   763
  (Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)) =
69236
wenzelm
parents: 69234
diff changeset
   764
  Just (((a, atts), body1), body2)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   765
unwrap_elem _ = Nothing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   766
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   767
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   768
{- text content -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   769
69482
186b03abb764 tuned signature;
wenzelm
parents: 69480
diff changeset
   770
add_content :: Tree -> Buffer.T -> Buffer.T
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   771
add_content tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   772
  case unwrap_elem tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   773
    Just (_, ts) -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   774
    Nothing ->
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   775
      case tree of
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   776
        Elem (_, ts) -> fold add_content ts
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   777
        Text s -> Buffer.add s
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   778
69482
186b03abb764 tuned signature;
wenzelm
parents: 69480
diff changeset
   779
content_of :: Body -> String
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   780
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   781
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   782
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   783
{- string representation -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   784
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   785
encode '<' = "&lt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   786
encode '>' = "&gt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   787
encode '&' = "&amp;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   788
encode '\'' = "&apos;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   789
encode '\"' = "&quot;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   790
encode c = [c]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   791
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   792
instance Show Tree where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   793
  show tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   794
    Buffer.empty |> show_tree tree |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   795
    where
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   796
      show_tree (Elem ((name, atts), [])) =
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   797
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   798
      show_tree (Elem ((name, atts), ts)) =
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   799
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   800
        fold show_tree ts #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   801
        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   802
      show_tree (Text s) = Buffer.add (show_text s)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   803
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   804
      show_elem name atts =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   805
        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   806
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   807
      show_text = concatMap encode
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   808
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   809
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   810
generate_file "Isabelle/XML/Encode.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   811
{-  Title:      Isabelle/XML/Encode.hs
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   812
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   813
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   814
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   815
XML as data representation language.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   816
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   817
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   818
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   819
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   820
module Isabelle.XML.Encode (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   821
  A, T, V,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   822
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   823
  int_atom, bool_atom, unit_atom,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   824
69287
0fde0dca6744 proper export;
wenzelm
parents: 69280
diff changeset
   825
  tree, properties, string, int, bool, unit, pair, triple, list, variant
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   826
)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   827
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   828
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   829
import Isabelle.Library
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   830
import qualified Isabelle.Value as Value
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   831
import qualified Isabelle.Properties as Properties
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   832
import qualified Isabelle.XML as XML
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   833
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   834
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   835
type A a = a -> String
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   836
type T a = a -> XML.Body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   837
type V a = a -> Maybe ([String], XML.Body)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   838
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   839
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   840
-- atomic values
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   841
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   842
int_atom :: A Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   843
int_atom = Value.print_int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   844
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   845
bool_atom :: A Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   846
bool_atom False = "0"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   847
bool_atom True = "1"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   848
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   849
unit_atom :: A ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   850
unit_atom () = ""
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   851
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   852
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   853
-- structural nodes
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   854
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   855
node ts = XML.Elem ((":", []), ts)
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   856
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   857
vector = map_index (\(i, x) -> (int_atom i, x))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   858
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   859
tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   860
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   861
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   862
-- representation of standard types
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   863
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   864
tree :: T XML.Tree
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   865
tree t = [t]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   866
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   867
properties :: T Properties.T
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   868
properties props = [XML.Elem ((":", props), [])]
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   869
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   870
string :: T String
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   871
string "" = []
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   872
string s = [XML.Text s]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   873
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   874
int :: T Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   875
int = string . int_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   876
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   877
bool :: T Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   878
bool = string . bool_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   879
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   880
unit :: T ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   881
unit = string . unit_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   882
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   883
pair :: T a -> T b -> T (a, b)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   884
pair f g (x, y) = [node (f x), node (g y)]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   885
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   886
triple :: T a -> T b -> T c -> T (a, b, c)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   887
triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   888
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   889
list :: T a -> T [a]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   890
list f xs = map (node . f) xs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   891
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   892
variant :: [V a] -> T a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   893
variant fs x = [tagged (the (get_index (\f -> f x) fs))]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   894
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   895
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
   896
generate_file "Isabelle/XML/Decode.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
   897
{-  Title:      Isabelle/XML/Decode.hs
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   898
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   899
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   900
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   901
XML as data representation language.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   902
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
   903
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   904
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   905
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   906
module Isabelle.XML.Decode (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   907
  A, T, V,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   908
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   909
  int_atom, bool_atom, unit_atom,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   910
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   911
  tree, properties, string, init, bool, unit, pair, triple, list, variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   912
)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   913
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   914
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   915
import Data.List ((!!))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   916
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   917
import Isabelle.Library
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   918
import qualified Isabelle.Value as Value
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   919
import qualified Isabelle.Properties as Properties
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   920
import qualified Isabelle.XML as XML
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   921
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   922
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   923
type A a = String -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   924
type T a = XML.Body -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   925
type V a = ([String], XML.Body) -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   926
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   927
err_atom = error "Malformed XML atom"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   928
err_body = error "Malformed XML body"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   929
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   930
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   931
{- atomic values -}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   932
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   933
int_atom :: A Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   934
int_atom s =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   935
  case Value.parse_int s of
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   936
    Just i -> i
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   937
    Nothing -> err_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   938
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   939
bool_atom :: A Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   940
bool_atom "0" = False
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   941
bool_atom "1" = True
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   942
bool_atom _ = err_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   943
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   944
unit_atom :: A ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   945
unit_atom "" = ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   946
unit_atom _ = err_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   947
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   948
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   949
{- structural nodes -}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   950
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   951
node (XML.Elem ((":", []), ts)) = ts
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   952
node _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   953
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   954
vector atts =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   955
  map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   956
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   957
tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   958
tagged _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   959
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   960
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   961
{- representation of standard types -}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   962
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   963
tree :: T XML.Tree
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   964
tree [t] = t
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   965
tree _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   966
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   967
properties :: T Properties.T
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
   968
properties [XML.Elem ((":", props), [])] = props
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   969
properties _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   970
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   971
string :: T String
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   972
string [] = ""
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   973
string [XML.Text s] = s
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   974
string _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   975
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   976
int :: T Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   977
int = int_atom . string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   978
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   979
bool :: T Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   980
bool = bool_atom . string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   981
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   982
unit :: T ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   983
unit = unit_atom . string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   984
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   985
pair :: T a -> T b -> T (a, b)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   986
pair f g [t1, t2] = (f (node t1), g (node t2))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   987
pair _ _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   988
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   989
triple :: T a -> T b -> T c -> T (a, b, c)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   990
triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   991
triple _ _ _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   992
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   993
list :: T a -> T [a]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   994
list f ts = map (f . node) ts
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   995
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   996
option :: T a -> T (Maybe a)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   997
option _ [] = Nothing
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   998
option f [t] = Just (f (node t))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   999
option _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1000
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1001
variant :: [V a] -> T a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1002
variant fs [t] = (fs !! tag) (xs, ts)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1003
  where (tag, (xs, ts)) = tagged t
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1004
variant _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1005
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1006
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
  1007
generate_file "Isabelle/YXML.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
  1008
{-  Title:      Isabelle/YXML.hs
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1009
    Author:     Makarius
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1010
    LICENSE:    BSD 3-clause (Isabelle)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1011
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1012
Efficient text representation of XML trees.  Suitable for direct
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1013
inlining into plain text.
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1014
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1015
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1016
-}
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1017
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1018
module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1019
  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1020
where
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1021
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1022
import qualified Data.Char as Char
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1023
import qualified Data.List as List
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1024
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1025
import Isabelle.Library
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1026
import qualified Isabelle.Markup as Markup
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1027
import qualified Isabelle.XML as XML
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1028
import qualified Isabelle.Buffer as Buffer
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1029
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1030
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1031
{- markers -}
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1032
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1033
charX, charY :: Char
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1034
charX = Char.chr 5
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1035
charY = Char.chr 6
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1036
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1037
strX, strY, strXY, strXYX :: String
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1038
strX = [charX]
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1039
strY = [charY]
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1040
strXY = strX ++ strY
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1041
strXYX = strXY ++ strX
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1042
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1043
detect :: String -> Bool
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1044
detect = any (\c -> c == charX || c == charY)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1045
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1046
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1047
{- output -}
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1048
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1049
output_markup :: Markup.T -> Markup.Output
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1050
output_markup markup@(name, atts) =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1051
  if Markup.is_empty markup then Markup.no_output
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1052
  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1053
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1054
buffer_attrib (a, x) =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1055
  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1056
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1057
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1058
buffer_body = fold buffer
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1059
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1060
buffer :: XML.Tree -> Buffer.T -> Buffer.T
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
  1061
buffer (XML.Elem ((name, atts), ts)) =
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1062
  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1063
  buffer_body ts #>
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1064
  Buffer.add strXYX
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1065
buffer (XML.Text s) = Buffer.add s
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1066
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1067
string_of_body :: XML.Body -> String
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1068
string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1069
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1070
string_of :: XML.Tree -> String
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1071
string_of = string_of_body . single
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1072
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1073
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1074
{- parse -}
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1075
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1076
-- split: fields or non-empty tokens
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1077
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1078
split :: Bool -> Char -> String -> [String]
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1079
split _ _ [] = []
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1080
split fields sep str = splitting str
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1081
  where
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1082
    splitting rest =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1083
      case span (/= sep) rest of
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1084
        (_, []) -> cons rest []
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1085
        (prfx, _ : rest') -> cons prfx (splitting rest')
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1086
    cons item = if fields || not (null item) then (:) item else id
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1087
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1088
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1089
-- structural errors
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1090
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1091
err msg = error ("Malformed YXML: " ++ msg)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1092
err_attribute = err "bad attribute"
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1093
err_element = err "bad element"
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1094
err_unbalanced "" = err "unbalanced element"
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1095
err_unbalanced name = err ("unbalanced element " ++ quote name)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1096
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1097
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1098
-- stack operations
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1099
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1100
add x ((elem, body) : pending) = (elem, x : body) : pending
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1101
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1102
push "" _ _ = err_element
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1103
push name atts pending = ((name, atts), []) : pending
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1104
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1105
pop ((("", _), _) : _) = err_unbalanced ""
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
  1106
pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
69288
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1107
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1108
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1109
-- parsing
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1110
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1111
parse_attrib s =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1112
  case List.elemIndex '=' s of
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1113
    Just i | i > 0 -> (take i s, drop (i + 1) s)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1114
    _ -> err_attribute
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1115
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1116
parse_chunk ["", ""] = pop
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1117
parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1118
parse_chunk txts = fold (add . XML.Text) txts
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1119
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1120
parse_body :: String -> XML.Body
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1121
parse_body source =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1122
  case fold parse_chunk chunks [(("", []), [])] of
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1123
    [(("", _), result)] -> reverse result
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1124
    ((name, _), _) : _ -> err_unbalanced name
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1125
  where chunks = split False charX source |> map (split True charY)
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1126
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1127
parse :: String -> XML.Tree
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1128
parse source =
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1129
  case parse_body source of
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1130
    [result] -> result
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1131
    [] -> XML.Text ""
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1132
    _ -> err "multiple results"
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1133
\<close>
4c3704ecb0e6 more Haskell operations;
wenzelm
parents: 69287
diff changeset
  1134
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
  1135
generate_file "Isabelle/Pretty.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
  1136
{-  Title:      Isabelle/Pretty.hs
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1137
    Author:     Makarius
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1138
    LICENSE:    BSD 3-clause (Isabelle)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1139
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1140
Generic pretty printing module.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
  1141
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
  1142
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1143
-}
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1144
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1145
module Isabelle.Pretty (
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1146
  T, symbolic, formatted, unformatted,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1147
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1148
  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1149
  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1150
  commas, enclose, enum, list, str_list, big_list)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1151
where
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1152
69453
dcea1fffbfe6 more Haskell operations;
wenzelm
parents: 69452
diff changeset
  1153
import Isabelle.Library hiding (quote, commas)
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1154
import qualified Data.List as List
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1155
import qualified Isabelle.Buffer as Buffer
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1156
import qualified Isabelle.Markup as Markup
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1157
import qualified Isabelle.XML as XML
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1158
import qualified Isabelle.YXML as YXML
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1159
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1160
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1161
data T =
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1162
    Block Markup.T Bool Int [T]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1163
  | Break Int Int
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1164
  | Str String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1165
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1166
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1167
{- output -}
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1168
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1169
output_spaces n = replicate n ' '
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1170
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1171
symbolic_text "" = []
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1172
symbolic_text s = [XML.Text s]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1173
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1174
symbolic_markup markup body =
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1175
  if Markup.is_empty markup then body
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
  1176
  else [XML.Elem (markup, body)]
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1177
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1178
symbolic :: T -> XML.Body
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1179
symbolic (Block markup consistent indent prts) =
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1180
  concatMap symbolic prts
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1181
  |> symbolic_markup block_markup
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1182
  |> symbolic_markup markup
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1183
  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
69290
fb77612d11eb tuned signature;
wenzelm
parents: 69289
diff changeset
  1184
symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
69248
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1185
symbolic (Str s) = symbolic_text s
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1186
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1187
formatted :: T -> String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1188
formatted = YXML.string_of_body . symbolic
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1189
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1190
unformatted :: T -> String
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1191
unformatted prt = Buffer.empty |> out prt |> Buffer.content
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1192
  where
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1193
    out (Block markup _ _ prts) =
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1194
      let (bg, en) = YXML.output_markup markup
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1195
      in Buffer.add bg #> fold out prts #> Buffer.add en
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1196
    out (Break _ wd) = Buffer.add (output_spaces wd)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1197
    out (Str s) = Buffer.add s
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1198
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1199
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1200
{- derived operations to create formatting expressions -}
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1201
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1202
force_nat n | n < 0 = 0
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1203
force_nat n = n
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1204
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1205
str :: String -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1206
str = Str
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1207
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1208
brk_indent :: Int -> Int -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1209
brk_indent wd ind = Break (force_nat wd) ind
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1210
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1211
brk :: Int -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1212
brk wd = brk_indent wd 0
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1213
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1214
fbrk :: T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1215
fbrk = str "\n"
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1216
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1217
breaks, fbreaks :: [T] -> [T]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1218
breaks = List.intersperse (brk 1)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1219
fbreaks = List.intersperse fbrk
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1220
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1221
blk :: (Int, [T]) -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1222
blk (indent, es) = Block Markup.empty False (force_nat indent) es
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1223
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1224
block :: [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1225
block prts = blk (2, prts)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1226
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1227
strs :: [String] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1228
strs = block . breaks . map str
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1229
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1230
markup :: Markup.T -> [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1231
markup m = Block m False 0
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1232
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1233
mark :: Markup.T -> T -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1234
mark m prt = if m == Markup.empty then prt else markup m [prt]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1235
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1236
mark_str :: (Markup.T, String) -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1237
mark_str (m, s) = mark m (str s)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1238
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1239
marks_str :: ([Markup.T], String) -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1240
marks_str (ms, s) = fold_rev mark ms (str s)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1241
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1242
item :: [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1243
item = markup Markup.item
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1244
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1245
text_fold :: [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1246
text_fold = markup Markup.text_fold
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1247
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1248
keyword1, keyword2 :: String -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1249
keyword1 name = mark_str (Markup.keyword1, name)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1250
keyword2 name = mark_str (Markup.keyword2, name)
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1251
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1252
text :: String -> [T]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1253
text = breaks . map str . words
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1254
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1255
paragraph :: [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1256
paragraph = markup Markup.paragraph
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1257
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1258
para :: String -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1259
para = paragraph . text
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1260
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1261
quote :: T -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1262
quote prt = blk (1, [str "\"", prt, str "\""])
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1263
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1264
cartouche :: T -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1265
cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1266
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1267
separate :: String -> [T] -> [T]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1268
separate sep = List.intercalate [str sep, brk 1] . map single
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1269
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1270
commas :: [T] -> [T]
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1271
commas = separate ","
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1272
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1273
enclose :: String -> String -> [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1274
enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1275
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1276
enum :: String -> String -> String -> [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1277
enum sep lpar rpar = enclose lpar rpar . separate sep
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1278
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1279
list :: String -> String -> [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1280
list = enum ","
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1281
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1282
str_list :: String -> String -> [String] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1283
str_list lpar rpar = list lpar rpar . map str
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1284
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1285
big_list :: String -> [T] -> T
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1286
big_list name prts = block (fbreaks (str name : prts))
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1287
\<close>
9f21381600e3 more Haskell operations;
wenzelm
parents: 69240
diff changeset
  1288
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
  1289
generate_file "Isabelle/Term.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
  1290
{-  Title:      Isabelle/Term.hs
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1291
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1292
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1293
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1294
Lambda terms, types, sorts.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
  1295
e1d01b351724 more formal references;
wenzelm
parents: 69278
diff changeset
  1296
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1297
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1298
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1299
module Isabelle.Term (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1300
  Indexname,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1301
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1302
  Sort, dummyS,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1303
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1304
  Typ(..), dummyT, Term(..))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1305
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1306
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1307
type Indexname = (String, Int)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1308
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1309
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1310
type Sort = [String]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1311
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1312
dummyS :: Sort
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1313
dummyS = [""]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1314
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1315
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1316
data Typ =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1317
    Type (String, [Typ])
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1318
  | TFree (String, Sort)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1319
  | TVar (Indexname, Sort)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1320
  deriving Show
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1321
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1322
dummyT :: Typ
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1323
dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1324
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1325
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1326
data Term =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1327
    Const (String, Typ)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1328
  | Free (String, Typ)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1329
  | Var (Indexname, Typ)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1330
  | Bound Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1331
  | Abs (String, Typ, Term)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1332
  | App (Term, Term)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1333
  deriving Show
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1334
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
  1335
69444
c3c9440cbf9b more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents: 69381
diff changeset
  1336
generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
69445
bff0011cdf42 tuned headers;
wenzelm
parents: 69444
diff changeset
  1337
{-  Title:      Isabelle/Term_XML/Encode.hs