src/Tools/Haskell/Haskell.thy
author wenzelm
Sun Mar 24 17:53:46 2019 +0100 (3 months ago)
changeset 69968 1a400b14fd3a
parent 69794 a19fdf64726c
child 70047 96fe857a7a6f
permissions -rw-r--r--
clarified spell-checking (see also 30233285270a);
wenzelm@69222
     1
(*  Title:      Tools/Haskell/Haskell.thy
wenzelm@69222
     2
    Author:     Makarius
wenzelm@69225
     3
wenzelm@69225
     4
Support for Isabelle tools in Haskell.
wenzelm@69222
     5
*)
wenzelm@69222
     6
wenzelm@69222
     7
theory Haskell
wenzelm@69222
     8
  imports Pure
wenzelm@69222
     9
begin
wenzelm@69222
    10
wenzelm@69490
    11
generate_file "Isabelle/Symbol.hs" = \<open>
wenzelm@69490
    12
{-  Title:      Isabelle/Symbols.hs
wenzelm@69490
    13
    Author:     Makarius
wenzelm@69490
    14
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69490
    15
wenzelm@69490
    16
Isabelle text symbols.
wenzelm@69490
    17
-}
wenzelm@69490
    18
wenzelm@69490
    19
module Isabelle.Symbol where
wenzelm@69490
    20
wenzelm@69490
    21
{- ASCII characters -}
wenzelm@69490
    22
wenzelm@69490
    23
is_ascii_letter :: Char -> Bool
wenzelm@69490
    24
is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
wenzelm@69490
    25
wenzelm@69490
    26
is_ascii_digit :: Char -> Bool
wenzelm@69490
    27
is_ascii_digit c = '0' <= c && c <= '9'
wenzelm@69490
    28
wenzelm@69490
    29
is_ascii_hex :: Char -> Bool
wenzelm@69490
    30
is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
wenzelm@69490
    31
wenzelm@69490
    32
is_ascii_quasi :: Char -> Bool
wenzelm@69490
    33
is_ascii_quasi c = c == '_' || c == '\''
wenzelm@69490
    34
wenzelm@69490
    35
is_ascii_blank :: Char -> Bool
wenzelm@69490
    36
is_ascii_blank c = c `elem` " \t\n\11\f\r"
wenzelm@69490
    37
wenzelm@69490
    38
is_ascii_line_terminator :: Char -> Bool
wenzelm@69490
    39
is_ascii_line_terminator c = c == '\r' || c == '\n'
wenzelm@69490
    40
wenzelm@69490
    41
is_ascii_letdig :: Char -> Bool
wenzelm@69490
    42
is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
wenzelm@69490
    43
wenzelm@69490
    44
is_ascii_identifier :: String -> Bool
wenzelm@69490
    45
is_ascii_identifier s =
wenzelm@69490
    46
  not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
wenzelm@69490
    47
\<close>
wenzelm@69490
    48
wenzelm@69444
    49
generate_file "Isabelle/Library.hs" = \<open>
wenzelm@69445
    50
{-  Title:      Isabelle/Library.hs
wenzelm@69225
    51
    Author:     Makarius
wenzelm@69225
    52
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
    53
wenzelm@69225
    54
Basic library of Isabelle idioms.
wenzelm@69280
    55
wenzelm@69280
    56
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>, \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
wenzelm@69225
    57
-}
wenzelm@69225
    58
wenzelm@69240
    59
