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