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