module Isabelle.Library (
wenzelm@69240
    60
  (|>), (|->), (#>), (#->),
wenzelm@69240
    61
wenzelm@69240
    62
  the, the_default,
wenzelm@69240
    63
wenzelm@69240
    64
  fold, fold_rev, single, map_index, get_index,
wenzelm@69240
    65
wenzelm@69477
    66
  proper_string, quote, space_implode, commas, commas_quote, cat_lines,
wenzelm@69453
    67
  space_explode, split_lines, trim_line, clean_name)
wenzelm@69225
    68
where
wenzelm@69225
    69
wenzelm@69234
    70
import Data.Maybe
wenzelm@69453
    71
import qualified Data.List as List
wenzelm@69453
    72
import qualified Data.List.Split as Split
wenzelm@69491
    73
import qualified Isabelle.Symbol as Symbol
wenzelm@69234
    74
wenzelm@69234
    75
wenzelm@69225
    76
{- functions -}
wenzelm@69225
    77
wenzelm@69225
    78
(|>) :: a -> (a -> b) -> b
wenzelm@69225
    79
x |> f = f x
wenzelm@69225
    80
wenzelm@69225
    81
(|->) :: (a, b) -> (a -> b -> c) -> c
wenzelm@69225
    82
(x, y) |-> f = f x y
wenzelm@69225
    83
wenzelm@69225
    84
(#>) :: (a -> b) -> (b -> c) -> a -> c
wenzelm@69225
    85
(f #> g) x = x |> f |> g
wenzelm@69225
    86
wenzelm@69225
    87
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
wenzelm@69225
    88
(f #-> g) x  = x |> f |-> g
wenzelm@69225
    89
wenzelm@69225
    90
wenzelm@69234
    91
{- options -}
wenzelm@69234
    92
wenzelm@69240
    93
the :: Maybe a -> a
wenzelm@69240
    94
the (Just x) = x
wenzelm@69240
    95
the Nothing = error "the Nothing"
wenzelm@69240
    96
wenzelm@69234
    97
the_default :: a -> Maybe a -> a
wenzelm@69234
    98
the_default x Nothing = x
wenzelm@69234
    99
the_default _ (Just y) = y
wenzelm@69234
   100
wenzelm@69234
   101
wenzelm@69225
   102
{- lists -}
wenzelm@69225
   103
wenzelm@69225
   104
fold :: (a -> b -> b) -> [a] -> b -> b
wenzelm@69225
   105
fold _ [] y = y
wenzelm@69225
   106
fold f (x : xs) y = fold f xs (f x y)
wenzelm@69225
   107
wenzelm@69225
   108
fold_rev :: (a -> b -> b) -> [a] -> b -> b
wenzelm@69225
   109
fold_rev _ [] y = y
wenzelm@69225
   110
fold_rev f (x : xs) y = f x (fold_rev f xs y)
wenzelm@69225
   111
wenzelm@69225
   112
single :: a -> [a]
wenzelm@69225
   113
single x = [x]
wenzelm@69225
   114
wenzelm@69240
   115
map_index :: ((Int, a) -> b) -> [a] -> [b]
wenzelm@69240
   116
map_index f = map_aux 0
wenzelm@69240
   117
  where
wenzelm@69240
   118
    map_aux _ [] = []
wenzelm@69240
   119
    map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
wenzelm@69240
   120
wenzelm@69240
   121
get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
wenzelm@69240
   122
get_index f = get_aux 0
wenzelm@69240
   123
  where
wenzelm@69240
   124
    get_aux _ [] = Nothing
wenzelm@69240
   125
    get_aux i (x : xs) =
wenzelm@69240
   126
      case f x of
wenzelm@69240
   127
        Nothing -> get_aux (i + 1) xs
wenzelm@69240
   128
        Just y -> Just (i, y)
wenzelm@69240
   129
wenzelm@69225
   130
wenzelm@69225
   131
{- strings -}
wenzelm@69225
   132
wenzelm@69477
   133
proper_string :: String -> Maybe String
wenzelm@69477
   134
proper_string s = if null s then Nothing else Just s
wenzelm@69477
   135
wenzelm@69225
   136
quote :: String -> String
wenzelm@69225
   137
quote s = "\"" ++ s ++ "\""
wenzelm@69225
   138
wenzelm@69453
   139
space_implode :: String -> [String] -> String
wenzelm@69453
   140
space_implode = List.intercalate
wenzelm@69453
   141
wenzelm@69453
   142
commas, commas_quote :: [String] -> String
wenzelm@69453
   143
commas = space_implode ", "
wenzelm@69453
   144
commas_quote = commas . map quote
wenzelm@69453
   145
wenzelm@69453
   146
cat_lines :: [String] -> String
wenzelm@69453
   147
cat_lines = space_implode "\n"
wenzelm@69453
   148
wenzelm@69453
   149
wenzelm@69453
   150
space_explode :: Char -> String -> [String]
wenzelm@69453
   151
space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
wenzelm@69453
   152
wenzelm@69453
   153
split_lines :: String -> [String]
wenzelm@69453
   154
split_lines = space_explode '\n'
wenzelm@69453
   155
wenzelm@69225
   156
trim_line :: String -> String
wenzelm@69225
   157
trim_line line =
wenzelm@69491
   158
  if not (null line) && Symbol.is_ascii_line_terminator (last line) then
wenzelm@69486
   159
    case reverse line of
wenzelm@69486
   160
      '\n' : '\r' : rest -> reverse rest
wenzelm@69486
   161
      '\r' : rest -> reverse rest
wenzelm@69486
   162
      '\n' : rest -> reverse rest
wenzelm@69486
   163
      _ -> line
wenzelm@69486
   164
  else line
wenzelm@69288
   165
wenzelm@69288
   166
clean_name :: String -> String
wenzelm@69288
   167
clean_name = reverse #> dropWhile (== '_') #> reverse
wenzelm@69225
   168
\<close>
wenzelm@69225
   169
wenzelm@69444
   170
generate_file "Isabelle/Value.hs" = \<open>
wenzelm@69233
   171
{-  Title:      Haskell/Tools/Value.hs
wenzelm@69233
   172
    Author:     Makarius
wenzelm@69233
   173
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69233
   174
wenzelm@69233
   175
Plain values, represented as string.
wenzelm@69280
   176
wenzelm@69280
   177
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
wenzelm@69233
   178
-}
wenzelm@69233
   179
wenzelm@69233
   180
module Isabelle.Value
wenzelm@69452
   181
  (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
wenzelm@69233
   182
where
wenzelm@69233
   183
wenzelm@69233
   184
import Data.Maybe
wenzelm@69233
   185
import qualified Data.List as List
wenzelm@69233
   186
import qualified Text.Read as Read
wenzelm@69233
   187
wenzelm@69233
   188
wenzelm@69233
   189
{- bool -}
wenzelm@69233
   190
wenzelm@69233
   191
print_bool :: Bool -> String
wenzelm@69233
   192
print_bool True = "true"
wenzelm@69233
   193
print_bool False = "false"
wenzelm@69233
   194
wenzelm@69233
   195
parse_bool :: String -> Maybe Bool
wenzelm@69233
   196
parse_bool "true" = Just True
wenzelm@69233
   197
parse_bool "false" = Just False
wenzelm@69233
   198
parse_bool _ = Nothing
wenzelm@69233
   199
wenzelm@69233
   200
wenzelm@69452
   201
{- nat -}
wenzelm@69452
   202
wenzelm@69452
   203
parse_nat :: String -> Maybe Int
wenzelm@69452
   204
parse_nat s =
wenzelm@69452
   205
  case Read.readMaybe s of
wenzelm@69452
   206
    Just n | n >= 0 -> Just n
wenzelm@69452
   207
    _ -> Nothing
wenzelm@69452
   208
wenzelm@69452
   209
wenzelm@69233
   210
{- int -}
wenzelm@69233
   211
wenzelm@69233
   212
print_int :: Int -> String
wenzelm@69233
   213
print_int = show
wenzelm@69233
   214
wenzelm@69233
   215
parse_int :: String -> Maybe Int
wenzelm@69233
   216
parse_int = Read.readMaybe
wenzelm@69233
   217
wenzelm@69233
   218
wenzelm@69233
   219
{- real -}
wenzelm@69233
   220
wenzelm@69233
   221
print_real :: Double -> String
wenzelm@69233
   222
print_real x =
wenzelm@69233
   223
  let s = show x in
wenzelm@69233
   224
    case span (/= '.') s of
wenzelm@69233
   225
      (a, '.' : b) | List.all (== '0') b -> a
wenzelm@69233
   226
      _ -> s
wenzelm@69233
   227
wenzelm@69233
   228
parse_real :: String -> Maybe Double
wenzelm@69233
   229
parse_real = Read.readMaybe
wenzelm@69233
   230
\<close>
wenzelm@69233
   231
wenzelm@69444
   232
generate_file "Isabelle/Buffer.hs" = \<open>
wenzelm@69445
   233
{-  Title:      Isabelle/Buffer.hs
wenzelm@69225
   234
    Author:     Makarius
wenzelm@69225
   235
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   236
wenzelm@69225
   237
Efficient text buffers.
wenzelm@69280
   238
wenzelm@69280
   239
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
wenzelm@69225
   240
-}
wenzelm@69222
   241
wenzelm@69225
   242
module Isabelle.Buffer (T, empty, add, content)
wenzelm@69225
   243
where
wenzelm@69225
   244
wenzelm@69474
   245
import Isabelle.Library
wenzelm@69474
   246
wenzelm@69474
   247
wenzelm@69474
   248
newtype T = Buffer [Char]
wenzelm@69225
   249
wenzelm@69225
   250
empty :: T
wenzelm@69225
   251
empty = Buffer []
wenzelm@69225
   252
wenzelm@69225
   253
add :: String -> T -> T
wenzelm@69474
   254
add s (Buffer cs) = Buffer (fold (:) s cs)
wenzelm@69225
   255
wenzelm@69225
   256
content :: T -> String
wenzelm@69474
   257
content (Buffer cs) = reverse cs
wenzelm@69225
   258
\<close>
wenzelm@69225
   259
wenzelm@69444
   260
generate_file "Isabelle/Properties.hs" = \<open>
wenzelm@69445
   261
{-  Title:      Isabelle/Properties.hs
wenzelm@69225
   262
    Author:     Makarius
wenzelm@69225
   263
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   264
wenzelm@69225
   265
Property lists.
wenzelm@69280
   266
wenzelm@69280
   267
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
wenzelm@69225
   268
-}
wenzelm@69225
   269
wenzelm@69477
   270
module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
wenzelm@69225
   271
where
wenzelm@69225
   272
wenzelm@69225
   273
import qualified Data.List as List
wenzelm@69225
   274
wenzelm@69225
   275
wenzelm@69225
   276
type Entry = (String, String)
wenzelm@69225
   277
type T = [Entry]
wenzelm@69225
   278
wenzelm@69225
   279
defined :: T -> String -> Bool
wenzelm@69225
   280
defined props name = any (\(a, _) -> a == name) props
wenzelm@69225
   281
wenzelm@69225
   282
get :: T -> String -> Maybe String
wenzelm@69225
   283
get props name = List.lookup name props
wenzelm@69225
   284
wenzelm@69477
   285
get_value :: (String -> Maybe a) -> T -> String -> Maybe a
wenzelm@69477
   286
get_value parse props name =
wenzelm@69477
   287
  case get props name of
wenzelm@69477
   288
    Nothing -> Nothing
wenzelm@69477
   289
    Just s -> parse s
wenzelm@69477
   290
wenzelm@69225
   291
put :: Entry -> T -> T
wenzelm@69225
   292
put entry props = entry : remove (fst entry) props
wenzelm@69225
   293
wenzelm@69225
   294
remove :: String -> T -> T
wenzelm@69225
   295
remove name props =
wenzelm@69225
   296
  if defined props name then filter (\(a, _) -> a /= name) props
wenzelm@69225
   297
  else props
wenzelm@69225
   298
\<close>
wenzelm@69225
   299
wenzelm@69444
   300
generate_file "Isabelle/Markup.hs" = \<open>
wenzelm@69226
   301
{-  Title:      Haskell/Tools/Markup.hs
wenzelm@69225
   302
    Author:     Makarius
wenzelm@69225
   303
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   304
wenzelm@69225
   305
Quasi-abstract markup elements.
wenzelm@69280
   306
wenzelm@69280
   307
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
wenzelm@69225
   308
-}
wenzelm@69225
   309
wenzelm@69234
   310
module Isabelle.Markup (
wenzelm@69234
   311
  T, empty, is_empty, properties,
wenzelm@69234
   312
wenzelm@69234
   313
  nameN, name, xnameN, xname, kindN,
wenzelm@69234
   314
wenzelm@69315
   315
  bindingN, binding, entityN, entity, defN, refN,
wenzelm@69315
   316
wenzelm@69288
   317
  completionN, completion, no_completionN, no_completion,
wenzelm@69288
   318
wenzelm@69234
   319
  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
wenzelm@69234
   320
wenzelm@69291
   321
  expressionN, expression,
wenzelm@69291
   322
wenzelm@69291
   323
  citationN, citation,
wenzelm@69291
   324
wenzelm@69291
   325
  pathN, urlN, docN,
wenzelm@69291
   326
wenzelm@69248
   327
  markupN, consistentN, unbreakableN, indentN, widthN,
wenzelm@69248
   328
  blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
wenzelm@69248
   329
wenzelm@69968
   330
  wordsN, words,
wenzelm@69234
   331
wenzelm@69234
   332
  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
wenzelm@69234
   333
  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
wenzelm@69320
   334
  inner_cartoucheN, inner_cartouche,
wenzelm@69234
   335
  token_rangeN, token_range,
wenzelm@69234
   336
  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
wenzelm@69234
   337
wenzelm@69234
   338
  antiquotedN, antiquoted, antiquoteN, antiquote,
wenzelm@69234
   339
wenzelm@69234
   340
  paragraphN, paragraph, text_foldN, text_fold,
wenzelm@69234
   341
wenzelm@69234
   342
  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
wenzelm@69234
   343
  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
wenzelm@69320
   344
  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
wenzelm@69320
   345
  comment2N, comment2, comment3N, comment3,
wenzelm@69234
   346
wenzelm@69794
   347
  acceptedN, accepted, forkedN, forked, joinedN, joined, runningN, running, finishedN, finished,
wenzelm@69794
   348
  failedN, failed, canceledN, canceled, initializedN, initialized, finalizedN, finalized,
wenzelm@69794
   349
  consolidatedN, consolidated,
wenzelm@69794
   350
wenzelm@69234
   351
  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
wenzelm@69234
   352
  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
wenzelm@69234
   353
wenzelm@69234
   354
  intensifyN, intensify,
wenzelm@69234
   355
  Output, no_output)
wenzelm@69225
   356
where
wenzelm@69225
   357
wenzelm@69248
   358
import Prelude hiding (words, error, break)
wenzelm@69234
   359
wenzelm@69234
   360
import Isabelle.Library
wenzelm@69225
   361
import qualified Isabelle.Properties as Properties
wenzelm@69248
   362
import qualified Isabelle.Value as Value
wenzelm@69225
   363
wenzelm@69225
   364
wenzelm@69234
   365
{- basic markup -}
wenzelm@69234
   366
wenzelm@69225
   367
type T = (String, Properties.T)
wenzelm@69225
   368
wenzelm@69225
   369
empty :: T
wenzelm@69225
   370
empty = ("", [])
wenzelm@69225
   371
wenzelm@69225
   372
is_empty :: T -> Bool
wenzelm@69225
   373
is_empty ("", _) = True
wenzelm@69225
   374
is_empty _ = False
wenzelm@69225
   375
wenzelm@69234
   376
properties :: Properties.T -> T -> T
wenzelm@69234
   377
properties more_props (elem, props) =
wenzelm@69234
   378
  (elem, fold_rev Properties.put more_props props)
wenzelm@69234
   379
wenzelm@69234
   380
markup_elem name = (name, (name, []) :: T)
wenzelm@69291
   381
markup_string name prop = (name, \s -> (name, [(prop, s)]) :: T)
wenzelm@69234
   382
wenzelm@69234
   383
wenzelm@69234
   384
{- misc properties -}
wenzelm@69234
   385
wenzelm@69234
   386
nameN :: String
wenzelm@69234
   387
nameN = \<open>Markup.nameN\<close>
wenzelm@69234
   388
wenzelm@69234
   389
name :: String -> T -> T
wenzelm@69234
   390
name a = properties [(nameN, a)]
wenzelm@69234
   391
wenzelm@69234
   392
xnameN :: String
wenzelm@69234
   393
xnameN = \<open>Markup.xnameN\<close>
wenzelm@69234
   394
wenzelm@69234
   395
xname :: String -> T -> T
wenzelm@69234
   396
xname a = properties [(xnameN, a)]
wenzelm@69234
   397
wenzelm@69234
   398
kindN :: String
wenzelm@69234
   399
kindN = \<open>Markup.kindN\<close>
wenzelm@69234
   400
wenzelm@69234
   401
wenzelm@69315
   402
{- formal entities -}
wenzelm@69315
   403
wenzelm@69315
   404
bindingN :: String; binding :: T
wenzelm@69315
   405
(bindingN, binding) = markup_elem \<open>Markup.bindingN\<close>
wenzelm@69315
   406
wenzelm@69315
   407
entityN :: String; entity :: String -> String -> T
wenzelm@69315
   408
entityN = \<open>Markup.entityN\<close>
wenzelm@69315
   409
entity kind name =
wenzelm@69315
   410
  (entityN,
wenzelm@69315
   411
    (if null name then [] else [(nameN, name)]) ++ (if null kind then [] else [(kindN, kind)]))
wenzelm@69315
   412
wenzelm@69315
   413
defN :: String
wenzelm@69315
   414
defN = \<open>Markup.defN\<close>
wenzelm@69315
   415
wenzelm@69315
   416
refN :: String
wenzelm@69315
   417
refN = \<open>Markup.refN\<close>
wenzelm@69315
   418
wenzelm@69315
   419
wenzelm@69288
   420
{- completion -}
wenzelm@69288
   421
wenzelm@69288
   422
completionN :: String; completion :: T
wenzelm@69288
   423
(completionN, completion) = markup_elem \<open>Markup.completionN\<close>
wenzelm@69288
   424
wenzelm@69288
   425
no_completionN :: String; no_completion :: T
wenzelm@69288
   426
(no_completionN, no_completion) = markup_elem \<open>Markup.no_completionN\<close>
wenzelm@69288
   427
wenzelm@69288
   428
wenzelm@69234
   429
{- position -}
wenzelm@69234
   430
wenzelm@69234
   431
lineN, end_lineN :: String
wenzelm@69234
   432
lineN = \<open>Markup.lineN\<close>
wenzelm@69234
   433
end_lineN = \<open>Markup.end_lineN\<close>
wenzelm@69234
   434
wenzelm@69234
   435
offsetN, end_offsetN :: String
wenzelm@69234
   436
offsetN = \<open>Markup.offsetN\<close>
wenzelm@69234
   437
end_offsetN = \<open>Markup.end_offsetN\<close>
wenzelm@69234
   438
wenzelm@69234
   439
fileN, idN :: String
wenzelm@69234
   440
fileN = \<open>Markup.fileN\<close>
wenzelm@69234
   441
idN = \<open>Markup.idN\<close>
wenzelm@69234
   442
wenzelm@69234
   443
positionN :: String; position :: T
wenzelm@69234
   444
(positionN, position) = markup_elem \<open>Markup.positionN\<close>
wenzelm@69234
   445
wenzelm@69234
   446
wenzelm@69291
   447
{- expression -}
wenzelm@69291
   448
wenzelm@69291
   449
expressionN :: String
wenzelm@69291
   450
expressionN = \<open>Markup.expressionN\<close>
wenzelm@69291
   451
wenzelm@69291
   452
expression :: String -> T
wenzelm@69291
   453
expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
wenzelm@69291
   454
wenzelm@69291
   455
wenzelm@69291
   456
{- citation -}
wenzelm@69291
   457
wenzelm@69291
   458
citationN :: String; citation :: String -> T
wenzelm@69291
   459
(citationN, citation) = markup_string \<open>Markup.citationN\<close> nameN
wenzelm@69291
   460
wenzelm@69291
   461
wenzelm@69291
   462
{- external resources -}
wenzelm@69291
   463
wenzelm@69291
   464
pathN :: String; path :: String -> T
wenzelm@69291
   465
(pathN, path) = markup_string \<open>Markup.pathN\<close> nameN
wenzelm@69291
   466
wenzelm@69291
   467
urlN :: String; url :: String -> T
wenzelm@69291
   468
(urlN, url) = markup_string \<open>Markup.urlN\<close> nameN
wenzelm@69291
   469
wenzelm@69291
   470
docN :: String; doc :: String -> T
wenzelm@69291
   471
(docN, doc) = markup_string \<open>Markup.docN\<close> nameN
wenzelm@69291
   472
wenzelm@69291
   473
wenzelm@69248
   474
{- pretty printing -}
wenzelm@69248
   475
wenzelm@69248
   476
markupN, consistentN, unbreakableN, indentN :: String
wenzelm@69248
   477
markupN = \<open>Markup.markupN\<close>;
wenzelm@69248
   478
consistentN = \<open>Markup.consistentN\<close>;
wenzelm@69248
   479
unbreakableN = \<open>Markup.unbreakableN\<close>;
wenzelm@69248
   480
indentN = \<open>Markup.indentN\<close>;
wenzelm@69248
   481
wenzelm@69248
   482
widthN :: String
wenzelm@69248
   483
widthN = \<open>Markup.widthN\<close>
wenzelm@69248
   484
wenzelm@69248
   485
blockN :: String
wenzelm@69248
   486
blockN = \<open>Markup.blockN\<close>
wenzelm@69248
   487
block :: Bool -> Int -> T
wenzelm@69248
   488
block c i =
wenzelm@69248
   489
  (blockN,
wenzelm@69248
   490
    (if c then [(consistentN, Value.print_bool c)] else []) ++
wenzelm@69248
   491
    (if i /= 0 then [(indentN, Value.print_int i)] else []))
wenzelm@69248
   492
wenzelm@69248
   493
breakN :: String
wenzelm@69248
   494
breakN = \<open>Markup.breakN\<close>
wenzelm@69248
   495
break :: Int -> Int -> T
wenzelm@69248
   496
break w i =
wenzelm@69248
   497
  (breakN,
wenzelm@69248
   498
    (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
wenzelm@69248
   499
    (if i /= 0 then [(indentN, Value.print_int i)] else []))
wenzelm@69248
   500
wenzelm@69248
   501
fbreakN :: String; fbreak :: T
wenzelm@69248
   502
(fbreakN, fbreak) = markup_elem \<open>Markup.fbreakN\<close>
wenzelm@69248
   503
wenzelm@69248
   504
itemN :: String; item :: T
wenzelm@69248
   505
(itemN, item) = markup_elem \<open>Markup.itemN\<close>
wenzelm@69248
   506
wenzelm@69248
   507
wenzelm@69234
   508
{- text properties -}
wenzelm@69234
   509
wenzelm@69234
   510
wordsN :: String; words :: T
wenzelm@69234
   511
(wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
wenzelm@69234
   512
wenzelm@69234
   513
wenzelm@69234
   514
{- inner syntax -}
wenzelm@69234
   515
wenzelm@69234
   516
tfreeN :: String; tfree :: T
wenzelm@69234
   517
(tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
wenzelm@69234
   518
wenzelm@69234
   519
tvarN :: String; tvar :: T
wenzelm@69234
   520
(tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
wenzelm@69234
   521
wenzelm@69234
   522
freeN :: String; free :: T
wenzelm@69234
   523
(freeN, free) = markup_elem \<open>Markup.freeN\<close>
wenzelm@69234
   524
wenzelm@69234
   525
skolemN :: String; skolem :: T
wenzelm@69234
   526
(skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
wenzelm@69234
   527
wenzelm@69234
   528
boundN :: String; bound :: T
wenzelm@69234
   529
(boundN, bound) = markup_elem \<open>Markup.boundN\<close>
wenzelm@69234
   530
wenzelm@69234
   531
varN :: String; var :: T
wenzelm@69234
   532
(varN, var) = markup_elem \<open>Markup.varN\<close>
wenzelm@69234
   533
wenzelm@69234
   534
numeralN :: String; numeral :: T
wenzelm@69234
   535
(numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
wenzelm@69234
   536
wenzelm@69234
   537
literalN :: String; literal :: T
wenzelm@69234
   538
(literalN, literal) = markup_elem \<open>Markup.literalN\<close>
wenzelm@69234
   539
wenzelm@69234
   540
delimiterN :: String; delimiter :: T
wenzelm@69234
   541
(delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
wenzelm@69234
   542
wenzelm@69234
   543
inner_stringN :: String; inner_string :: T
wenzelm@69234
   544
(inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
wenzelm@69234
   545
wenzelm@69234
   546
inner_cartoucheN :: String; inner_cartouche :: T
wenzelm@69234
   547
(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
wenzelm@69234
   548
wenzelm@69234
   549
wenzelm@69234
   550
token_rangeN :: String; token_range :: T
wenzelm@69234
   551
(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
wenzelm@69234
   552
wenzelm@69234
   553
wenzelm@69234
   554
sortingN :: String; sorting :: T
wenzelm@69234
   555
(sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
wenzelm@69234
   556
wenzelm@69234
   557
typingN :: String; typing :: T
wenzelm@69234
   558
(typingN, typing) = markup_elem \<open>Markup.typingN\<close>
wenzelm@69234
   559
wenzelm@69234
   560
class_parameterN :: String; class_parameter :: T
wenzelm@69234
   561
(class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
wenzelm@69234
   562
wenzelm@69234
   563
wenzelm@69234
   564
{- antiquotations -}
wenzelm@69234
   565
wenzelm@69234
   566
antiquotedN :: String; antiquoted :: T
wenzelm@69234
   567
(antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
wenzelm@69234
   568
wenzelm@69234
   569
antiquoteN :: String; antiquote :: T
wenzelm@69234
   570
(antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
wenzelm@69234
   571
wenzelm@69234
   572
wenzelm@69234
   573
{- text structure -}
wenzelm@69234
   574
wenzelm@69234
   575
paragraphN :: String; paragraph :: T
wenzelm@69234
   576
(paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
wenzelm@69234
   577
wenzelm@69234
   578
text_foldN :: String; text_fold :: T
wenzelm@69234
   579
(text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
wenzelm@69234
   580
wenzelm@69234
   581
wenzelm@69234
   582
{- outer syntax -}
wenzelm@69234
   583
wenzelm@69234
   584
keyword1N :: String; keyword1 :: T
wenzelm@69234
   585
(keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
wenzelm@69234
   586
wenzelm@69234
   587
keyword2N :: String; keyword2 :: T
wenzelm@69234
   588
(keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
wenzelm@69234
   589
wenzelm@69234
   590
keyword3N :: String; keyword3 :: T
wenzelm@69234
   591
(keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
wenzelm@69234
   592
wenzelm@69234
   593
quasi_keywordN :: String; quasi_keyword :: T
wenzelm@69234
   594
(quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
wenzelm@69234
   595
wenzelm@69234
   596
improperN :: String; improper :: T
wenzelm@69234
   597
(improperN, improper) = markup_elem \<open>Markup.improperN\<close>
wenzelm@69234
   598
wenzelm@69234
   599
operatorN :: String; operator :: T
wenzelm@69234
   600
(operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
wenzelm@69234
   601
wenzelm@69234
   602
stringN :: String; string :: T
wenzelm@69234
   603
(stringN, string) = markup_elem \<open>Markup.stringN\<close>
wenzelm@69234
   604
wenzelm@69234
   605
alt_stringN :: String; alt_string :: T
wenzelm@69234
   606
(alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
wenzelm@69234
   607
wenzelm@69234
   608
verbatimN :: String; verbatim :: T
wenzelm@69234
   609
(verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
wenzelm@69234
   610
wenzelm@69234
   611
cartoucheN :: String; cartouche :: T
wenzelm@69234
   612
(cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
wenzelm@69234
   613
wenzelm@69234
   614
commentN :: String; comment :: T
wenzelm@69234
   615
(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
wenzelm@69234
   616
wenzelm@69234
   617
wenzelm@69320
   618
{- comments -}
wenzelm@69320
   619
wenzelm@69320
   620
comment1N :: String; comment1 :: T
wenzelm@69320
   621
(comment1N, comment1) = markup_elem \<open>Markup.comment1N\<close>
wenzelm@69320
   622
wenzelm@69320
   623
comment2N :: String; comment2 :: T
wenzelm@69320
   624
(comment2N, comment2) = markup_elem \<open>Markup.comment2N\<close>
wenzelm@69320
   625
wenzelm@69320
   626
comment3N :: String; comment3 :: T
wenzelm@69320
   627
(comment3N, comment3) = markup_elem \<open>Markup.comment3N\<close>
wenzelm@69320
   628
wenzelm@69320
   629
wenzelm@69793
   630
{- command status -}
wenzelm@69793
   631
wenzelm@69793
   632
acceptedN, forkedN, joinedN, runningN, finishedN, failedN, canceledN,
wenzelm@69793
   633
  initializedN, finalizedN, consolidatedN :: String
wenzelm@69793
   634
accepted, forked, joined, running, finished, failed, canceled,
wenzelm@69793
   635
  initialized, finalized, consolidated :: T
wenzelm@69793
   636
(acceptedN, accepted) = markup_elem \<open>Markup.acceptedN\<close>
wenzelm@69793
   637
(forkedN, forked) = markup_elem \<open>Markup.forkedN\<close>
wenzelm@69793
   638
(joinedN, joined) = markup_elem \<open>Markup.joinedN\<close>
wenzelm@69793
   639
(runningN, running) = markup_elem \<open>Markup.runningN\<close>
wenzelm@69793
   640
(finishedN, finished) = markup_elem \<open>Markup.finishedN\<close>
wenzelm@69793
   641
(failedN, failed) = markup_elem \<open>Markup.failedN\<close>
wenzelm@69793
   642
(canceledN, canceled) = markup_elem \<open>Markup.canceledN\<close>
wenzelm@69793
   643
(initializedN, initialized) = markup_elem \<open>Markup.initializedN\<close>
wenzelm@69793
   644
(finalizedN, finalized) = markup_elem \<open>Markup.finalizedN\<close>
wenzelm@69793
   645
(consolidatedN, consolidated) = markup_elem \<open>Markup.consolidatedN\<close>
wenzelm@69793
   646
wenzelm@69793
   647
wenzelm@69234
   648
{- messages -}
wenzelm@69234
   649
wenzelm@69234
   650
writelnN :: String; writeln :: T
wenzelm@69234
   651
(writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
wenzelm@69234
   652
wenzelm@69234
   653
stateN :: String; state :: T
wenzelm@69234
   654
(stateN, state) = markup_elem \<open>Markup.stateN\<close>
wenzelm@69234
   655
wenzelm@69234
   656
informationN :: String; information :: T
wenzelm@69234
   657
(informationN, information) = markup_elem \<open>Markup.informationN\<close>
wenzelm@69234
   658
wenzelm@69234
   659
tracingN :: String; tracing :: T
wenzelm@69234
   660
(tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
wenzelm@69234
   661
wenzelm@69234
   662
warningN :: String; warning :: T
wenzelm@69234
   663
(warningN, warning) = markup_elem \<open>Markup.warningN\<close>
wenzelm@69234
   664
wenzelm@69234
   665
legacyN :: String; legacy :: T
wenzelm@69234
   666
(legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
wenzelm@69234
   667
wenzelm@69234
   668
errorN :: String; error :: T
wenzelm@69234
   669
(errorN, error) = markup_elem \<open>Markup.errorN\<close>
wenzelm@69234
   670
wenzelm@69234
   671
reportN :: String; report :: T
wenzelm@69234
   672
(reportN, report) = markup_elem \<open>Markup.reportN\<close>
wenzelm@69234
   673
wenzelm@69234
   674
no_reportN :: String; no_report :: T
wenzelm@69234
   675
(no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
wenzelm@69234
   676
wenzelm@69234
   677
intensifyN :: String; intensify :: T
wenzelm@69234
   678
(intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
wenzelm@69234
   679
wenzelm@69234
   680
wenzelm@69234
   681
{- output -}
wenzelm@69225
   682
wenzelm@69225
   683
type Output = (String, String)
wenzelm@69225
   684
wenzelm@69225
   685
no_output :: Output
wenzelm@69225
   686
no_output = ("", "")
wenzelm@69222
   687
\<close>
wenzelm@69222
   688
wenzelm@69444
   689
generate_file "Isabelle/Completion.hs" = \<open>
wenzelm@69445
   690
{-  Title:      Isabelle/Completion.hs
wenzelm@69288
   691
    Author:     Makarius
wenzelm@69288
   692
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69288
   693
wenzelm@69288
   694
Completion of names.
wenzelm@69288
   695
wenzelm@69288
   696
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
wenzelm@69288
   697
-}
wenzelm@69288
   698
wenzelm@69289
   699
module Isabelle.Completion (
wenzelm@69289
   700
    Name, T, names, none, make, markup_element, markup_report, make_report
wenzelm@69289
   701
  ) where
wenzelm@69288
   702
wenzelm@69288
   703
import qualified Data.List as List
wenzelm@69288
   704
wenzelm@69288
   705
import Isabelle.Library
wenzelm@69288
   706
import qualified Isabelle.Properties as Properties
wenzelm@69288
   707
import qualified Isabelle.Markup as Markup
wenzelm@69288
   708
import qualified Isabelle.XML.Encode as Encode
wenzelm@69288
   709
import qualified Isabelle.XML as XML
wenzelm@69288
   710
import qualified Isabelle.YXML as YXML
wenzelm@69288
   711
wenzelm@69288
   712
wenzelm@69288
   713
type Name = (String, (String, String))  -- external name, kind, internal name
wenzelm@69288
   714
data T = Completion Properties.T Int [Name]  -- position, total length, names
wenzelm@69288
   715
wenzelm@69288
   716
names :: Int -> Properties.T -> [Name] -> T
wenzelm@69288
   717
names limit props names = Completion props (length names) (take limit names)
wenzelm@69288
   718
wenzelm@69288
   719
none :: T
wenzelm@69288
   720
none = names 0 [] []
wenzelm@69288
   721
wenzelm@69288
   722
make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T
wenzelm@69288
   723
make limit (name, props) make_names =
wenzelm@69288
   724
  if name /= "" && name /= "_"
wenzelm@69288
   725
  then names limit props (make_names $ List.isPrefixOf $ clean_name name)
wenzelm@69288
   726
  else none
wenzelm@69288
   727
wenzelm@69289
   728
markup_element :: T -> (Markup.T, XML.Body)
wenzelm@69289
   729
markup_element (Completion props total names) =
wenzelm@69289
   730
  if not (null names) then
wenzelm@69289
   731
    let
wenzelm@69289
   732
      markup = Markup.properties props Markup.completion
wenzelm@69289
   733
      body =
wenzelm@69289
   734
        Encode.pair Encode.int
wenzelm@69289
   735
          (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
wenzelm@69289
   736
          (total, names)
wenzelm@69289
   737
    in (markup, body)
wenzelm@69289
   738
  else (Markup.empty, [])
wenzelm@69288
   739
wenzelm@69289
   740
markup_report :: [T] -> String
wenzelm@69289
   741
markup_report [] = ""
wenzelm@69289
   742
markup_report elems =
wenzelm@69290
   743
  YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
wenzelm@69289
   744
wenzelm@69289
   745
make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
wenzelm@69289
   746
make_report limit name_props make_names =
wenzelm@69289
   747
  markup_report [make limit name_props make_names]
wenzelm@69288
   748
\<close>
wenzelm@69288
   749
wenzelm@69444
   750
generate_file "Isabelle/File.hs" = \<open>
wenzelm@69445
   751
{-  Title:      Isabelle/File.hs
wenzelm@69278
   752
    Author:     Makarius
wenzelm@69278
   753
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69278
   754
wenzelm@69280
   755
File-system operations.
wenzelm@69280
   756
wenzelm@69280
   757
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
wenzelm@69278
   758
-}
wenzelm@69278
   759
wenzelm@69278
   760
module Isabelle.File (setup, read, write, append) where
wenzelm@69278
   761
wenzelm@69278
   762
import Prelude hiding (read)
wenzelm@69278
   763
import System.IO (IO)
wenzelm@69278
   764
import qualified System.IO as IO
wenzelm@69278
   765
wenzelm@69278
   766
setup :: IO.Handle -> IO ()
wenzelm@69278
   767
setup h = do
wenzelm@69278
   768
  IO.hSetEncoding h IO.utf8
wenzelm@69278
   769
  IO.hSetNewlineMode h IO.noNewlineTranslation
wenzelm@69278
   770
wenzelm@69278
   771
read :: IO.FilePath -> IO String
wenzelm@69278
   772
read path =
wenzelm@69278
   773
  IO.withFile path IO.ReadMode (\h ->
wenzelm@69278
   774
    do setup h; IO.hGetContents h >>= \s -> length s `seq` return s)
wenzelm@69278
   775
wenzelm@69278
   776
write :: IO.FilePath -> String -> IO ()
wenzelm@69278
   777
write path s =
wenzelm@69278
   778
  IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s)
wenzelm@69278
   779
wenzelm@69278
   780
append :: IO.FilePath -> String -> IO ()
wenzelm@69278
   781
append path s =
wenzelm@69278
   782
  IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
wenzelm@69278
   783
\<close>
wenzelm@69278
   784
wenzelm@69444
   785
generate_file "Isabelle/XML.hs" = \<open>
wenzelm@69445
   786
{-  Title:      Isabelle/XML.hs
wenzelm@69225
   787
    Author:     Makarius
wenzelm@69225
   788
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   789
wenzelm@69225
   790
Untyped XML trees and representation of ML values.
wenzelm@69280
   791
wenzelm@69280
   792
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
wenzelm@69225
   793
-}
wenzelm@69225
   794
wenzelm@69225
   795
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
wenzelm@69225
   796
where
wenzelm@69225
   797
wenzelm@69225
   798
import qualified Data.List as List
wenzelm@69225
   799
wenzelm@69225
   800
import Isabelle.Library
wenzelm@69225
   801
import qualified Isabelle.Properties as Properties
wenzelm@69225
   802
import qualified Isabelle.Markup as Markup
wenzelm@69225
   803
import qualified Isabelle.Buffer as Buffer
wenzelm@69225
   804
wenzelm@69225
   805
wenzelm@69225
   806
{- types -}
wenzelm@69225
   807
wenzelm@69225
   808
type Attributes = Properties.T
wenzelm@69225
   809
type Body = [Tree]
wenzelm@69290
   810
data Tree = Elem (Markup.T, Body) | Text String
wenzelm@69225
   811
wenzelm@69225
   812
wenzelm@69225
   813
{- wrapped elements -}
wenzelm@69225
   814
wenzelm@69482
   815
wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
wenzelm@69236
   816
wrap_elem (((a, atts), body1), body2) =
wenzelm@69290
   817
  Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)
wenzelm@69225
   818
wenzelm@69482
   819
unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
wenzelm@69236
   820
unwrap_elem
wenzelm@69290
   821
  (Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)) =
wenzelm@69236
   822
  Just (((a, atts), body1), body2)
wenzelm@69225
   823
unwrap_elem _ = Nothing
wenzelm@69225
   824
wenzelm@69225
   825
wenzelm@69225
   826
{- text content -}
wenzelm@69225
   827
wenzelm@69482
   828
add_content :: Tree -> Buffer.T -> Buffer.T
wenzelm@69225
   829
add_content tree =
wenzelm@69225
   830
  case unwrap_elem tree of
wenzelm@69225
   831
    Just (_, ts) -> fold add_content ts
wenzelm@69225
   832
    Nothing ->
wenzelm@69225
   833
      case tree of
wenzelm@69290
   834
        Elem (_, ts) -> fold add_content ts
wenzelm@69225
   835
        Text s -> Buffer.add s
wenzelm@69225
   836
wenzelm@69482
   837
content_of :: Body -> String
wenzelm@69225
   838
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
wenzelm@69225
   839
wenzelm@69225
   840
wenzelm@69225
   841
{- string representation -}
wenzelm@69225
   842
wenzelm@69225
   843
encode '<' = "&lt;"
wenzelm@69225
   844
encode '>' = "&gt;"
wenzelm@69225
   845
encode '&' = "&amp;"
wenzelm@69225
   846
encode '\'' = "&apos;"
wenzelm@69225
   847
encode '\"' = "&quot;"
wenzelm@69225
   848
encode c = [c]
wenzelm@69225
   849
wenzelm@69225
   850
instance Show Tree where
wenzelm@69225
   851
  show tree =
wenzelm@69225
   852
    Buffer.empty |> show_tree tree |> Buffer.content
wenzelm@69225
   853
    where
wenzelm@69290
   854
      show_tree (Elem ((name, atts), [])) =
wenzelm@69225
   855
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
wenzelm@69290
   856
      show_tree (Elem ((name, atts), ts)) =
wenzelm@69225
   857
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
wenzelm@69225
   858
        fold show_tree ts #>
wenzelm@69225
   859
        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
wenzelm@69225
   860
      show_tree (Text s) = Buffer.add (show_text s)
wenzelm@69225
   861
wenzelm@69225
   862
      show_elem name atts =
wenzelm@69225
   863
        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
wenzelm@69225
   864
wenzelm@69225
   865
      show_text = concatMap encode
wenzelm@69225
   866
\<close>
wenzelm@69225
   867
wenzelm@69444
   868
generate_file "Isabelle/XML/Encode.hs" = \<open>
wenzelm@69445
   869
{-  Title:      Isabelle/XML/Encode.hs
wenzelm@69240
   870
    Author:     Makarius
wenzelm@69240
   871
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240
   872
wenzelm@69240
   873
XML as data representation language.
wenzelm@69280
   874
wenzelm@69280
   875
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
wenzelm@69240
   876
-}
wenzelm@69240
   877
wenzelm@69240
   878
module Isabelle.XML.Encode (
wenzelm@69240
   879
  A, T, V,
wenzelm@69240
   880
wenzelm@69240
   881
  int_atom, bool_atom, unit_atom,
wenzelm@69240
   882
wenzelm@69287
   883
  tree, properties, string, int, bool, unit, pair, triple, list, variant
wenzelm@69240
   884
)
wenzelm@69240
   885
where
wenzelm@69240
   886
wenzelm@69240
   887
import Isabelle.Library
wenzelm@69240
   888
import qualified Isabelle.Value as Value
wenzelm@69240
   889
import qualified Isabelle.Properties as Properties
wenzelm@69240
   890
import qualified Isabelle.XML as XML
wenzelm@69240
   891
wenzelm@69240
   892
wenzelm@69240
   893
type A a = a -> String
wenzelm@69240
   894
type T a = a -> XML.Body
wenzelm@69240
   895
type V a = a -> Maybe ([String], XML.Body)
wenzelm@69240
   896
wenzelm@69240
   897
wenzelm@69240
   898
-- atomic values
wenzelm@69240
   899
wenzelm@69240
   900
int_atom :: A Int
wenzelm@69240
   901
int_atom = Value.print_int
wenzelm@69240
   902
wenzelm@69240
   903
bool_atom :: A Bool
wenzelm@69240
   904
bool_atom False = "0"
wenzelm@69240
   905
bool_atom True = "1"
wenzelm@69240
   906
wenzelm@69240
   907
unit_atom :: A ()
wenzelm@69240
   908
unit_atom () = ""
wenzelm@69240
   909
wenzelm@69240
   910
wenzelm@69240
   911
-- structural nodes
wenzelm@69240
   912
wenzelm@69290
   913
node ts = XML.Elem ((":", []), ts)
wenzelm@69240
   914
wenzelm@69240
   915
vector = map_index (\(i, x) -> (int_atom i, x))
wenzelm@69240
   916
wenzelm@69290
   917
tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
wenzelm@69240
   918
wenzelm@69240
   919
wenzelm@69240
   920
-- representation of standard types
wenzelm@69240
   921
wenzelm@69240
   922
tree :: T XML.Tree
wenzelm@69240
   923
tree t = [t]
wenzelm@69240
   924
wenzelm@69240
   925
properties :: T Properties.T
wenzelm@69290
   926
properties props = [XML.Elem ((":", props), [])]
wenzelm@69240
   927
wenzelm@69240
   928
string :: T String
wenzelm@69240
   929
string "" = []
wenzelm@69240
   930
string s = [XML.Text s]
wenzelm@69240
   931
wenzelm@69240
   932
int :: T Int
wenzelm@69240
   933
int = string . int_atom
wenzelm@69240
   934
wenzelm@69240
   935
bool :: T Bool
wenzelm@69240
   936
bool = string . bool_atom
wenzelm@69240
   937
wenzelm@69240
   938
unit :: T ()
wenzelm@69240
   939
unit = string . unit_atom
wenzelm@69240
   940
wenzelm@69240
   941
pair :: T a -> T b -> T (a, b)
wenzelm@69240
   942
pair f g (x, y) = [node (f x), node (g y)]
wenzelm@69240
   943
wenzelm@69240
   944
triple :: T a -> T b -> T c -> T (a, b, c)
wenzelm@69240
   945
triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
wenzelm@69240
   946
wenzelm@69240
   947
list :: T a -> T [a]
wenzelm@69240
   948
list f xs = map (node . f) xs
wenzelm@69240
   949
wenzelm@69240
   950
variant :: [V a] -> T a
wenzelm@69240
   951
variant fs x = [tagged (the (get_index (\f -> f x) fs))]
wenzelm@69240
   952
\<close>
wenzelm@69240
   953
wenzelm@69444
   954
generate_file "Isabelle/XML/Decode.hs" = \<open>
wenzelm@69445
   955
{-  Title:      Isabelle/XML/Decode.hs
wenzelm@69240
   956
    Author:     Makarius
wenzelm@69240
   957
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240
   958
wenzelm@69240
   959
XML as data representation language.
wenzelm@69280
   960
wenzelm@69280
   961
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
wenzelm@69240
   962
-}
wenzelm@69240
   963
wenzelm@69240
   964
module Isabelle.XML.Decode (
wenzelm@69240
   965
  A, T, V,
wenzelm@69240
   966
wenzelm@69240
   967
  int_atom, bool_atom, unit_atom,
wenzelm@69240
   968
wenzelm@69240
   969
  tree, properties, string, init, bool, unit, pair, triple, list, variant
wenzelm@69240
   970
)
wenzelm@69240
   971
where
wenzelm@69240
   972
wenzelm@69240
   973
import Data.List ((!!))
wenzelm@69240
   974
wenzelm@69240
   975
import Isabelle.Library
wenzelm@69240
   976
import qualified Isabelle.Value as Value
wenzelm@69240
   977
import qualified Isabelle.Properties as Properties
wenzelm@69240
   978
import qualified Isabelle.XML as XML
wenzelm@69240
   979
wenzelm@69240
   980
wenzelm@69240
   981
type A a = String -> a
wenzelm@69240
   982
type T a = XML.Body -> a
wenzelm@69240
   983
type V a = ([String], XML.Body) -> a
wenzelm@69240
   984
wenzelm@69240
   985
err_atom = error "Malformed XML atom"
wenzelm@69240
   986
err_body = error "Malformed XML body"
wenzelm@69240
   987
wenzelm@69240
   988
wenzelm@69240
   989
{- atomic values -}
wenzelm@69240
   990
wenzelm@69240
   991
int_atom :: A Int
wenzelm@69240
   992
int_atom s =
wenzelm@69240
   993
  case Value.parse_int s of
wenzelm@69240
   994
    Just i -> i
wenzelm@69240
   995
    Nothing -> err_atom
wenzelm@69240
   996
wenzelm@69240
   997
bool_atom :: A Bool
wenzelm@69240
   998
bool_atom "0" = False
wenzelm@69240
   999
bool_atom "1" = True
wenzelm@69240
  1000
bool_atom _ = err_atom
wenzelm@69240
  1001
wenzelm@69240
  1002
unit_atom :: A ()
wenzelm@69240
  1003
unit_atom "" = ()
wenzelm@69240
  1004
unit_atom _ = err_atom
wenzelm@69240
  1005
wenzelm@69240
  1006
wenzelm@69240
  1007
{- structural nodes -}
wenzelm@69240
  1008
wenzelm@69290
  1009
node (XML.Elem ((":", []), ts)) = ts
wenzelm@69240
  1010
node _ = err_body
wenzelm@69240
  1011
wenzelm@69240
  1012
vector atts =
wenzelm@69240
  1013
  map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
wenzelm@69240
  1014
wenzelm@69290
  1015
tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
wenzelm@69240
  1016
tagged _ = err_body
wenzelm@69240
  1017
wenzelm@69240
  1018
wenzelm@69240
  1019
{- representation of standard types -}
wenzelm@69240
  1020
wenzelm@69240
  1021
tree :: T XML.Tree
wenzelm@69240
  1022
tree [t] = t
wenzelm@69240
  1023
tree _ = err_body
wenzelm@69240
  1024
wenzelm@69240
  1025
properties :: T Properties.T
wenzelm@69290
  1026
properties [XML.Elem ((":", props), [])] = props
wenzelm@69240
  1027
properties _ = err_body
wenzelm@69240
  1028
wenzelm@69240
  1029
string :: T String
wenzelm@69240
  1030
string [] = ""
wenzelm@69240
  1031
string [XML.Text s] = s
wenzelm@69240
  1032
string _ = err_body
wenzelm@69240
  1033
wenzelm@69240
  1034
int :: T Int
wenzelm@69240
  1035
int = int_atom . string
wenzelm@69240
  1036
wenzelm@69240
  1037
bool :: T Bool
wenzelm@69240
  1038
bool = bool_atom . string
wenzelm@69240
  1039
wenzelm@69240
  1040
unit :: T ()
wenzelm@69240
  1041
unit = unit_atom . string
wenzelm@69240
  1042
wenzelm@69240
  1043
pair :: T a -> T b -> T (a, b)
wenzelm@69240
  1044
pair f g [t1, t2] = (f (node t1), g (node t2))
wenzelm@69240
  1045
pair _ _ _ = err_body
wenzelm@69240
  1046
wenzelm@69240
  1047
triple :: T a -> T b -> T c -> T (a, b, c)
wenzelm@69240
  1048
triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
wenzelm@69240
  1049
triple _ _ _ _ = err_body
wenzelm@69240
  1050
wenzelm@69240
  1051
list :: T a -> T [a]
wenzelm@69240
  1052
list f ts = map (f . node) ts
wenzelm@69240
  1053
wenzelm@69240
  1054
option :: T a -> T (Maybe a)
wenzelm@69240
  1055
option _ [] = Nothing
wenzelm@69240
  1056
option f [t] = Just (f (node t))
wenzelm@69240
  1057
option _ _ = err_body
wenzelm@69240
  1058
wenzelm@69240
  1059
variant :: [V a] -> T a
wenzelm@69240
  1060
variant fs [t] = (fs !! tag) (xs, ts)
wenzelm@69240
  1061
  where (tag, (xs, ts)) = tagged t
wenzelm@69240
  1062
variant _ _ = err_body
wenzelm@69240
  1063
\<close>
wenzelm@69240
  1064
wenzelm@69444
  1065
generate_file "Isabelle/YXML.hs" = \<open>
wenzelm@69445
  1066
{-  Title:      Isabelle/YXML.hs
wenzelm@69288
  1067
    Author:     Makarius
wenzelm@69288
  1068
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69288
  1069
wenzelm@69288
  1070
Efficient text representation of XML trees.  Suitable for direct
wenzelm@69288
  1071
inlining into plain text.
wenzelm@69288
  1072
wenzelm@69288
  1073
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
wenzelm@69288
  1074
-}
wenzelm@69288
  1075
wenzelm@69288
  1076
module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
wenzelm@69288
  1077
  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
wenzelm@69288
  1078
where
wenzelm@69288
  1079
wenzelm@69288
  1080
import qualified Data.Char as Char
wenzelm@69288
  1081
import qualified Data.List as List
wenzelm@69288
  1082
wenzelm@69288
  1083
import Isabelle.Library
wenzelm@69288
  1084
import qualified Isabelle.Markup as Markup
wenzelm@69288
  1085
import qualified Isabelle.XML as XML
wenzelm@69288
  1086
import qualified Isabelle.Buffer as Buffer
wenzelm@69288
  1087
wenzelm@69288
  1088
wenzelm@69288
  1089
{- markers -}
wenzelm@69288
  1090
wenzelm@69288
  1091
charX, charY :: Char
wenzelm@69288
  1092
charX = Char.chr 5
wenzelm@69288
  1093
charY = Char.chr 6
wenzelm@69288
  1094
wenzelm@69288
  1095
strX, strY, strXY, strXYX :: String
wenzelm@69288
  1096
strX = [charX]
wenzelm@69288
  1097
strY = [charY]
wenzelm@69288
  1098
strXY = strX ++ strY
wenzelm@69288
  1099
strXYX = strXY ++ strX
wenzelm@69288
  1100
wenzelm@69288
  1101
detect :: String -> Bool
wenzelm@69288
  1102
detect = any (\c -> c == charX || c == charY)
wenzelm@69288
  1103
wenzelm@69288
  1104
wenzelm@69288
  1105
{- output -}
wenzelm@69288
  1106
wenzelm@69288
  1107
output_markup :: Markup.T -> Markup.Output
wenzelm@69288
  1108
output_markup markup@(name, atts) =
wenzelm@69288
  1109
  if Markup.is_empty markup then Markup.no_output
wenzelm@69288
  1110
  else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
wenzelm@69288
  1111
wenzelm@69288
  1112
buffer_attrib (a, x) =
wenzelm@69288
  1113
  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
wenzelm@69288
  1114
wenzelm@69288
  1115
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
wenzelm@69288
  1116
buffer_body = fold buffer
wenzelm@69288
  1117
wenzelm@69288
  1118
buffer :: XML.Tree -> Buffer.T -> Buffer.T
wenzelm@69290
  1119
buffer (XML.Elem ((name, atts), ts)) =
wenzelm@69288
  1120
  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
wenzelm@69288
  1121
  buffer_body ts #>
wenzelm@69288
  1122
  Buffer.add strXYX
wenzelm@69288
  1123
buffer (XML.Text s) = Buffer.add s
wenzelm@69288
  1124
wenzelm@69288
  1125
string_of_body :: XML.Body -> String
wenzelm@69288
  1126
string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
wenzelm@69288
  1127
wenzelm@69288
  1128
string_of :: XML.Tree -> String
wenzelm@69288
  1129
string_of = string_of_body . single
wenzelm@69288
  1130
wenzelm@69288
  1131
wenzelm@69288
  1132
{- parse -}
wenzelm@69288
  1133
wenzelm@69288
  1134
-- split: fields or non-empty tokens
wenzelm@69288
  1135
wenzelm@69288
  1136
split :: Bool -> Char -> String -> [String]
wenzelm@69288
  1137
split _ _ [] = []
wenzelm@69288
  1138
split fields sep str = splitting str
wenzelm@69288
  1139
  where
wenzelm@69288
  1140
    splitting rest =
wenzelm@69288
  1141
      case span (/= sep) rest of
wenzelm@69288
  1142
        (_, []) -> cons rest []
wenzelm@69288
  1143
        (prfx, _ : rest') -> cons prfx (splitting rest')
wenzelm@69288
  1144
    cons item = if fields || not (null item) then (:) item else id
wenzelm@69288
  1145
wenzelm@69288
  1146
wenzelm@69288
  1147
-- structural errors
wenzelm@69288
  1148
wenzelm@69288
  1149
err msg = error ("Malformed YXML: " ++ msg)
wenzelm@69288
  1150
err_attribute = err "bad attribute"
wenzelm@69288
  1151
err_element = err "bad element"
wenzelm@69288
  1152
err_unbalanced "" = err "unbalanced element"
wenzelm@69288
  1153
err_unbalanced name = err ("unbalanced element " ++ quote name)
wenzelm@69288
  1154
wenzelm@69288
  1155
wenzelm@69288
  1156
-- stack operations
wenzelm@69288
  1157
wenzelm@69288
  1158
add x ((elem, body) : pending) = (elem, x : body) : pending
wenzelm@69288
  1159
wenzelm@69288
  1160
push "" _ _ = err_element
wenzelm@69288
  1161
push name atts pending = ((name, atts), []) : pending
wenzelm@69288
  1162
wenzelm@69288
  1163
pop ((("", _), _) : _) = err_unbalanced ""
wenzelm@69290
  1164
pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
wenzelm@69288
  1165
wenzelm@69288
  1166
wenzelm@69288
  1167
-- parsing
wenzelm@69288
  1168
wenzelm@69288
  1169
parse_attrib s =
wenzelm@69288
  1170
  case List.elemIndex '=' s of
wenzelm@69288
  1171
    Just i | i > 0 -> (take i s, drop (i + 1) s)
wenzelm@69288
  1172
    _ -> err_attribute
wenzelm@69288
  1173
wenzelm@69288
  1174
parse_chunk ["", ""] = pop
wenzelm@69288
  1175
parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
wenzelm@69288
  1176
parse_chunk txts = fold (add . XML.Text) txts
wenzelm@69288
  1177
wenzelm@69288
  1178
parse_body :: String -> XML.Body
wenzelm@69288
  1179
parse_body source =
wenzelm@69288
  1180
  case fold parse_chunk chunks [(("", []), [])] of
wenzelm@69288
  1181
    [(("", _), result)] -> reverse result
wenzelm@69288
  1182
    ((name, _), _) : _ -> err_unbalanced name
wenzelm@69288
  1183
  where chunks = split False charX source |> map (split True charY)
wenzelm@69288
  1184
wenzelm@69288
  1185
parse :: String -> XML.Tree
wenzelm@69288
  1186
parse source =
wenzelm@69288
  1187
  case parse_body source of
wenzelm@69288
  1188
    [result] -> result
wenzelm@69288
  1189
    [] -> XML.Text ""
wenzelm@69288
  1190
    _ -> err "multiple results"
wenzelm@69288
  1191
\<close>
wenzelm@69288
  1192
wenzelm@69444
  1193
generate_file "Isabelle/Pretty.hs" = \<open>
wenzelm@69445
  1194
{-  Title:      Isabelle/Pretty.hs
wenzelm@69248
  1195
    Author:     Makarius
wenzelm@69248
  1196
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69248
  1197
wenzelm@69248
  1198
Generic pretty printing module.
wenzelm@69280
  1199
wenzelm@69280
  1200
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
wenzelm@69248
  1201
-}
wenzelm@69248
  1202
wenzelm@69248
  1203
module Isabelle.Pretty (
wenzelm@69248
  1204
  T, symbolic, formatted, unformatted,
wenzelm@69248
  1205
wenzelm@69248
  1206
  str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
wenzelm@69248
  1207
  item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
wenzelm@69248
  1208
  commas, enclose, enum, list, str_list, big_list)
wenzelm@69248
  1209
where
wenzelm@69248
  1210
wenzelm@69453
  1211
import Isabelle.Library hiding (quote, commas)
wenzelm@69248
  1212
import qualified Data.List as List
wenzelm@69248
  1213
import qualified Isabelle.Buffer as Buffer
wenzelm@69248
  1214
import qualified Isabelle.Markup as Markup
wenzelm@69248
  1215
import qualified Isabelle.XML as XML
wenzelm@69248
  1216
import qualified Isabelle.YXML as YXML
wenzelm@69248
  1217
wenzelm@69248
  1218
wenzelm@69248
  1219
data T =
wenzelm@69248
  1220
    Block Markup.T Bool Int [T]
wenzelm@69248
  1221
  | Break Int Int
wenzelm@69248
  1222
  | Str String
wenzelm@69248
  1223
wenzelm@69248
  1224
wenzelm@69248
  1225
{- output -}
wenzelm@69248
  1226
wenzelm@69248
  1227
output_spaces n = replicate n ' '
wenzelm@69248
  1228
wenzelm@69248
  1229
symbolic_text "" = []
wenzelm@69248
  1230
symbolic_text s = [XML.Text s]
wenzelm@69248
  1231
wenzelm@69248
  1232
symbolic_markup markup body =
wenzelm@69248
  1233
  if Markup.is_empty markup then body
wenzelm@69290
  1234
  else [XML.Elem (markup, body)]
wenzelm@69248
  1235
wenzelm@69248
  1236
symbolic :: T -> XML.Body
wenzelm@69248
  1237
symbolic (Block markup consistent indent prts) =
wenzelm@69248
  1238
  concatMap symbolic prts
wenzelm@69248
  1239
  |> symbolic_markup block_markup
wenzelm@69248
  1240
  |> symbolic_markup markup
wenzelm@69248
  1241
  where block_markup = if null prts then Markup.empty else Markup.block consistent indent
wenzelm@69290
  1242
symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
wenzelm@69248
  1243
symbolic (Str s) = symbolic_text s
wenzelm@69248
  1244
wenzelm@69248
  1245
formatted :: T -> String
wenzelm@69248
  1246
formatted = YXML.string_of_body . symbolic
wenzelm@69248
  1247
wenzelm@69248
  1248
unformatted :: T -> String
wenzelm@69248
  1249
unformatted prt = Buffer.empty |> out prt |> Buffer.content
wenzelm@69248
  1250
  where
wenzelm@69248
  1251
    out (Block markup _ _ prts) =
wenzelm@69248
  1252
      let (bg, en) = YXML.output_markup markup
wenzelm@69248
  1253
      in Buffer.add bg #> fold out prts #> Buffer.add en
wenzelm@69248
  1254
    out (Break _ wd) = Buffer.add (output_spaces wd)
wenzelm@69248
  1255
    out (Str s) = Buffer.add s
wenzelm@69248
  1256
wenzelm@69248
  1257
wenzelm@69248
  1258
{- derived operations to create formatting expressions -}
wenzelm@69248
  1259
wenzelm@69248
  1260
force_nat n | n < 0 = 0
wenzelm@69248
  1261
force_nat n = n
wenzelm@69248
  1262
wenzelm@69248
  1263
str :: String -> T
wenzelm@69248
  1264
str = Str
wenzelm@69248
  1265
wenzelm@69248
  1266
brk_indent :: Int -> Int -> T
wenzelm@69248
  1267
brk_indent wd ind = Break (force_nat wd) ind
wenzelm@69248
  1268
wenzelm@69248
  1269
brk :: Int -> T
wenzelm@69248
  1270
brk wd = brk_indent wd 0
wenzelm@69248
  1271
wenzelm@69248
  1272
fbrk :: T
wenzelm@69248
  1273
fbrk = str "\n"
wenzelm@69248
  1274
wenzelm@69248
  1275
breaks, fbreaks :: [T] -> [T]
wenzelm@69248
  1276
breaks = List.intersperse (brk 1)
wenzelm@69248
  1277
fbreaks = List.intersperse fbrk
wenzelm@69248
  1278
wenzelm@69248
  1279
blk :: (Int, [T]) -> T
wenzelm@69248
  1280
blk (indent, es) = Block Markup.empty False (force_nat indent) es
wenzelm@69248
  1281
wenzelm@69248
  1282
block :: [T] -> T
wenzelm@69248
  1283
block prts = blk (2, prts)
wenzelm@69248
  1284
wenzelm@69248
  1285
strs :: [String] -> T
wenzelm@69248
  1286
strs = block . breaks . map str
wenzelm@69248
  1287
wenzelm@69248
  1288
markup :: Markup.T -> [T] -> T
wenzelm@69248
  1289
markup m = Block m False 0
wenzelm@69248
  1290
wenzelm@69248
  1291
mark :: Markup.T -> T -> T
wenzelm@69248
  1292
mark m prt = if m == Markup.empty then prt else markup m [prt]
wenzelm@69248
  1293
wenzelm@69248
  1294
mark_str :: (Markup.T, String) -> T
wenzelm@69248
  1295
mark_str (m, s) = mark m (str s)
wenzelm@69248
  1296
wenzelm@69248
  1297
marks_str :: ([Markup.T], String) -> T
wenzelm@69248
  1298
marks_str (ms, s) = fold_rev mark ms (str s)
wenzelm@69248
  1299
wenzelm@69248
  1300
item :: [T] -> T
wenzelm@69248
  1301
item = markup Markup.item
wenzelm@69248
  1302
wenzelm@69248
  1303
text_fold :: [T] -> T
wenzelm@69248
  1304
text_fold = markup Markup.text_fold
wenzelm@69248
  1305
wenzelm@69248
  1306
keyword1, keyword2 :: String -> T
wenzelm@69248
  1307
keyword1 name = mark_str (Markup.keyword1, name)
wenzelm@69248
  1308
keyword2 name = mark_str (Markup.keyword2, name)
wenzelm@69248
  1309
wenzelm@69248
  1310
text :: String -> [T]
wenzelm@69248
  1311
text = breaks . map str . words
wenzelm@69248
  1312
wenzelm@69248
  1313
paragraph :: [T] -> T
wenzelm@69248
  1314
paragraph = markup Markup.paragraph
wenzelm@69248
  1315
wenzelm@69248
  1316
para :: String -> T
wenzelm@69248
  1317
para = paragraph . text
wenzelm@69248
  1318
wenzelm@69248
  1319
quote :: T -> T
wenzelm@69248
  1320
quote prt = blk (1, [str "\"", prt, str "\""])
wenzelm@69248
  1321
wenzelm@69248
  1322
cartouche :: T -> T
wenzelm@69248
  1323
cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
wenzelm@69248
  1324
wenzelm@69248
  1325
separate :: String -> [T] -> [T]
wenzelm@69248
  1326
separate sep = List.intercalate [str sep, brk 1] . map single
wenzelm@69248
  1327
wenzelm@69248
  1328
commas :: [T] -> [T]
wenzelm@69248
  1329
commas = separate ","
wenzelm@69248
  1330
wenzelm@69248
  1331
enclose :: String -> String -> [T] -> T
wenzelm@69248
  1332
enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
wenzelm@69248
  1333
wenzelm@69248
  1334
enum :: String -> String -> String -> [T] -> T
wenzelm@69248
  1335
enum sep lpar rpar = enclose lpar rpar . separate sep
wenzelm@69248
  1336
wenzelm@69248
  1337
list :: String -> String -> [T] -> T
wenzelm@69248
  1338
list = enum ","
wenzelm@69248
  1339
wenzelm@69248
  1340
str_list :: String -> String -> [String] -> T
wenzelm@69248
  1341
str_list lpar rpar = list lpar rpar . map str
wenzelm@69248
  1342
wenzelm@69248
  1343
big_list :: String -> [T] -> T
wenzelm@69248
  1344
big_list name prts = block (fbreaks (str name : prts))
wenzelm@69248
  1345
\<close>
wenzelm@69248
  1346
wenzelm@69444
  1347
generate_file "Isabelle/Term.hs" = \<open>
wenzelm@69445
  1348
{-  Title:      Isabelle/Term.hs
wenzelm@69240
  1349
    Author:     Makarius
wenzelm@69240
  1350
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240
  1351
wenzelm@69240
  1352
Lambda terms, types, sorts.
wenzelm@69280
  1353
wenzelm@69280
  1354
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
wenzelm@69240
  1355
-}
wenzelm@69240
  1356
wenzelm@69240
  1357
module Isabelle.Term (
wenzelm@69240
  1358
  Indexname,
wenzelm@69240
  1359
wenzelm@69240
  1360
  Sort, dummyS,
wenzelm@69240
  1361
wenzelm@69240
  1362
  Typ(..), dummyT, Term(..))
wenzelm@69240
  1363
where
wenzelm@69240
  1364
wenzelm@69240
  1365
type Indexname = (String, Int)
wenzelm@69240
  1366
wenzelm@69240
  1367
wenzelm@69240
  1368
type Sort = [String]
wenzelm@69240
  1369
wenzelm@69240
  1370
dummyS :: Sort
wenzelm@69240
  1371
dummyS = [""]
wenzelm@69240
  1372
wenzelm@69240
  1373
wenzelm@69240
  1374
data Typ =
wenzelm@69240
  1375
    Type (String, [Typ])
wenzelm@69240
  1376
  | TFree (String, Sort)
wenzelm@69240
  1377
  | TVar (Indexname, Sort)
wenzelm@69240
  1378
  deriving Show
wenzelm@69240
  1379
wenzelm@69240
  1380
dummyT :: Typ
wenzelm@69240
  1381
dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
wenzelm@69240
  1382
wenzelm@69240
  1383
wenzelm@69240
  1384
data Term =
wenzelm@69240
  1385
    Const (String, Typ)
wenzelm@69240
  1386
  | Free (String, Typ)
wenzelm@69240
  1387
  | Var (Indexname, Typ)
wenzelm@69240
  1388
  | Bound Int
wenzelm@69240
  1389
  | Abs (String, Typ, Term)
wenzelm@69240
  1390
  | App (Term, Term)
wenzelm@69240
  1391
  deriving Show
wenzelm@69240
  1392
\<close>
wenzelm@69240
  1393
wenzelm@69444
  1394
generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
wenzelm@69445
  1395
{-  Title:      Isabelle/Term_XML/Encode.hs
wenzelm@69240
  1396
    Author:     Makarius
wenzelm@69240
  1397
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240
  1398
wenzelm@69240
  1399
XML data representation of lambda terms.
wenzelm@69280
  1400
wenzelm@69280
  1401
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
wenzelm@69240
  1402
-}
wenzelm@69240
  1403
wenzelm@69240
  1404
{-# LANGUAGE LambdaCase #-}
wenzelm@69240
  1405
wenzelm@69240
  1406
module Isabelle.Term_XML.Encode (sort, typ, term)
wenzelm@69240
  1407
where
wenzelm@69240
  1408
wenzelm@69240
  1409
import Isabelle.Library
wenzelm@69240
  1410
import qualified Isabelle.XML as XML
wenzelm@69240
  1411
import Isabelle.XML.Encode
wenzelm@69240
  1412
import Isabelle.Term
wenzelm@69240
  1413
wenzelm@69240
  1414
wenzelm@69240
  1415
sort :: T Sort
wenzelm@69240
  1416
sort = list string
wenzelm@69240
  1417
wenzelm@69240
  1418
typ :: T Typ
wenzelm@69240
  1419
typ ty =
wenzelm@69240
  1420
  ty |> variant
wenzelm@69240
  1421
   [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
wenzelm@69240
  1422
    \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
wenzelm@69240
  1423
    \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
wenzelm@69240
  1424
wenzelm@69240
  1425
term :: T Term
wenzelm@69240
  1426
term t =
wenzelm@69240
  1427
  t |> variant
wenzelm@69240
  1428
   [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
wenzelm@69240
  1429
    \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
wenzelm@69240
  1430
    \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
wenzelm@69240
  1431
    \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
wenzelm@69240
  1432
    \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
wenzelm@69240
  1433
    \case { App a -> Just ([], pair term term a); _ -> Nothing }]
wenzelm@69240
  1434
\<close>
wenzelm@69240
  1435
wenzelm@69444
  1436
generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
wenzelm@69445
  1437
{-  Title:      Isabelle/Term_XML/Decode.hs
wenzelm@69240
  1438
    Author:     Makarius
wenzelm@69240
  1439
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240
  1440
wenzelm@69240
  1441
XML data representation of lambda terms.
wenzelm@69280
  1442
wenzelm@69280
  1443
See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
wenzelm@69240
  1444
-}
wenzelm@69240
  1445
wenzelm@69240
  1446
module Isabelle.Term_XML.Decode (sort, typ, term)
wenzelm@69240
  1447
where
wenzelm@69240
  1448
wenzelm@69240
  1449
import Isabelle.Library
wenzelm@69240
  1450
import qualified Isabelle.XML as XML
wenzelm@69240
  1451
import Isabelle.XML.Decode
wenzelm@69240
  1452
import Isabelle.Term
wenzelm@69240
  1453
wenzelm@69240
  1454
wenzelm@69240
  1455
sort :: T Sort
wenzelm@69240
  1456
sort = list string
wenzelm@69240
  1457
wenzelm@69240
  1458
typ :: T Typ
wenzelm@69240
  1459
typ ty =
wenzelm@69240
  1460
  ty |> variant
wenzelm@69240
  1461
  [\([a], b) -> Type (a, list typ b),
wenzelm@69240
  1462
   \([a], b) -> TFree (a, sort b),
wenzelm@69240
  1463
   \([a, b], c) -> TVar ((a, int_atom b), sort c)]
wenzelm@69240
  1464
wenzelm@69240
  1465
term :: T Term
wenzelm@69240
  1466
term t =
wenzelm@69240
  1467
  t |> variant
wenzelm@69240
  1468
   [\([a], b) -> Const (a, typ b),
wenzelm@69240
  1469
    \([a], b) -> Free (a, typ b),
wenzelm@69240
  1470
    \([a, b], c) -> Var ((a, int_atom b), typ c),
wenzelm@69240
  1471
    \([a], []) -> Bound (int_atom a),
wenzelm@69240
  1472
    \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
wenzelm@69240
  1473
    \([], a) -> App (pair term term a)]
wenzelm@69240
  1474
\<close>
wenzelm@69240
  1475
wenzelm@69459
  1476
generate_file "Isabelle/UUID.hs" = \<open>
wenzelm@69459
  1477
{-  Title:      Isabelle/UUID.hs
wenzelm@69459
  1478
    Author:     Makarius
wenzelm@69459
  1479
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69459
  1480
wenzelm@69459
  1481
Universally unique identifiers.
wenzelm@69459
  1482
wenzelm@69459
  1483
See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
wenzelm@69459
  1484
-}
wenzelm@69459
  1485
wenzelm@69465
  1486
module Isabelle.UUID (
wenzelm@69465
  1487
    T,
wenzelm@69465
  1488
    parse_string, parse_bytes,
wenzelm@69465
  1489
    string, bytes,
wenzelm@69465
  1490
    random, random_string, random_bytes
wenzelm@69465
  1491
  )
wenzelm@69459
  1492
where
wenzelm@69459
  1493
wenzelm@69465
  1494
import Data.ByteString (ByteString)
wenzelm@69465
  1495
import qualified Data.ByteString
wenzelm@69459
  1496
import Data.UUID (UUID)
wenzelm@69459
  1497
import qualified Data.UUID as UUID
wenzelm@69459
  1498
import Data.UUID.V4 (nextRandom)
wenzelm@69459
  1499
wenzelm@69459
  1500
wenzelm@69462
  1501
type T = UUID
wenzelm@69462
  1502
wenzelm@69465
  1503
wenzelm@69465
  1504
{- parse -}
wenzelm@69465
  1505
wenzelm@69465
  1506
parse_string :: String -> Maybe T
wenzelm@69465
  1507
parse_string = UUID.fromString
wenzelm@69465
  1508
wenzelm@69465
  1509
parse_bytes :: ByteString -> Maybe T
wenzelm@69465
  1510
parse_bytes = UUID.fromASCIIBytes
wenzelm@69465
  1511
wenzelm@69465
  1512
wenzelm@69465
  1513
{- print -}
wenzelm@69465
  1514
wenzelm@69465
  1515
string :: T -> String
wenzelm@69465
  1516
string = UUID.toString
wenzelm@69465
  1517
wenzelm@69465
  1518
bytes :: T -> ByteString
wenzelm@69465
  1519
bytes = UUID.toASCIIBytes
wenzelm@69465
  1520
wenzelm@69465
  1521
wenzelm@69465
  1522
{- random id -}
wenzelm@69465
  1523
wenzelm@69462
  1524
random :: IO T
wenzelm@69459
  1525
random = nextRandom
wenzelm@69459
  1526
wenzelm@69459
  1527
random_string :: IO String
wenzelm@69465
  1528
random_string = string <$> random
wenzelm@69459
  1529
wenzelm@69465
  1530
random_bytes :: IO ByteString
wenzelm@69465
  1531
random_bytes = bytes <$> random
wenzelm@69459
  1532
\<close>
wenzelm@69459
  1533
wenzelm@69448
  1534
generate_file "Isabelle/Byte_Message.hs" = \<open>
wenzelm@69448
  1535
{-  Title:      Isabelle/Byte_Message.hs
wenzelm@69446
  1536
    Author:     Makarius
wenzelm@69446
  1537
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69446
  1538
wenzelm@69448
  1539
Byte-oriented messages.
wenzelm@69448
  1540
wenzelm@69448
  1541
See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
wenzelm@69448
  1542
and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
wenzelm@69446
  1543
-}
wenzelm@69446
  1544
wenzelm@69452
  1545
module Isabelle.Byte_Message (
wenzelm@69467
  1546
    write, write_line,
wenzelm@69467
  1547
    read, read_block, trim_line, read_line,
wenzelm@69476
  1548
    make_message, write_message, read_message,
wenzelm@69476
  1549
    make_line_message, write_line_message, read_line_message
wenzelm@69452
  1550
  )
wenzelm@69446
  1551
where
wenzelm@69446
  1552
wenzelm@69449
  1553
import Prelude hiding (read)
wenzelm@69454
  1554
import Data.Maybe
wenzelm@69446
  1555
import Data.ByteString (ByteString)
wenzelm@69446
  1556
import qualified Data.ByteString as ByteString
wenzelm@69446
  1557
import qualified Data.ByteString.UTF8 as UTF8
wenzelm@69446
  1558
import Data.Word (Word8)
wenzelm@69446
  1559
wenzelm@69448
  1560
import Control.Monad (when)
wenzelm@69446
  1561
import Network.Socket (Socket)
wenzelm@69446
  1562
import qualified Network.Socket as Socket
wenzelm@69446
  1563
import qualified Network.Socket.ByteString as ByteString
wenzelm@69446
  1564
wenzelm@69454
  1565
import Isabelle.Library hiding (trim_line)
wenzelm@69446
  1566
import qualified Isabelle.Value as Value
wenzelm@69446
  1567
wenzelm@69446
  1568
wenzelm@69452
  1569
{- output operations -}
wenzelm@69452
  1570
wenzelm@69452
  1571
write :: Socket -> [ByteString] -> IO ()
wenzelm@69452
  1572
write = ByteString.sendMany
wenzelm@69452
  1573
wenzelm@69452
  1574
newline :: ByteString
wenzelm@69452
  1575
newline = ByteString.singleton 10
wenzelm@69452
  1576
wenzelm@69467
  1577
write_line :: Socket -> ByteString -> IO ()
wenzelm@69467
  1578
write_line socket s = write socket [s, newline]
wenzelm@69467
  1579
wenzelm@69452
  1580
wenzelm@69452
  1581
{- input operations -}
wenzelm@69452
  1582
wenzelm@69449
  1583
read :: Socket -> Int -> IO ByteString
wenzelm@69452
  1584
read socket n = read_body 0 []
wenzelm@69449
  1585
  where
wenzelm@69449
  1586
    result = ByteString.concat . reverse
wenzelm@69452
  1587
    read_body len ss =
wenzelm@69449
  1588
      if len >= n then return (result ss)
wenzelm@69449
  1589
      else
wenzelm@69449
  1590
        (do
wenzelm@69449
  1591
          s <- ByteString.recv socket (min (n - len) 8192)
wenzelm@69449
  1592
          case ByteString.length s of
wenzelm@69449
  1593
            0 -> return (result ss)
wenzelm@69452
  1594
            m -> read_body (len + m) (s : ss))
wenzelm@69452
  1595
wenzelm@69452
  1596
read_block :: Socket -> Int -> IO (Maybe ByteString, Int)
wenzelm@69452
  1597
read_block socket n = do
wenzelm@69452
  1598
  msg <- read socket n
wenzelm@69452
  1599
  let len = ByteString.length msg
wenzelm@69452
  1600
  return (if len == n then Just msg else Nothing, len)
wenzelm@69449
  1601
wenzelm@69452
  1602
trim_line :: ByteString -> ByteString
wenzelm@69452
  1603
trim_line s =
wenzelm@69452
  1604
  if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s
wenzelm@69452
  1605
  else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s
wenzelm@69452
  1606
  else s
wenzelm@69452
  1607
  where
wenzelm@69452
  1608
    n = ByteString.length s
wenzelm@69452
  1609
    at = ByteString.index s
wenzelm@69449
  1610
wenzelm@69446
  1611
read_line :: Socket -> IO (Maybe ByteString)
wenzelm@69452
  1612
read_line socket = read_body []
wenzelm@69446
  1613
  where
wenzelm@69452
  1614
    result = trim_line . ByteString.pack . reverse
wenzelm@69452
  1615
    read_body bs = do
wenzelm@69446
  1616
      s <- ByteString.recv socket 1
wenzelm@69446
  1617
      case ByteString.length s of
wenzelm@69446
  1618
        0 -> return (if null bs then Nothing else Just (result bs))
wenzelm@69446
  1619
        1 ->
wenzelm@69446
  1620
          case ByteString.head s of
wenzelm@69446
  1621
            10 -> return (Just (result bs))
wenzelm@69452
  1622
            b -> read_body (b : bs)
wenzelm@69446
  1623
wenzelm@69448
  1624
wenzelm@69454
  1625
{- messages with multiple chunks (arbitrary content) -}
wenzelm@69454
  1626
wenzelm@69454
  1627
make_header :: [Int] -> [ByteString]
wenzelm@69454
  1628
make_header ns =
wenzelm@69454
  1629
  [UTF8.fromString (space_implode "," (map Value.print_int ns)), newline]
wenzelm@69454
  1630
wenzelm@69476
  1631
make_message :: [ByteString] -> [ByteString]
wenzelm@69476
  1632
make_message chunks = make_header (map ByteString.length chunks) ++ chunks
wenzelm@69476
  1633
wenzelm@69454
  1634
write_message :: Socket -> [ByteString] -> IO ()
wenzelm@69476
  1635
write_message socket = write socket . make_message
wenzelm@69454
  1636
wenzelm@69454
  1637
parse_header :: ByteString -> [Int]
wenzelm@69454
  1638
parse_header line =
wenzelm@69454
  1639
  let
wenzelm@69454
  1640
    res = map Value.parse_nat (space_explode ',' (UTF8.toString line))
wenzelm@69454
  1641
  in
wenzelm@69454
  1642
    if all isJust res then map fromJust res
wenzelm@69454
  1643
    else error ("Malformed message header: " ++ quote (UTF8.toString line))
wenzelm@69454
  1644
wenzelm@69454
  1645
read_chunk :: Socket -> Int -> IO ByteString
wenzelm@69454
  1646
read_chunk socket n = do
wenzelm@69454
  1647
  res <- read_block socket n
wenzelm@69454
  1648
  return $
wenzelm@69454
  1649
    case res of
wenzelm@69454
  1650
      (Just chunk, _) -> chunk
wenzelm@69454
  1651
      (Nothing, len) ->
wenzelm@69454
  1652
        error ("Malformed message chunk: unexpected EOF after " ++
wenzelm@69454
  1653
          show len ++ " of " ++ show n ++ " bytes")
wenzelm@69454
  1654
wenzelm@69454
  1655
read_message :: Socket -> IO (Maybe [ByteString])
wenzelm@69454
  1656
read_message socket = do
wenzelm@69454
  1657
  res <- read_line socket
wenzelm@69454
  1658
  case res of
wenzelm@69454
  1659
    Just line -> Just <$> mapM (read_chunk socket) (parse_header line)
wenzelm@69454
  1660
    Nothing -> return Nothing
wenzelm@69454
  1661
wenzelm@69454
  1662
wenzelm@69448
  1663
-- hybrid messages: line or length+block (with content restriction)
wenzelm@69448
  1664
wenzelm@69448
  1665
is_length :: ByteString -> Bool
wenzelm@69452
  1666
is_length msg =
wenzelm@69452
  1667
  not (ByteString.null msg) && ByteString.all (\b -> 48 <= b && b <= 57) msg
wenzelm@69446
  1668
wenzelm@69452
  1669
is_terminated :: ByteString -> Bool
wenzelm@69452
  1670
is_terminated msg =
wenzelm@69452
  1671
  not (ByteString.null msg) && (ByteString.last msg == 13 || ByteString.last msg == 10)
wenzelm@69448
  1672
wenzelm@69476
  1673
make_line_message :: ByteString -> [ByteString]
wenzelm@69476
  1674
make_line_message msg =
wenzelm@69476
  1675
  let n = ByteString.length msg in
wenzelm@69476
  1676
    if is_length msg || is_terminated msg then
wenzelm@69476
  1677
      error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
wenzelm@69476
  1678
    else
wenzelm@69476
  1679
      (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) ++
wenzelm@69476
  1680
      [msg, newline]
wenzelm@69448
  1681
wenzelm@69476
  1682
write_line_message :: Socket -> ByteString -> IO ()
wenzelm@69476
  1683
write_line_message socket = write socket . make_line_message
wenzelm@69448
  1684
wenzelm@69448
  1685
read_line_message :: Socket -> IO (Maybe ByteString)
wenzelm@69448
  1686
read_line_message socket = do
wenzelm@69446
  1687
  opt_line <- read_line socket
wenzelm@69446
  1688
  case opt_line of
wenzelm@69446
  1689
    Nothing -> return Nothing
wenzelm@69446
  1690
    Just line ->
wenzelm@69452
  1691
      case Value.parse_nat (UTF8.toString line) of
wenzelm@69446
  1692
        Nothing -> return $ Just line
wenzelm@69452
  1693
        Just n -> fmap trim_line . fst <$> read_block socket n
wenzelm@69446
  1694
\<close>
wenzelm@69446
  1695
wenzelm@69473
  1696
generate_file "Isabelle/Standard_Thread.hs" = \<open>
wenzelm@69473
  1697
{-  Title:      Isabelle/Standard_Thread.hs
wenzelm@69473
  1698
    Author:     Makarius
wenzelm@69473
  1699
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69473
  1700
wenzelm@69473
  1701
Standard thread operations.
wenzelm@69473
  1702
wenzelm@69473
  1703
See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.ML\<close>
wenzelm@69473
  1704
and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.scala\<close>.
wenzelm@69473
  1705
-}
wenzelm@69473
  1706
wenzelm@69473
  1707
{-# LANGUAGE NamedFieldPuns #-}
wenzelm@69473
  1708
wenzelm@69473
  1709
module Isabelle.Standard_Thread (
wenzelm@69473
  1710
  ThreadId, Result,
wenzelm@69494
  1711
  find_id,
wenzelm@69473
  1712
  properties, change_properties,
wenzelm@69499
  1713
  add_resource, del_resource, bracket_resource,
wenzelm@69497
  1714
  is_stopped, expose_stopped, stop,
wenzelm@69496
  1715
  my_uuid, stop_uuid,
wenzelm@69494
  1716
  Fork, fork_finally, fork)
wenzelm@69473
  1717
where
wenzelm@69473
  1718
wenzelm@69499
  1719
import Data.Unique
wenzelm@69473
  1720
import Data.Maybe
wenzelm@69473
  1721
import Data.IORef
wenzelm@69473
  1722
import System.IO.Unsafe
wenzelm@69473
  1723
wenzelm@69494
  1724
import qualified Data.List as List
wenzelm@69497
  1725
import Control.Monad (when, forM_)
wenzelm@69473
  1726
import Data.Map.Strict (Map)
wenzelm@69473
  1727
import qualified Data.Map.Strict as Map
wenzelm@69473
  1728
import Control.Exception.Base (SomeException)
wenzelm@69473
  1729
import Control.Exception as Exception
wenzelm@69473
  1730
import Control.Concurrent (ThreadId)
wenzelm@69473
  1731
import qualified Control.Concurrent as Concurrent
wenzelm@69473
  1732
import Control.Concurrent.Thread (Result)
wenzelm@69473
  1733
import qualified Control.Concurrent.Thread as Thread
wenzelm@69494
  1734
import qualified Isabelle.UUID as UUID
wenzelm@69473
  1735
import qualified Isabelle.Properties as Properties
wenzelm@69473
  1736
wenzelm@69473
  1737
wenzelm@69473
  1738
{- thread info -}
wenzelm@69473
  1739
wenzelm@69499
  1740
type Resources = Map Unique (IO ())
wenzelm@69499
  1741
data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool, resources :: Resources}
wenzelm@69473
  1742
type Infos = Map ThreadId Info
wenzelm@69473
  1743
wenzelm@69473
  1744
lookup_info :: Infos -> ThreadId -> Maybe Info
wenzelm@69494
  1745
lookup_info infos id = Map.lookup id infos
wenzelm@69494
  1746
wenzelm@69494
  1747
init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ())
wenzelm@69499
  1748
init_info id uuid infos = (Map.insert id (Info uuid [] False Map.empty) infos, ())
wenzelm@69473
  1749
wenzelm@69473
  1750
wenzelm@69473
  1751
{- global state -}
wenzelm@69473
  1752
wenzelm@69473
  1753
{-# NOINLINE global_state #-}
wenzelm@69473
  1754
global_state :: IORef Infos
wenzelm@69473
  1755
global_state = unsafePerformIO (newIORef Map.empty)
wenzelm@69473
  1756
wenzelm@69494
  1757
find_id :: UUID.T -> IO (Maybe ThreadId)
wenzelm@69494
  1758
find_id uuid = do
wenzelm@69494
  1759
  state <- readIORef global_state
wenzelm@69494
  1760
  return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state)
wenzelm@69494
  1761
wenzelm@69473
  1762
get_info :: ThreadId -> IO (Maybe Info)
wenzelm@69473
  1763
get_info id = do
wenzelm@69473
  1764
  state <- readIORef global_state
wenzelm@69473
  1765
  return $ lookup_info state id
wenzelm@69473
  1766
wenzelm@69499
  1767
map_info :: ThreadId -> (Info -> Info) -> IO (Maybe Info)
wenzelm@69473
  1768
map_info id f =
wenzelm@69473
  1769
  atomicModifyIORef' global_state
wenzelm@69473
  1770
    (\infos ->
wenzelm@69473
  1771
      case lookup_info infos id of
wenzelm@69499
  1772
        Nothing -> (infos, Nothing)
wenzelm@69499
  1773
        Just info ->
wenzelm@69499
  1774
          let info' = f info
wenzelm@69499
  1775
          in (Map.insert id info' infos, Just info'))
wenzelm@69473
  1776
wenzelm@69495
  1777
delete_info :: ThreadId -> IO ()
wenzelm@69495
  1778
delete_info id =
wenzelm@69495
  1779
  atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ()))
wenzelm@69495
  1780
wenzelm@69473
  1781
wenzelm@69473
  1782
{- thread properties -}
wenzelm@69473
  1783
wenzelm@69498
  1784
my_info :: IO (Maybe Info)
wenzelm@69473
  1785
my_info = do
wenzelm@69473
  1786
  id <- Concurrent.myThreadId
wenzelm@69498
  1787
  get_info id
wenzelm@69473
  1788
wenzelm@69473
  1789
properties :: IO Properties.T
wenzelm@69498
  1790
properties = maybe [] props <$> my_info
wenzelm@69473
  1791
wenzelm@69473
  1792
change_properties :: (Properties.T -> Properties.T) -> IO ()
wenzelm@69473
  1793
change_properties f = do
wenzelm@69473
  1794
  id <- Concurrent.myThreadId
wenzelm@69473
  1795
  map_info id (\info -> info {props = f (props info)})
wenzelm@69499
  1796
  return ()
wenzelm@69499
  1797
wenzelm@69499
  1798
wenzelm@69499
  1799
{- managed resources -}
wenzelm@69499
  1800
wenzelm@69499
  1801
add_resource :: IO () -> IO Unique
wenzelm@69499
  1802
add_resource resource = do
wenzelm@69499
  1803
  id <- Concurrent.myThreadId
wenzelm@69499
  1804
  u <- newUnique
wenzelm@69499
  1805
  map_info id (\info -> info {resources = Map.insert u resource (resources info)})
wenzelm@69499
  1806
  return u
wenzelm@69499
  1807
wenzelm@69499
  1808
del_resource :: Unique -> IO ()
wenzelm@69499
  1809
del_resource u = do
wenzelm@69499
  1810
  id <- Concurrent.myThreadId
wenzelm@69499
  1811
  map_info id (\info -> info {resources = Map.delete u (resources info)})
wenzelm@69499
  1812
  return ()
wenzelm@69499
  1813
wenzelm@69499
  1814
bracket_resource :: IO () -> IO a -> IO a
wenzelm@69499
  1815
bracket_resource resource body =
wenzelm@69499
  1816
  Exception.bracket (add_resource resource) del_resource (const body)
wenzelm@69473
  1817
wenzelm@69473
  1818
wenzelm@69473
  1819
{- stop -}
wenzelm@69473
  1820
wenzelm@69473
  1821
is_stopped :: IO Bool
wenzelm@69498
  1822
is_stopped = maybe False stopped <$> my_info
wenzelm@69473
  1823
wenzelm@69497
  1824
expose_stopped :: IO ()
wenzelm@69497
  1825
expose_stopped = do
wenzelm@69497
  1826
  stopped <- is_stopped
wenzelm@69497
  1827
  when stopped $ throw ThreadKilled
wenzelm@69497
  1828
wenzelm@69473
  1829
stop :: ThreadId -> IO ()
wenzelm@69499
  1830
stop id = do
wenzelm@69499
  1831
  info <- map_info id (\info -> info {stopped = True})
wenzelm@69499
  1832
  let ops = case info of Nothing -> []; Just Info{resources} -> map snd (Map.toDescList resources)
wenzelm@69499
  1833
  sequence_ ops
wenzelm@69473
  1834
wenzelm@69473
  1835
wenzelm@69496
  1836
{- UUID -}
wenzelm@69496
  1837
wenzelm@69498
  1838
my_uuid :: IO (Maybe UUID.T)
wenzelm@69498
  1839
my_uuid = fmap uuid <$> my_info
wenzelm@69496
  1840
wenzelm@69496
  1841
stop_uuid :: UUID.T -> IO ()
wenzelm@69496
  1842
stop_uuid uuid = do
wenzelm@69496
  1843
  id <- find_id uuid
wenzelm@69496
  1844
  forM_ id stop
wenzelm@69496
  1845
wenzelm@69496
  1846
wenzelm@69473
  1847
{- fork -}
wenzelm@69473
  1848
wenzelm@69494
  1849
type Fork a = (ThreadId, UUID.T, IO (Result a))
wenzelm@69494
  1850
wenzelm@69494
  1851
fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b)
wenzelm@69473
  1852
fork_finally body finally = do
wenzelm@69494
  1853
  uuid <- UUID.random
wenzelm@69473
  1854
  (id, result) <-
wenzelm@69473
  1855
    Exception.mask (\restore ->
wenzelm@69473
  1856
      Thread.forkIO
wenzelm@69473
  1857
        (Exception.try
wenzelm@69473
  1858
          (do
wenzelm@69473
  1859
            id <- Concurrent.myThreadId
wenzelm@69494
  1860
            atomicModifyIORef' global_state (init_info id uuid)
wenzelm@69495
  1861
            restore body)
wenzelm@69495
  1862
         >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res)))
wenzelm@69494
  1863
  return (id, uuid, result)
wenzelm@69494
  1864
wenzelm@69494
  1865
fork :: IO a -> IO (Fork a)
wenzelm@69473
  1866
fork body = fork_finally body Thread.result
wenzelm@69473
  1867
\<close>
wenzelm@69473
  1868
wenzelm@69455
  1869
generate_file "Isabelle/Server.hs" = \<open>
wenzelm@69455
  1870
{-  Title:      Isabelle/Server.hs
wenzelm@69455
  1871
    Author:     Makarius
wenzelm@69455
  1872
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69455
  1873
wenzelm@69455
  1874
TCP server on localhost.
wenzelm@69455
  1875
-}
wenzelm@69455
  1876
wenzelm@69465
  1877
module Isabelle.Server (
wenzelm@69465
  1878
  localhost_name, localhost, publish_text, publish_stdout,
wenzelm@69465
  1879
  server
wenzelm@69465
  1880
)
wenzelm@69465
  1881
where
wenzelm@69455
  1882
wenzelm@69465
  1883
import Data.ByteString (ByteString)
wenzelm@69465
  1884
import Control.Monad (forever, when)
wenzelm@69455
  1885
import qualified Control.Exception as Exception
wenzelm@69455
  1886
import Network.Socket (Socket)
wenzelm@69455
  1887
import qualified Network.Socket as Socket
wenzelm@69472
  1888
import qualified System.IO as IO
wenzelm@69455
  1889
wenzelm@69462
  1890
import Isabelle.Library
wenzelm@69462
  1891
import qualified Isabelle.UUID as UUID
wenzelm@69465
  1892
import qualified Isabelle.Byte_Message as Byte_Message
wenzelm@69473
  1893
import qualified Isabelle.Standard_Thread as Standard_Thread
wenzelm@69462
  1894
wenzelm@69462
  1895
wenzelm@69462
  1896
{- server address -}
wenzelm@69455
  1897
wenzelm@69463
  1898
localhost_name :: String
wenzelm@69463
  1899
localhost_name = "127.0.0.1"
wenzelm@69463
  1900
wenzelm@69455
  1901
localhost :: Socket.HostAddress
wenzelm@69455
  1902
localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
wenzelm@69455
  1903
wenzelm@69462
  1904
publish_text :: String -> String -> UUID.T -> String
wenzelm@69462
  1905
publish_text name address password =
wenzelm@69462
  1906
  "server " ++ quote name ++ " = " ++ address ++ " (password " ++ quote (show password) ++ ")"
wenzelm@69462
  1907
wenzelm@69462
  1908
publish_stdout :: String -> String -> UUID.T -> IO ()
wenzelm@69462
  1909
publish_stdout name address password = putStrLn (publish_text name address password)
wenzelm@69462
  1910
wenzelm@69462
  1911
wenzelm@69462
  1912
{- server -}
wenzelm@69462
  1913
wenzelm@69462
  1914
server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
wenzelm@69455
  1915
server publish handle =
wenzelm@69462
  1916
  Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
wenzelm@69455
  1917
  where
wenzelm@69465
  1918
    open :: IO (Socket, ByteString)
wenzelm@69455
  1919
    open = do
wenzelm@69466
  1920
      server_socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol
wenzelm@69466
  1921
      Socket.bind server_socket (Socket.SockAddrInet 0 localhost)
wenzelm@69466
  1922
      Socket.listen server_socket 50
wenzelm@69462
  1923
wenzelm@69466
  1924
      port <- Socket.socketPort server_socket
wenzelm@69462
  1925
      let address = localhost_name ++ ":" ++ show port
wenzelm@69462
  1926
      password <- UUID.random
wenzelm@69462
  1927
      publish address password
wenzelm@69455
  1928
wenzelm@69466
  1929
      return (server_socket, UUID.bytes password)
wenzelm@69462
  1930
wenzelm@69465
  1931
    loop :: Socket -> ByteString -> IO ()
wenzelm@69466
  1932
    loop server_socket password = forever $ do
wenzelm@69480
  1933
      (connection, _) <- Socket.accept server_socket
wenzelm@69473
  1934
      Standard_Thread.fork_finally
wenzelm@69465
  1935
        (do
wenzelm@69465
  1936
          line <- Byte_Message.read_line connection
wenzelm@69465
  1937
          when (line == Just password) $ handle connection)
wenzelm@69473
  1938
        (\finally -> do
wenzelm@69472
  1939
          Socket.close connection
wenzelm@69473
  1940
          case finally of
wenzelm@69472
  1941
            Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn
wenzelm@69472
  1942
            Right () -> return ())
wenzelm@69455
  1943
      return ()
wenzelm@69455
  1944
\<close>
wenzelm@69455
  1945
wenzelm@69662
  1946
export_generated_files
wenzelm@69628
  1947
wenzelm@69222
  1948
end