src/Tools/Haskell/Haskell.thy
author wenzelm
Sat, 03 Nov 2018 19:33:15 +0100
changeset 69225 bf2fecda8383
parent 69222 8365124a86ae
child 69226 68f5dc2275ac
permissions -rw-r--r--
support for Isabelle tools in Haskell;
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
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    30
generate_haskell_file Library.hs =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    31
\<open>{-  Title:      Tools/Haskell/Library.hs
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.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    36
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    37
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    38
module Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    39
  ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    40
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    41
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    42
{- functions -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    43
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    44
(|>) :: a -> (a -> b) -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    45
x |> f = f x
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    46
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    47
(|->) :: (a, b) -> (a -> b -> c) -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    48
(x, y) |-> f = f x y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    49
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    50
(#>) :: (a -> b) -> (b -> c) -> a -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    51
(f #> g) x = x |> f |> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    52
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    53
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    54
(f #-> g) x  = x |> f |-> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    55
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    56
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    57
{- lists -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    58
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    59
fold :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    60
fold _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    61
fold f (x : xs) y = fold f xs (f x y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    62
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    63
fold_rev :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    64
fold_rev _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    65
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
    66
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    67
single :: a -> [a]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    68
single x = [x]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    69
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    70
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    71
{- strings -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    72
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    73
quote :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    74
quote s = "\"" ++ s ++ "\""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    75
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    76
trim_line :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    77
trim_line line =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    78
  case reverse line of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    79
    '\n' : '\r' : rest -> reverse rest
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    80
    '\n' : rest -> reverse rest
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    81
    _ -> line
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    82
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    83
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    84
generate_haskell_file Buffer.hs =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    85
\<open>{-  Title:      Tools/Haskell/Buffer.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    86
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    87
    LICENSE:    BSD 3-clause (Isabelle)
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
Efficient text buffers.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    90
-}
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
    91
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    92
module Isabelle.Buffer (T, empty, add, content)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    93
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    94
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    95
newtype T = Buffer [String]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    96
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    97
empty :: T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    98
empty = Buffer []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    99
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   100
add :: String -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   101
add "" buf = buf
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   102
add x (Buffer xs) = Buffer (x : xs)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   103
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   104
content :: T -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   105
content (Buffer xs) = concat (reverse xs)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   106
\<close>
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
generate_haskell_file Properties.hs =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   109
\<open>{-  Title:      Tools/Haskell/Properties.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   110
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   111
    LICENSE:    BSD 3-clause (Isabelle)
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
Property lists.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   114
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   115
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   116
module Isabelle.Properties (Entry, T, defined, get, put, remove)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   117
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   118
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   119
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   120
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   121
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   122
type Entry = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   123
type T = [Entry]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   124
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   125
defined :: T -> String -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   126
defined props name = any (\(a, _) -> a == name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   127
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   128
get :: T -> String -> Maybe String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   129
get props name = List.lookup name props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   130
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   131
put :: Entry -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   132
put entry props = entry : remove (fst entry) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   133
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   134
remove :: String -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   135
remove name props =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   136
  if defined props name then filter (\(a, _) -> a /= name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   137
  else props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   138
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   139
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   140
generate_haskell_file Markup.hs =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   141
\<open>{-  Title:      Haskell/Tools/Markup.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   142
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   143
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   144
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   145
Quasi-abstract markup elements.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   146
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   147
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   148
module Isabelle.Markup (T, empty, is_empty, Output, no_output)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   149
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   150
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   151
import qualified Isabelle.Properties as Properties
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   152
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   153
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   154
type T = (String, Properties.T)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   155
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   156
empty :: T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   157
empty = ("", [])
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   158
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   159
is_empty :: T -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   160
is_empty ("", _) = True
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   161
is_empty _ = False
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   162
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   163
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   164
type Output = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   165
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   166
no_output :: Output
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   167
no_output = ("", "")
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   168
\<close>
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   169
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   170
generate_haskell_file XML.hs =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   171
\<open>{-  Title:      Tools/Haskell/XML.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   172
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   173
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   174
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   175
Untyped XML trees and representation of ML values.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   176
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   177
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   178
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   179
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   180
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   181
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   182
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   183
import Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   184
import qualified Isabelle.Properties as Properties
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   185
import qualified Isabelle.Markup as Markup
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   186
import qualified Isabelle.Buffer as Buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   187
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   188
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   189
{- types -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   190
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   191
type Attributes = Properties.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   192
type Body = [Tree]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   193
data Tree = Elem Markup.T Body | Text String
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
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   196
{- wrapped elements -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   197
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   198
xml_elemN = "xml_elem";
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   199
xml_nameN = "xml_name";
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   200
xml_bodyN = "xml_body";
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   201
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   202
wrap_elem (((a, atts), body1), body2) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   203
  Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   204
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   205
unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   206
  if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts'
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   207
  then Just (((a, atts), body1), body2) else Nothing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   208
unwrap_elem _ = Nothing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   209
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   210
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   211
{- text content -}
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
add_content tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   214
  case unwrap_elem tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   215
    Just (_, ts) -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   216
    Nothing ->
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   217
      case tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   218
        Elem _ ts -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   219
        Text s -> Buffer.add s
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   220
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   221
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   222
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   223
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   224
{- string representation -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   226
encode '<' = "&lt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   227
encode '>' = "&gt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   228
encode '&' = "&amp;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   229
encode '\'' = "&apos;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   230
encode '\"' = "&quot;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   231
encode c = [c]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   232
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   233
instance Show Tree where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   234
  show tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   235
    Buffer.empty |> show_tree tree |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   236
    where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   237
      show_tree (Elem (name, atts) []) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   238
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   239
      show_tree (Elem (name, atts) ts) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   240
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   241
        fold show_tree ts #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   242
        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   243
      show_tree (Text s) = Buffer.add (show_text s)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   244
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   245
      show_elem name atts =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   246
        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   247
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   248
      show_text = concatMap encode
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   249
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   250
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   251
generate_haskell_file YXML.hs =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   252
\<open>{-  Title:      Tools/Haskell/YXML.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   253
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   254
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   255
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   256
Efficient text representation of XML trees.  Suitable for direct
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   257
inlining into plain text.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   258
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   259
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   260
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   261
module Isabelle.YXML (charX, charY, strX, strY, detect,
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   262
  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   263
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   264
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   265
import qualified Data.Char as Char
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   266
import qualified Data.List as List
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   267
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   268
import Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   269
import qualified Isabelle.Markup as Markup
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   270
import qualified Isabelle.XML as XML
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   271
import qualified Isabelle.Buffer as Buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   272
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   273
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   274
{- markers -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   275
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   276
charX, charY :: Char
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   277
charX = Char.chr 5
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   278
charY = Char.chr 6
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   279
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   280
strX, strY, strXY, strXYX :: String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   281
strX = [charX]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   282
strY = [charY]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   283
strXY = strX ++ strY
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   284
strXYX = strXY ++ strX
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   285
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   286
detect :: String -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   287
detect = any (\c -> c == charX || c == charY)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   288
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   289
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   290
{- output -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   291
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   292
buffer_attrib (a, x) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   293
  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   294
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   295
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   296
buffer_body = fold buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   297
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   298
buffer :: XML.Tree -> Buffer.T -> Buffer.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   299
buffer (XML.Elem (name, atts) ts) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   300
  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   301
  buffer_body ts #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   302
  Buffer.add strXYX
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   303
buffer (XML.Text s) = Buffer.add s
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   304
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   305
string_of_body :: XML.Body -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   306
string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   307
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   308
string_of :: XML.Tree -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   309
string_of = string_of_body . single
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   310
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   311
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   312
{- parse -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   313
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   314
-- split: fields or non-empty tokens
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   315
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   316
split :: Bool -> Char -> String -> [String]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   317
split _ _ [] = []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   318
split fields sep str = splitting str
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   319
  where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   320
    splitting rest =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   321
      case span (/= sep) rest of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   322
        (_, []) -> cons rest []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   323
        (prfx, _ : rest') -> cons prfx (splitting rest')
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   324
    cons item = if fields || not (null item) then (:) item else id
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   325
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   326
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   327
-- structural errors
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   328
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   329
err msg = error ("Malformed YXML: " ++ msg)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   330
err_attribute = err "bad attribute"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   331
err_element = err "bad element"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   332
err_unbalanced "" = err "unbalanced element"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   333
err_unbalanced name = err ("unbalanced element " ++ quote name)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   334
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   335
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   336
-- stack operations
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   337
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   338
add x ((elem, body) : pending) = (elem, x : body) : pending
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   339
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   340
push "" _ _ = err_element
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   341
push name atts pending = ((name, atts), []) : pending
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   342
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   343
pop ((("", _), _) : _) = err_unbalanced ""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   344
pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   345
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   346
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   347
-- parsing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   348
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   349
parse_attrib s =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   350
  case List.elemIndex '=' s of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   351
    Just i | i > 0 -> (take i s, drop (i + 1) s)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   352
    _ -> err_attribute
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   353
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   354
parse_chunk ["", ""] = pop
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   355
parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   356
parse_chunk txts = fold (add . XML.Text) txts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   357
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   358
parse_body :: String -> XML.Body
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   359
parse_body source =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   360
  case fold parse_chunk chunks [(("", []), [])] of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   361
    [(("", _), result)] -> reverse result
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   362
    ((name, _), _) : _ -> err_unbalanced name
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   363
  where chunks = split False charX source |> map (split True charY)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   364
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   365
parse :: String -> XML.Tree
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   366
parse source =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   367
  case parse_body source of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   368
    [result] -> result
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   369
    [] -> XML.Text ""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   370
    _ -> err "multiple results"
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   371
\<close>
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   372
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   373
end