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