wenzelm@69222: (*  Title:      Tools/Haskell/Haskell.thy
wenzelm@69222:     Author:     Makarius
wenzelm@69225: 
wenzelm@69225: Support for Isabelle tools in Haskell.
wenzelm@69222: *)
wenzelm@69222: 
wenzelm@69222: theory Haskell
wenzelm@69222:   imports Pure
wenzelm@69222: begin
wenzelm@69222: 
wenzelm@69490: generate_file "Isabelle/Symbol.hs" = \<open>
wenzelm@69490: {-  Title:      Isabelle/Symbols.hs
wenzelm@69490:     Author:     Makarius
wenzelm@69490:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69490: 
wenzelm@69490: Isabelle text symbols.
wenzelm@69490: -}
wenzelm@69490: 
wenzelm@69490: module Isabelle.Symbol where
wenzelm@69490: 
wenzelm@69490: {- ASCII characters -}
wenzelm@69490: 
wenzelm@69490: is_ascii_letter :: Char -> Bool
wenzelm@69490: is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
wenzelm@69490: 
wenzelm@69490: is_ascii_digit :: Char -> Bool
wenzelm@69490: is_ascii_digit c = '0' <= c && c <= '9'
wenzelm@69490: 
wenzelm@69490: is_ascii_hex :: Char -> Bool
wenzelm@69490: is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
wenzelm@69490: 
wenzelm@69490: is_ascii_quasi :: Char -> Bool
wenzelm@69490: is_ascii_quasi c = c == '_' || c == '\''
wenzelm@69490: 
wenzelm@69490: is_ascii_blank :: Char -> Bool
wenzelm@69490: is_ascii_blank c = c `elem` " \t\n\11\f\r"
wenzelm@69490: 
wenzelm@69490: is_ascii_line_terminator :: Char -> Bool
wenzelm@69490: is_ascii_line_terminator c = c == '\r' || c == '\n'
wenzelm@69490: 
wenzelm@69490: is_ascii_letdig :: Char -> Bool
wenzelm@69490: is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
wenzelm@69490: 
wenzelm@69490: is_ascii_identifier :: String -> Bool
wenzelm@69490: is_ascii_identifier s =
wenzelm@69490:   not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
wenzelm@69490: \<close>
wenzelm@69490: 
wenzelm@69444: generate_file "Isabelle/Library.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Library.hs
wenzelm@69225:     Author:     Makarius
wenzelm@69225:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225: 
wenzelm@69225: Basic library of Isabelle idioms.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/basics.ML\<close>, \<^file>\<open>$ISABELLE_HOME/src/Pure/library.ML\<close>.
wenzelm@69225: -}
wenzelm@69225: 
wenzelm@69240: module Isabelle.Library (
wenzelm@69240:   (|>), (|->), (#>), (#->),
wenzelm@69240: 
wenzelm@69240:   the, the_default,
wenzelm@69240: 
wenzelm@69240:   fold, fold_rev, single, map_index, get_index,
wenzelm@69240: 
wenzelm@69477:   proper_string, quote, space_implode, commas, commas_quote, cat_lines,
wenzelm@69453:   space_explode, split_lines, trim_line, clean_name)
wenzelm@69225: where
wenzelm@69225: 
wenzelm@69234: import Data.Maybe
wenzelm@69453: import qualified Data.List as List
wenzelm@69453: import qualified Data.List.Split as Split
wenzelm@69491: import qualified Isabelle.Symbol as Symbol
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69225: {- functions -}
wenzelm@69225: 
wenzelm@69225: (|>) :: a -> (a -> b) -> b
wenzelm@69225: x |> f = f x
wenzelm@69225: 
wenzelm@69225: (|->) :: (a, b) -> (a -> b -> c) -> c
wenzelm@69225: (x, y) |-> f = f x y
wenzelm@69225: 
wenzelm@69225: (#>) :: (a -> b) -> (b -> c) -> a -> c
wenzelm@69225: (f #> g) x = x |> f |> g
wenzelm@69225: 
wenzelm@69225: (#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
wenzelm@69225: (f #-> g) x  = x |> f |-> g
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69234: {- options -}
wenzelm@69234: 
wenzelm@69240: the :: Maybe a -> a
wenzelm@69240: the (Just x) = x
wenzelm@69240: the Nothing = error "the Nothing"
wenzelm@69240: 
wenzelm@69234: the_default :: a -> Maybe a -> a
wenzelm@69234: the_default x Nothing = x
wenzelm@69234: the_default _ (Just y) = y
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69225: {- lists -}
wenzelm@69225: 
wenzelm@69225: fold :: (a -> b -> b) -> [a] -> b -> b
wenzelm@69225: fold _ [] y = y
wenzelm@69225: fold f (x : xs) y = fold f xs (f x y)
wenzelm@69225: 
wenzelm@69225: fold_rev :: (a -> b -> b) -> [a] -> b -> b
wenzelm@69225: fold_rev _ [] y = y
wenzelm@69225: fold_rev f (x : xs) y = f x (fold_rev f xs y)
wenzelm@69225: 
wenzelm@69225: single :: a -> [a]
wenzelm@69225: single x = [x]
wenzelm@69225: 
wenzelm@69240: map_index :: ((Int, a) -> b) -> [a] -> [b]
wenzelm@69240: map_index f = map_aux 0
wenzelm@69240:   where
wenzelm@69240:     map_aux _ [] = []
wenzelm@69240:     map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
wenzelm@69240: 
wenzelm@69240: get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
wenzelm@69240: get_index f = get_aux 0
wenzelm@69240:   where
wenzelm@69240:     get_aux _ [] = Nothing
wenzelm@69240:     get_aux i (x : xs) =
wenzelm@69240:       case f x of
wenzelm@69240:         Nothing -> get_aux (i + 1) xs
wenzelm@69240:         Just y -> Just (i, y)
wenzelm@69240: 
wenzelm@69225: 
wenzelm@69225: {- strings -}
wenzelm@69225: 
wenzelm@69477: proper_string :: String -> Maybe String
wenzelm@69477: proper_string s = if null s then Nothing else Just s
wenzelm@69477: 
wenzelm@69225: quote :: String -> String
wenzelm@69225: quote s = "\"" ++ s ++ "\""
wenzelm@69225: 
wenzelm@69453: space_implode :: String -> [String] -> String
wenzelm@69453: space_implode = List.intercalate
wenzelm@69453: 
wenzelm@69453: commas, commas_quote :: [String] -> String
wenzelm@69453: commas = space_implode ", "
wenzelm@69453: commas_quote = commas . map quote
wenzelm@69453: 
wenzelm@69453: cat_lines :: [String] -> String
wenzelm@69453: cat_lines = space_implode "\n"
wenzelm@69453: 
wenzelm@69453: 
wenzelm@69453: space_explode :: Char -> String -> [String]
wenzelm@69453: space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
wenzelm@69453: 
wenzelm@69453: split_lines :: String -> [String]
wenzelm@69453: split_lines = space_explode '\n'
wenzelm@69453: 
wenzelm@69225: trim_line :: String -> String
wenzelm@69225: trim_line line =
wenzelm@69491:   if not (null line) && Symbol.is_ascii_line_terminator (last line) then
wenzelm@69486:     case reverse line of
wenzelm@69486:       '\n' : '\r' : rest -> reverse rest
wenzelm@69486:       '\r' : rest -> reverse rest
wenzelm@69486:       '\n' : rest -> reverse rest
wenzelm@69486:       _ -> line
wenzelm@69486:   else line
wenzelm@69288: 
wenzelm@69288: clean_name :: String -> String
wenzelm@69288: clean_name = reverse #> dropWhile (== '_') #> reverse
wenzelm@69225: \<close>
wenzelm@69225: 
wenzelm@69444: generate_file "Isabelle/Value.hs" = \<open>
wenzelm@69233: {-  Title:      Haskell/Tools/Value.hs
wenzelm@69233:     Author:     Makarius
wenzelm@69233:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69233: 
wenzelm@69233: Plain values, represented as string.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/value.ML\<close>.
wenzelm@69233: -}
wenzelm@69233: 
wenzelm@69233: module Isabelle.Value
wenzelm@69452:   (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
wenzelm@69233: where
wenzelm@69233: 
wenzelm@69233: import Data.Maybe
wenzelm@69233: import qualified Data.List as List
wenzelm@69233: import qualified Text.Read as Read
wenzelm@69233: 
wenzelm@69233: 
wenzelm@69233: {- bool -}
wenzelm@69233: 
wenzelm@69233: print_bool :: Bool -> String
wenzelm@69233: print_bool True = "true"
wenzelm@69233: print_bool False = "false"
wenzelm@69233: 
wenzelm@69233: parse_bool :: String -> Maybe Bool
wenzelm@69233: parse_bool "true" = Just True
wenzelm@69233: parse_bool "false" = Just False
wenzelm@69233: parse_bool _ = Nothing
wenzelm@69233: 
wenzelm@69233: 
wenzelm@69452: {- nat -}
wenzelm@69452: 
wenzelm@69452: parse_nat :: String -> Maybe Int
wenzelm@69452: parse_nat s =
wenzelm@69452:   case Read.readMaybe s of
wenzelm@69452:     Just n | n >= 0 -> Just n
wenzelm@69452:     _ -> Nothing
wenzelm@69452: 
wenzelm@69452: 
wenzelm@69233: {- int -}
wenzelm@69233: 
wenzelm@69233: print_int :: Int -> String
wenzelm@69233: print_int = show
wenzelm@69233: 
wenzelm@69233: parse_int :: String -> Maybe Int
wenzelm@69233: parse_int = Read.readMaybe
wenzelm@69233: 
wenzelm@69233: 
wenzelm@69233: {- real -}
wenzelm@69233: 
wenzelm@69233: print_real :: Double -> String
wenzelm@69233: print_real x =
wenzelm@69233:   let s = show x in
wenzelm@69233:     case span (/= '.') s of
wenzelm@69233:       (a, '.' : b) | List.all (== '0') b -> a
wenzelm@69233:       _ -> s
wenzelm@69233: 
wenzelm@69233: parse_real :: String -> Maybe Double
wenzelm@69233: parse_real = Read.readMaybe
wenzelm@69233: \<close>
wenzelm@69233: 
wenzelm@69444: generate_file "Isabelle/Buffer.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Buffer.hs
wenzelm@69225:     Author:     Makarius
wenzelm@69225:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225: 
wenzelm@69225: Efficient text buffers.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
wenzelm@69225: -}
wenzelm@69222: 
wenzelm@69225: module Isabelle.Buffer (T, empty, add, content)
wenzelm@69225: where
wenzelm@69225: 
wenzelm@69474: import Isabelle.Library
wenzelm@69474: 
wenzelm@69474: 
wenzelm@69474: newtype T = Buffer [Char]
wenzelm@69225: 
wenzelm@69225: empty :: T
wenzelm@69225: empty = Buffer []
wenzelm@69225: 
wenzelm@69225: add :: String -> T -> T
wenzelm@69474: add s (Buffer cs) = Buffer (fold (:) s cs)
wenzelm@69225: 
wenzelm@69225: content :: T -> String
wenzelm@69474: content (Buffer cs) = reverse cs
wenzelm@69225: \<close>
wenzelm@69225: 
wenzelm@69444: generate_file "Isabelle/Properties.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Properties.hs
wenzelm@69225:     Author:     Makarius
wenzelm@69225:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225: 
wenzelm@69225: Property lists.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
wenzelm@69225: -}
wenzelm@69225: 
wenzelm@69477: module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
wenzelm@69225: where
wenzelm@69225: 
wenzelm@69225: import qualified Data.List as List
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69225: type Entry = (String, String)
wenzelm@69225: type T = [Entry]
wenzelm@69225: 
wenzelm@69225: defined :: T -> String -> Bool
wenzelm@69225: defined props name = any (\(a, _) -> a == name) props
wenzelm@69225: 
wenzelm@69225: get :: T -> String -> Maybe String
wenzelm@69225: get props name = List.lookup name props
wenzelm@69225: 
wenzelm@69477: get_value :: (String -> Maybe a) -> T -> String -> Maybe a
wenzelm@69477: get_value parse props name =
wenzelm@69477:   case get props name of
wenzelm@69477:     Nothing -> Nothing
wenzelm@69477:     Just s -> parse s
wenzelm@69477: 
wenzelm@69225: put :: Entry -> T -> T
wenzelm@69225: put entry props = entry : remove (fst entry) props
wenzelm@69225: 
wenzelm@69225: remove :: String -> T -> T
wenzelm@69225: remove name props =
wenzelm@69225:   if defined props name then filter (\(a, _) -> a /= name) props
wenzelm@69225:   else props
wenzelm@69225: \<close>
wenzelm@69225: 
wenzelm@69444: generate_file "Isabelle/Markup.hs" = \<open>
wenzelm@69226: {-  Title:      Haskell/Tools/Markup.hs
wenzelm@69225:     Author:     Makarius
wenzelm@69225:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225: 
wenzelm@69225: Quasi-abstract markup elements.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>.
wenzelm@69225: -}
wenzelm@69225: 
wenzelm@69234: module Isabelle.Markup (
wenzelm@69234:   T, empty, is_empty, properties,
wenzelm@69234: 
wenzelm@69234:   nameN, name, xnameN, xname, kindN,
wenzelm@69234: 
wenzelm@69315:   bindingN, binding, entityN, entity, defN, refN,
wenzelm@69315: 
wenzelm@69288:   completionN, completion, no_completionN, no_completion,
wenzelm@69288: 
wenzelm@69234:   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
wenzelm@69234: 
wenzelm@69291:   expressionN, expression,
wenzelm@69291: 
wenzelm@69291:   citationN, citation,
wenzelm@69291: 
wenzelm@69291:   pathN, urlN, docN,
wenzelm@69291: 
wenzelm@69248:   markupN, consistentN, unbreakableN, indentN, widthN,
wenzelm@69248:   blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
wenzelm@69248: 
wenzelm@69968:   wordsN, words,
wenzelm@69234: 
wenzelm@69234:   tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
wenzelm@69234:   numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
wenzelm@69320:   inner_cartoucheN, inner_cartouche,
wenzelm@69234:   token_rangeN, token_range,
wenzelm@69234:   sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
wenzelm@69234: 
wenzelm@69234:   antiquotedN, antiquoted, antiquoteN, antiquote,
wenzelm@69234: 
wenzelm@69234:   paragraphN, paragraph, text_foldN, text_fold,
wenzelm@69234: 
wenzelm@69234:   keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
wenzelm@69234:   improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
wenzelm@69320:   verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
wenzelm@69320:   comment2N, comment2, comment3N, comment3,
wenzelm@69234: 
wenzelm@69794:   acceptedN, accepted, forkedN, forked, joinedN, joined, runningN, running, finishedN, finished,
wenzelm@69794:   failedN, failed, canceledN, canceled, initializedN, initialized, finalizedN, finalized,
wenzelm@69794:   consolidatedN, consolidated,
wenzelm@69794: 
wenzelm@69234:   writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
wenzelm@69234:   warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
wenzelm@69234: 
wenzelm@69234:   intensifyN, intensify,
wenzelm@69234:   Output, no_output)
wenzelm@69225: where
wenzelm@69225: 
wenzelm@69248: import Prelude hiding (words, error, break)
wenzelm@69234: 
wenzelm@69234: import Isabelle.Library
wenzelm@69225: import qualified Isabelle.Properties as Properties
wenzelm@69248: import qualified Isabelle.Value as Value
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69234: {- basic markup -}
wenzelm@69234: 
wenzelm@69225: type T = (String, Properties.T)
wenzelm@69225: 
wenzelm@69225: empty :: T
wenzelm@69225: empty = ("", [])
wenzelm@69225: 
wenzelm@69225: is_empty :: T -> Bool
wenzelm@69225: is_empty ("", _) = True
wenzelm@69225: is_empty _ = False
wenzelm@69225: 
wenzelm@69234: properties :: Properties.T -> T -> T
wenzelm@69234: properties more_props (elem, props) =
wenzelm@69234:   (elem, fold_rev Properties.put more_props props)
wenzelm@69234: 
wenzelm@69234: markup_elem name = (name, (name, []) :: T)
wenzelm@69291: markup_string name prop = (name, \s -> (name, [(prop, s)]) :: T)
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: {- misc properties -}
wenzelm@69234: 
wenzelm@69234: nameN :: String
wenzelm@69234: nameN = \<open>Markup.nameN\<close>
wenzelm@69234: 
wenzelm@69234: name :: String -> T -> T
wenzelm@69234: name a = properties [(nameN, a)]
wenzelm@69234: 
wenzelm@69234: xnameN :: String
wenzelm@69234: xnameN = \<open>Markup.xnameN\<close>
wenzelm@69234: 
wenzelm@69234: xname :: String -> T -> T
wenzelm@69234: xname a = properties [(xnameN, a)]
wenzelm@69234: 
wenzelm@69234: kindN :: String
wenzelm@69234: kindN = \<open>Markup.kindN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69315: {- formal entities -}
wenzelm@69315: 
wenzelm@69315: bindingN :: String; binding :: T
wenzelm@69315: (bindingN, binding) = markup_elem \<open>Markup.bindingN\<close>
wenzelm@69315: 
wenzelm@69315: entityN :: String; entity :: String -> String -> T
wenzelm@69315: entityN = \<open>Markup.entityN\<close>
wenzelm@69315: entity kind name =
wenzelm@69315:   (entityN,
wenzelm@69315:     (if null name then [] else [(nameN, name)]) ++ (if null kind then [] else [(kindN, kind)]))
wenzelm@69315: 
wenzelm@69315: defN :: String
wenzelm@69315: defN = \<open>Markup.defN\<close>
wenzelm@69315: 
wenzelm@69315: refN :: String
wenzelm@69315: refN = \<open>Markup.refN\<close>
wenzelm@69315: 
wenzelm@69315: 
wenzelm@69288: {- completion -}
wenzelm@69288: 
wenzelm@69288: completionN :: String; completion :: T
wenzelm@69288: (completionN, completion) = markup_elem \<open>Markup.completionN\<close>
wenzelm@69288: 
wenzelm@69288: no_completionN :: String; no_completion :: T
wenzelm@69288: (no_completionN, no_completion) = markup_elem \<open>Markup.no_completionN\<close>
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69234: {- position -}
wenzelm@69234: 
wenzelm@69234: lineN, end_lineN :: String
wenzelm@69234: lineN = \<open>Markup.lineN\<close>
wenzelm@69234: end_lineN = \<open>Markup.end_lineN\<close>
wenzelm@69234: 
wenzelm@69234: offsetN, end_offsetN :: String
wenzelm@69234: offsetN = \<open>Markup.offsetN\<close>
wenzelm@69234: end_offsetN = \<open>Markup.end_offsetN\<close>
wenzelm@69234: 
wenzelm@69234: fileN, idN :: String
wenzelm@69234: fileN = \<open>Markup.fileN\<close>
wenzelm@69234: idN = \<open>Markup.idN\<close>
wenzelm@69234: 
wenzelm@69234: positionN :: String; position :: T
wenzelm@69234: (positionN, position) = markup_elem \<open>Markup.positionN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69291: {- expression -}
wenzelm@69291: 
wenzelm@69291: expressionN :: String
wenzelm@69291: expressionN = \<open>Markup.expressionN\<close>
wenzelm@69291: 
wenzelm@69291: expression :: String -> T
wenzelm@69291: expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
wenzelm@69291: 
wenzelm@69291: 
wenzelm@69291: {- citation -}
wenzelm@69291: 
wenzelm@69291: citationN :: String; citation :: String -> T
wenzelm@69291: (citationN, citation) = markup_string \<open>Markup.citationN\<close> nameN
wenzelm@69291: 
wenzelm@69291: 
wenzelm@69291: {- external resources -}
wenzelm@69291: 
wenzelm@69291: pathN :: String; path :: String -> T
wenzelm@69291: (pathN, path) = markup_string \<open>Markup.pathN\<close> nameN
wenzelm@69291: 
wenzelm@69291: urlN :: String; url :: String -> T
wenzelm@69291: (urlN, url) = markup_string \<open>Markup.urlN\<close> nameN
wenzelm@69291: 
wenzelm@69291: docN :: String; doc :: String -> T
wenzelm@69291: (docN, doc) = markup_string \<open>Markup.docN\<close> nameN
wenzelm@69291: 
wenzelm@69291: 
wenzelm@69248: {- pretty printing -}
wenzelm@69248: 
wenzelm@69248: markupN, consistentN, unbreakableN, indentN :: String
wenzelm@69248: markupN = \<open>Markup.markupN\<close>;
wenzelm@69248: consistentN = \<open>Markup.consistentN\<close>;
wenzelm@69248: unbreakableN = \<open>Markup.unbreakableN\<close>;
wenzelm@69248: indentN = \<open>Markup.indentN\<close>;
wenzelm@69248: 
wenzelm@69248: widthN :: String
wenzelm@69248: widthN = \<open>Markup.widthN\<close>
wenzelm@69248: 
wenzelm@69248: blockN :: String
wenzelm@69248: blockN = \<open>Markup.blockN\<close>
wenzelm@69248: block :: Bool -> Int -> T
wenzelm@69248: block c i =
wenzelm@69248:   (blockN,
wenzelm@69248:     (if c then [(consistentN, Value.print_bool c)] else []) ++
wenzelm@69248:     (if i /= 0 then [(indentN, Value.print_int i)] else []))
wenzelm@69248: 
wenzelm@69248: breakN :: String
wenzelm@69248: breakN = \<open>Markup.breakN\<close>
wenzelm@69248: break :: Int -> Int -> T
wenzelm@69248: break w i =
wenzelm@69248:   (breakN,
wenzelm@69248:     (if w /= 0 then [(widthN, Value.print_int w)] else []) ++
wenzelm@69248:     (if i /= 0 then [(indentN, Value.print_int i)] else []))
wenzelm@69248: 
wenzelm@69248: fbreakN :: String; fbreak :: T
wenzelm@69248: (fbreakN, fbreak) = markup_elem \<open>Markup.fbreakN\<close>
wenzelm@69248: 
wenzelm@69248: itemN :: String; item :: T
wenzelm@69248: (itemN, item) = markup_elem \<open>Markup.itemN\<close>
wenzelm@69248: 
wenzelm@69248: 
wenzelm@69234: {- text properties -}
wenzelm@69234: 
wenzelm@69234: wordsN :: String; words :: T
wenzelm@69234: (wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: {- inner syntax -}
wenzelm@69234: 
wenzelm@69234: tfreeN :: String; tfree :: T
wenzelm@69234: (tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
wenzelm@69234: 
wenzelm@69234: tvarN :: String; tvar :: T
wenzelm@69234: (tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
wenzelm@69234: 
wenzelm@69234: freeN :: String; free :: T
wenzelm@69234: (freeN, free) = markup_elem \<open>Markup.freeN\<close>
wenzelm@69234: 
wenzelm@69234: skolemN :: String; skolem :: T
wenzelm@69234: (skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
wenzelm@69234: 
wenzelm@69234: boundN :: String; bound :: T
wenzelm@69234: (boundN, bound) = markup_elem \<open>Markup.boundN\<close>
wenzelm@69234: 
wenzelm@69234: varN :: String; var :: T
wenzelm@69234: (varN, var) = markup_elem \<open>Markup.varN\<close>
wenzelm@69234: 
wenzelm@69234: numeralN :: String; numeral :: T
wenzelm@69234: (numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
wenzelm@69234: 
wenzelm@69234: literalN :: String; literal :: T
wenzelm@69234: (literalN, literal) = markup_elem \<open>Markup.literalN\<close>
wenzelm@69234: 
wenzelm@69234: delimiterN :: String; delimiter :: T
wenzelm@69234: (delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
wenzelm@69234: 
wenzelm@69234: inner_stringN :: String; inner_string :: T
wenzelm@69234: (inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
wenzelm@69234: 
wenzelm@69234: inner_cartoucheN :: String; inner_cartouche :: T
wenzelm@69234: (inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: token_rangeN :: String; token_range :: T
wenzelm@69234: (token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: sortingN :: String; sorting :: T
wenzelm@69234: (sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
wenzelm@69234: 
wenzelm@69234: typingN :: String; typing :: T
wenzelm@69234: (typingN, typing) = markup_elem \<open>Markup.typingN\<close>
wenzelm@69234: 
wenzelm@69234: class_parameterN :: String; class_parameter :: T
wenzelm@69234: (class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: {- antiquotations -}
wenzelm@69234: 
wenzelm@69234: antiquotedN :: String; antiquoted :: T
wenzelm@69234: (antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
wenzelm@69234: 
wenzelm@69234: antiquoteN :: String; antiquote :: T
wenzelm@69234: (antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: {- text structure -}
wenzelm@69234: 
wenzelm@69234: paragraphN :: String; paragraph :: T
wenzelm@69234: (paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
wenzelm@69234: 
wenzelm@69234: text_foldN :: String; text_fold :: T
wenzelm@69234: (text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: {- outer syntax -}
wenzelm@69234: 
wenzelm@69234: keyword1N :: String; keyword1 :: T
wenzelm@69234: (keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
wenzelm@69234: 
wenzelm@69234: keyword2N :: String; keyword2 :: T
wenzelm@69234: (keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
wenzelm@69234: 
wenzelm@69234: keyword3N :: String; keyword3 :: T
wenzelm@69234: (keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
wenzelm@69234: 
wenzelm@69234: quasi_keywordN :: String; quasi_keyword :: T
wenzelm@69234: (quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
wenzelm@69234: 
wenzelm@69234: improperN :: String; improper :: T
wenzelm@69234: (improperN, improper) = markup_elem \<open>Markup.improperN\<close>
wenzelm@69234: 
wenzelm@69234: operatorN :: String; operator :: T
wenzelm@69234: (operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
wenzelm@69234: 
wenzelm@69234: stringN :: String; string :: T
wenzelm@69234: (stringN, string) = markup_elem \<open>Markup.stringN\<close>
wenzelm@69234: 
wenzelm@69234: alt_stringN :: String; alt_string :: T
wenzelm@69234: (alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
wenzelm@69234: 
wenzelm@69234: verbatimN :: String; verbatim :: T
wenzelm@69234: (verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
wenzelm@69234: 
wenzelm@69234: cartoucheN :: String; cartouche :: T
wenzelm@69234: (cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
wenzelm@69234: 
wenzelm@69234: commentN :: String; comment :: T
wenzelm@69234: (commentN, comment) = markup_elem \<open>Markup.commentN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69320: {- comments -}
wenzelm@69320: 
wenzelm@69320: comment1N :: String; comment1 :: T
wenzelm@69320: (comment1N, comment1) = markup_elem \<open>Markup.comment1N\<close>
wenzelm@69320: 
wenzelm@69320: comment2N :: String; comment2 :: T
wenzelm@69320: (comment2N, comment2) = markup_elem \<open>Markup.comment2N\<close>
wenzelm@69320: 
wenzelm@69320: comment3N :: String; comment3 :: T
wenzelm@69320: (comment3N, comment3) = markup_elem \<open>Markup.comment3N\<close>
wenzelm@69320: 
wenzelm@69320: 
wenzelm@69793: {- command status -}
wenzelm@69793: 
wenzelm@69793: acceptedN, forkedN, joinedN, runningN, finishedN, failedN, canceledN,
wenzelm@69793:   initializedN, finalizedN, consolidatedN :: String
wenzelm@69793: accepted, forked, joined, running, finished, failed, canceled,
wenzelm@69793:   initialized, finalized, consolidated :: T
wenzelm@69793: (acceptedN, accepted) = markup_elem \<open>Markup.acceptedN\<close>
wenzelm@69793: (forkedN, forked) = markup_elem \<open>Markup.forkedN\<close>
wenzelm@69793: (joinedN, joined) = markup_elem \<open>Markup.joinedN\<close>
wenzelm@69793: (runningN, running) = markup_elem \<open>Markup.runningN\<close>
wenzelm@69793: (finishedN, finished) = markup_elem \<open>Markup.finishedN\<close>
wenzelm@69793: (failedN, failed) = markup_elem \<open>Markup.failedN\<close>
wenzelm@69793: (canceledN, canceled) = markup_elem \<open>Markup.canceledN\<close>
wenzelm@69793: (initializedN, initialized) = markup_elem \<open>Markup.initializedN\<close>
wenzelm@69793: (finalizedN, finalized) = markup_elem \<open>Markup.finalizedN\<close>
wenzelm@69793: (consolidatedN, consolidated) = markup_elem \<open>Markup.consolidatedN\<close>
wenzelm@69793: 
wenzelm@69793: 
wenzelm@69234: {- messages -}
wenzelm@69234: 
wenzelm@69234: writelnN :: String; writeln :: T
wenzelm@69234: (writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
wenzelm@69234: 
wenzelm@69234: stateN :: String; state :: T
wenzelm@69234: (stateN, state) = markup_elem \<open>Markup.stateN\<close>
wenzelm@69234: 
wenzelm@69234: informationN :: String; information :: T
wenzelm@69234: (informationN, information) = markup_elem \<open>Markup.informationN\<close>
wenzelm@69234: 
wenzelm@69234: tracingN :: String; tracing :: T
wenzelm@69234: (tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
wenzelm@69234: 
wenzelm@69234: warningN :: String; warning :: T
wenzelm@69234: (warningN, warning) = markup_elem \<open>Markup.warningN\<close>
wenzelm@69234: 
wenzelm@69234: legacyN :: String; legacy :: T
wenzelm@69234: (legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
wenzelm@69234: 
wenzelm@69234: errorN :: String; error :: T
wenzelm@69234: (errorN, error) = markup_elem \<open>Markup.errorN\<close>
wenzelm@69234: 
wenzelm@69234: reportN :: String; report :: T
wenzelm@69234: (reportN, report) = markup_elem \<open>Markup.reportN\<close>
wenzelm@69234: 
wenzelm@69234: no_reportN :: String; no_report :: T
wenzelm@69234: (no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
wenzelm@69234: 
wenzelm@69234: intensifyN :: String; intensify :: T
wenzelm@69234: (intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
wenzelm@69234: 
wenzelm@69234: 
wenzelm@69234: {- output -}
wenzelm@69225: 
wenzelm@69225: type Output = (String, String)
wenzelm@69225: 
wenzelm@69225: no_output :: Output
wenzelm@69225: no_output = ("", "")
wenzelm@69222: \<close>
wenzelm@69222: 
wenzelm@69444: generate_file "Isabelle/Completion.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Completion.hs
wenzelm@69288:     Author:     Makarius
wenzelm@69288:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69288: 
wenzelm@69288: Completion of names.
wenzelm@69288: 
wenzelm@69288: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
wenzelm@69288: -}
wenzelm@69288: 
wenzelm@69289: module Isabelle.Completion (
wenzelm@69289:     Name, T, names, none, make, markup_element, markup_report, make_report
wenzelm@69289:   ) where
wenzelm@69288: 
wenzelm@69288: import qualified Data.List as List
wenzelm@69288: 
wenzelm@69288: import Isabelle.Library
wenzelm@69288: import qualified Isabelle.Properties as Properties
wenzelm@69288: import qualified Isabelle.Markup as Markup
wenzelm@69288: import qualified Isabelle.XML.Encode as Encode
wenzelm@69288: import qualified Isabelle.XML as XML
wenzelm@69288: import qualified Isabelle.YXML as YXML
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: type Name = (String, (String, String))  -- external name, kind, internal name
wenzelm@69288: data T = Completion Properties.T Int [Name]  -- position, total length, names
wenzelm@69288: 
wenzelm@69288: names :: Int -> Properties.T -> [Name] -> T
wenzelm@69288: names limit props names = Completion props (length names) (take limit names)
wenzelm@69288: 
wenzelm@69288: none :: T
wenzelm@69288: none = names 0 [] []
wenzelm@69288: 
wenzelm@69288: make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T
wenzelm@69288: make limit (name, props) make_names =
wenzelm@69288:   if name /= "" && name /= "_"
wenzelm@69288:   then names limit props (make_names $ List.isPrefixOf $ clean_name name)
wenzelm@69288:   else none
wenzelm@69288: 
wenzelm@69289: markup_element :: T -> (Markup.T, XML.Body)
wenzelm@69289: markup_element (Completion props total names) =
wenzelm@69289:   if not (null names) then
wenzelm@69289:     let
wenzelm@69289:       markup = Markup.properties props Markup.completion
wenzelm@69289:       body =
wenzelm@69289:         Encode.pair Encode.int
wenzelm@69289:           (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
wenzelm@69289:           (total, names)
wenzelm@69289:     in (markup, body)
wenzelm@69289:   else (Markup.empty, [])
wenzelm@69288: 
wenzelm@69289: markup_report :: [T] -> String
wenzelm@69289: markup_report [] = ""
wenzelm@69289: markup_report elems =
wenzelm@69290:   YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
wenzelm@69289: 
wenzelm@69289: make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
wenzelm@69289: make_report limit name_props make_names =
wenzelm@69289:   markup_report [make limit name_props make_names]
wenzelm@69288: \<close>
wenzelm@69288: 
wenzelm@69444: generate_file "Isabelle/File.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/File.hs
wenzelm@69278:     Author:     Makarius
wenzelm@69278:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69278: 
wenzelm@69280: File-system operations.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
wenzelm@69278: -}
wenzelm@69278: 
wenzelm@69278: module Isabelle.File (setup, read, write, append) where
wenzelm@69278: 
wenzelm@69278: import Prelude hiding (read)
wenzelm@69278: import System.IO (IO)
wenzelm@69278: import qualified System.IO as IO
wenzelm@69278: 
wenzelm@69278: setup :: IO.Handle -> IO ()
wenzelm@69278: setup h = do
wenzelm@69278:   IO.hSetEncoding h IO.utf8
wenzelm@69278:   IO.hSetNewlineMode h IO.noNewlineTranslation
wenzelm@69278: 
wenzelm@69278: read :: IO.FilePath -> IO String
wenzelm@69278: read path =
wenzelm@69278:   IO.withFile path IO.ReadMode (\h ->
wenzelm@69278:     do setup h; IO.hGetContents h >>= \s -> length s `seq` return s)
wenzelm@69278: 
wenzelm@69278: write :: IO.FilePath -> String -> IO ()
wenzelm@69278: write path s =
wenzelm@69278:   IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s)
wenzelm@69278: 
wenzelm@69278: append :: IO.FilePath -> String -> IO ()
wenzelm@69278: append path s =
wenzelm@69278:   IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
wenzelm@69278: \<close>
wenzelm@69278: 
wenzelm@69444: generate_file "Isabelle/XML.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/XML.hs
wenzelm@69225:     Author:     Makarius
wenzelm@69225:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225: 
wenzelm@69225: Untyped XML trees and representation of ML values.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
wenzelm@69225: -}
wenzelm@69225: 
wenzelm@69225: module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
wenzelm@69225: where
wenzelm@69225: 
wenzelm@69225: import qualified Data.List as List
wenzelm@69225: 
wenzelm@69225: import Isabelle.Library
wenzelm@69225: import qualified Isabelle.Properties as Properties
wenzelm@69225: import qualified Isabelle.Markup as Markup
wenzelm@69225: import qualified Isabelle.Buffer as Buffer
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69225: {- types -}
wenzelm@69225: 
wenzelm@69225: type Attributes = Properties.T
wenzelm@69225: type Body = [Tree]
wenzelm@69290: data Tree = Elem (Markup.T, Body) | Text String
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69225: {- wrapped elements -}
wenzelm@69225: 
wenzelm@69482: wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
wenzelm@69236: wrap_elem (((a, atts), body1), body2) =
wenzelm@69290:   Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)
wenzelm@69225: 
wenzelm@69482: unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
wenzelm@69236: unwrap_elem
wenzelm@69290:   (Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)) =
wenzelm@69236:   Just (((a, atts), body1), body2)
wenzelm@69225: unwrap_elem _ = Nothing
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69225: {- text content -}
wenzelm@69225: 
wenzelm@69482: add_content :: Tree -> Buffer.T -> Buffer.T
wenzelm@69225: add_content tree =
wenzelm@69225:   case unwrap_elem tree of
wenzelm@69225:     Just (_, ts) -> fold add_content ts
wenzelm@69225:     Nothing ->
wenzelm@69225:       case tree of
wenzelm@69290:         Elem (_, ts) -> fold add_content ts
wenzelm@69225:         Text s -> Buffer.add s
wenzelm@69225: 
wenzelm@69482: content_of :: Body -> String
wenzelm@69225: content_of body = Buffer.empty |> fold add_content body |> Buffer.content
wenzelm@69225: 
wenzelm@69225: 
wenzelm@69225: {- string representation -}
wenzelm@69225: 
wenzelm@69225: encode '<' = "&lt;"
wenzelm@69225: encode '>' = "&gt;"
wenzelm@69225: encode '&' = "&amp;"
wenzelm@69225: encode '\'' = "&apos;"
wenzelm@69225: encode '\"' = "&quot;"
wenzelm@69225: encode c = [c]
wenzelm@69225: 
wenzelm@69225: instance Show Tree where
wenzelm@69225:   show tree =
wenzelm@69225:     Buffer.empty |> show_tree tree |> Buffer.content
wenzelm@69225:     where
wenzelm@69290:       show_tree (Elem ((name, atts), [])) =
wenzelm@69225:         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
wenzelm@69290:       show_tree (Elem ((name, atts), ts)) =
wenzelm@69225:         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
wenzelm@69225:         fold show_tree ts #>
wenzelm@69225:         Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
wenzelm@69225:       show_tree (Text s) = Buffer.add (show_text s)
wenzelm@69225: 
wenzelm@69225:       show_elem name atts =
wenzelm@69225:         unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
wenzelm@69225: 
wenzelm@69225:       show_text = concatMap encode
wenzelm@69225: \<close>
wenzelm@69225: 
wenzelm@69444: generate_file "Isabelle/XML/Encode.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/XML/Encode.hs
wenzelm@69240:     Author:     Makarius
wenzelm@69240:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240: 
wenzelm@69240: XML as data representation language.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
wenzelm@69240: -}
wenzelm@69240: 
wenzelm@69240: module Isabelle.XML.Encode (
wenzelm@69240:   A, T, V,
wenzelm@69240: 
wenzelm@69240:   int_atom, bool_atom, unit_atom,
wenzelm@69240: 
wenzelm@69287:   tree, properties, string, int, bool, unit, pair, triple, list, variant
wenzelm@69240: )
wenzelm@69240: where
wenzelm@69240: 
wenzelm@69240: import Isabelle.Library
wenzelm@69240: import qualified Isabelle.Value as Value
wenzelm@69240: import qualified Isabelle.Properties as Properties
wenzelm@69240: import qualified Isabelle.XML as XML
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: type A a = a -> String
wenzelm@69240: type T a = a -> XML.Body
wenzelm@69240: type V a = a -> Maybe ([String], XML.Body)
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: -- atomic values
wenzelm@69240: 
wenzelm@69240: int_atom :: A Int
wenzelm@69240: int_atom = Value.print_int
wenzelm@69240: 
wenzelm@69240: bool_atom :: A Bool
wenzelm@69240: bool_atom False = "0"
wenzelm@69240: bool_atom True = "1"
wenzelm@69240: 
wenzelm@69240: unit_atom :: A ()
wenzelm@69240: unit_atom () = ""
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: -- structural nodes
wenzelm@69240: 
wenzelm@69290: node ts = XML.Elem ((":", []), ts)
wenzelm@69240: 
wenzelm@69240: vector = map_index (\(i, x) -> (int_atom i, x))
wenzelm@69240: 
wenzelm@69290: tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: -- representation of standard types
wenzelm@69240: 
wenzelm@69240: tree :: T XML.Tree
wenzelm@69240: tree t = [t]
wenzelm@69240: 
wenzelm@69240: properties :: T Properties.T
wenzelm@69290: properties props = [XML.Elem ((":", props), [])]
wenzelm@69240: 
wenzelm@69240: string :: T String
wenzelm@69240: string "" = []
wenzelm@69240: string s = [XML.Text s]
wenzelm@69240: 
wenzelm@69240: int :: T Int
wenzelm@69240: int = string . int_atom
wenzelm@69240: 
wenzelm@69240: bool :: T Bool
wenzelm@69240: bool = string . bool_atom
wenzelm@69240: 
wenzelm@69240: unit :: T ()
wenzelm@69240: unit = string . unit_atom
wenzelm@69240: 
wenzelm@69240: pair :: T a -> T b -> T (a, b)
wenzelm@69240: pair f g (x, y) = [node (f x), node (g y)]
wenzelm@69240: 
wenzelm@69240: triple :: T a -> T b -> T c -> T (a, b, c)
wenzelm@69240: triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
wenzelm@69240: 
wenzelm@69240: list :: T a -> T [a]
wenzelm@69240: list f xs = map (node . f) xs
wenzelm@69240: 
wenzelm@69240: variant :: [V a] -> T a
wenzelm@69240: variant fs x = [tagged (the (get_index (\f -> f x) fs))]
wenzelm@69240: \<close>
wenzelm@69240: 
wenzelm@69444: generate_file "Isabelle/XML/Decode.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/XML/Decode.hs
wenzelm@69240:     Author:     Makarius
wenzelm@69240:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240: 
wenzelm@69240: XML as data representation language.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>.
wenzelm@69240: -}
wenzelm@69240: 
wenzelm@69240: module Isabelle.XML.Decode (
wenzelm@69240:   A, T, V,
wenzelm@69240: 
wenzelm@69240:   int_atom, bool_atom, unit_atom,
wenzelm@69240: 
wenzelm@69240:   tree, properties, string, init, bool, unit, pair, triple, list, variant
wenzelm@69240: )
wenzelm@69240: where
wenzelm@69240: 
wenzelm@69240: import Data.List ((!!))
wenzelm@69240: 
wenzelm@69240: import Isabelle.Library
wenzelm@69240: import qualified Isabelle.Value as Value
wenzelm@69240: import qualified Isabelle.Properties as Properties
wenzelm@69240: import qualified Isabelle.XML as XML
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: type A a = String -> a
wenzelm@69240: type T a = XML.Body -> a
wenzelm@69240: type V a = ([String], XML.Body) -> a
wenzelm@69240: 
wenzelm@69240: err_atom = error "Malformed XML atom"
wenzelm@69240: err_body = error "Malformed XML body"
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: {- atomic values -}
wenzelm@69240: 
wenzelm@69240: int_atom :: A Int
wenzelm@69240: int_atom s =
wenzelm@69240:   case Value.parse_int s of
wenzelm@69240:     Just i -> i
wenzelm@69240:     Nothing -> err_atom
wenzelm@69240: 
wenzelm@69240: bool_atom :: A Bool
wenzelm@69240: bool_atom "0" = False
wenzelm@69240: bool_atom "1" = True
wenzelm@69240: bool_atom _ = err_atom
wenzelm@69240: 
wenzelm@69240: unit_atom :: A ()
wenzelm@69240: unit_atom "" = ()
wenzelm@69240: unit_atom _ = err_atom
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: {- structural nodes -}
wenzelm@69240: 
wenzelm@69290: node (XML.Elem ((":", []), ts)) = ts
wenzelm@69240: node _ = err_body
wenzelm@69240: 
wenzelm@69240: vector atts =
wenzelm@69240:   map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
wenzelm@69240: 
wenzelm@69290: tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
wenzelm@69240: tagged _ = err_body
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: {- representation of standard types -}
wenzelm@69240: 
wenzelm@69240: tree :: T XML.Tree
wenzelm@69240: tree [t] = t
wenzelm@69240: tree _ = err_body
wenzelm@69240: 
wenzelm@69240: properties :: T Properties.T
wenzelm@69290: properties [XML.Elem ((":", props), [])] = props
wenzelm@69240: properties _ = err_body
wenzelm@69240: 
wenzelm@69240: string :: T String
wenzelm@69240: string [] = ""
wenzelm@69240: string [XML.Text s] = s
wenzelm@69240: string _ = err_body
wenzelm@69240: 
wenzelm@69240: int :: T Int
wenzelm@69240: int = int_atom . string
wenzelm@69240: 
wenzelm@69240: bool :: T Bool
wenzelm@69240: bool = bool_atom . string
wenzelm@69240: 
wenzelm@69240: unit :: T ()
wenzelm@69240: unit = unit_atom . string
wenzelm@69240: 
wenzelm@69240: pair :: T a -> T b -> T (a, b)
wenzelm@69240: pair f g [t1, t2] = (f (node t1), g (node t2))
wenzelm@69240: pair _ _ _ = err_body
wenzelm@69240: 
wenzelm@69240: triple :: T a -> T b -> T c -> T (a, b, c)
wenzelm@69240: triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
wenzelm@69240: triple _ _ _ _ = err_body
wenzelm@69240: 
wenzelm@69240: list :: T a -> T [a]
wenzelm@69240: list f ts = map (f . node) ts
wenzelm@69240: 
wenzelm@69240: option :: T a -> T (Maybe a)
wenzelm@69240: option _ [] = Nothing
wenzelm@69240: option f [t] = Just (f (node t))
wenzelm@69240: option _ _ = err_body
wenzelm@69240: 
wenzelm@69240: variant :: [V a] -> T a
wenzelm@69240: variant fs [t] = (fs !! tag) (xs, ts)
wenzelm@69240:   where (tag, (xs, ts)) = tagged t
wenzelm@69240: variant _ _ = err_body
wenzelm@69240: \<close>
wenzelm@69240: 
wenzelm@69444: generate_file "Isabelle/YXML.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/YXML.hs
wenzelm@69288:     Author:     Makarius
wenzelm@69288:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69288: 
wenzelm@69288: Efficient text representation of XML trees.  Suitable for direct
wenzelm@69288: inlining into plain text.
wenzelm@69288: 
wenzelm@69288: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>.
wenzelm@69288: -}
wenzelm@69288: 
wenzelm@69288: module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
wenzelm@69288:   buffer_body, buffer, string_of_body, string_of, parse_body, parse)
wenzelm@69288: where
wenzelm@69288: 
wenzelm@69288: import qualified Data.Char as Char
wenzelm@69288: import qualified Data.List as List
wenzelm@69288: 
wenzelm@69288: import Isabelle.Library
wenzelm@69288: import qualified Isabelle.Markup as Markup
wenzelm@69288: import qualified Isabelle.XML as XML
wenzelm@69288: import qualified Isabelle.Buffer as Buffer
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: {- markers -}
wenzelm@69288: 
wenzelm@69288: charX, charY :: Char
wenzelm@69288: charX = Char.chr 5
wenzelm@69288: charY = Char.chr 6
wenzelm@69288: 
wenzelm@69288: strX, strY, strXY, strXYX :: String
wenzelm@69288: strX = [charX]
wenzelm@69288: strY = [charY]
wenzelm@69288: strXY = strX ++ strY
wenzelm@69288: strXYX = strXY ++ strX
wenzelm@69288: 
wenzelm@69288: detect :: String -> Bool
wenzelm@69288: detect = any (\c -> c == charX || c == charY)
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: {- output -}
wenzelm@69288: 
wenzelm@69288: output_markup :: Markup.T -> Markup.Output
wenzelm@69288: output_markup markup@(name, atts) =
wenzelm@69288:   if Markup.is_empty markup then Markup.no_output
wenzelm@69288:   else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX)
wenzelm@69288: 
wenzelm@69288: buffer_attrib (a, x) =
wenzelm@69288:   Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
wenzelm@69288: 
wenzelm@69288: buffer_body :: XML.Body -> Buffer.T -> Buffer.T
wenzelm@69288: buffer_body = fold buffer
wenzelm@69288: 
wenzelm@69288: buffer :: XML.Tree -> Buffer.T -> Buffer.T
wenzelm@69290: buffer (XML.Elem ((name, atts), ts)) =
wenzelm@69288:   Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
wenzelm@69288:   buffer_body ts #>
wenzelm@69288:   Buffer.add strXYX
wenzelm@69288: buffer (XML.Text s) = Buffer.add s
wenzelm@69288: 
wenzelm@69288: string_of_body :: XML.Body -> String
wenzelm@69288: string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
wenzelm@69288: 
wenzelm@69288: string_of :: XML.Tree -> String
wenzelm@69288: string_of = string_of_body . single
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: {- parse -}
wenzelm@69288: 
wenzelm@69288: -- split: fields or non-empty tokens
wenzelm@69288: 
wenzelm@69288: split :: Bool -> Char -> String -> [String]
wenzelm@69288: split _ _ [] = []
wenzelm@69288: split fields sep str = splitting str
wenzelm@69288:   where
wenzelm@69288:     splitting rest =
wenzelm@69288:       case span (/= sep) rest of
wenzelm@69288:         (_, []) -> cons rest []
wenzelm@69288:         (prfx, _ : rest') -> cons prfx (splitting rest')
wenzelm@69288:     cons item = if fields || not (null item) then (:) item else id
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: -- structural errors
wenzelm@69288: 
wenzelm@69288: err msg = error ("Malformed YXML: " ++ msg)
wenzelm@69288: err_attribute = err "bad attribute"
wenzelm@69288: err_element = err "bad element"
wenzelm@69288: err_unbalanced "" = err "unbalanced element"
wenzelm@69288: err_unbalanced name = err ("unbalanced element " ++ quote name)
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: -- stack operations
wenzelm@69288: 
wenzelm@69288: add x ((elem, body) : pending) = (elem, x : body) : pending
wenzelm@69288: 
wenzelm@69288: push "" _ _ = err_element
wenzelm@69288: push name atts pending = ((name, atts), []) : pending
wenzelm@69288: 
wenzelm@69288: pop ((("", _), _) : _) = err_unbalanced ""
wenzelm@69290: pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending
wenzelm@69288: 
wenzelm@69288: 
wenzelm@69288: -- parsing
wenzelm@69288: 
wenzelm@69288: parse_attrib s =
wenzelm@69288:   case List.elemIndex '=' s of
wenzelm@69288:     Just i | i > 0 -> (take i s, drop (i + 1) s)
wenzelm@69288:     _ -> err_attribute
wenzelm@69288: 
wenzelm@69288: parse_chunk ["", ""] = pop
wenzelm@69288: parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
wenzelm@69288: parse_chunk txts = fold (add . XML.Text) txts
wenzelm@69288: 
wenzelm@69288: parse_body :: String -> XML.Body
wenzelm@69288: parse_body source =
wenzelm@69288:   case fold parse_chunk chunks [(("", []), [])] of
wenzelm@69288:     [(("", _), result)] -> reverse result
wenzelm@69288:     ((name, _), _) : _ -> err_unbalanced name
wenzelm@69288:   where chunks = split False charX source |> map (split True charY)
wenzelm@69288: 
wenzelm@69288: parse :: String -> XML.Tree
wenzelm@69288: parse source =
wenzelm@69288:   case parse_body source of
wenzelm@69288:     [result] -> result
wenzelm@69288:     [] -> XML.Text ""
wenzelm@69288:     _ -> err "multiple results"
wenzelm@69288: \<close>
wenzelm@69288: 
wenzelm@69444: generate_file "Isabelle/Pretty.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Pretty.hs
wenzelm@69248:     Author:     Makarius
wenzelm@69248:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69248: 
wenzelm@69248: Generic pretty printing module.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
wenzelm@69248: -}
wenzelm@69248: 
wenzelm@69248: module Isabelle.Pretty (
wenzelm@69248:   T, symbolic, formatted, unformatted,
wenzelm@69248: 
wenzelm@69248:   str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str,
wenzelm@69248:   item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate,
wenzelm@69248:   commas, enclose, enum, list, str_list, big_list)
wenzelm@69248: where
wenzelm@69248: 
wenzelm@69453: import Isabelle.Library hiding (quote, commas)
wenzelm@69248: import qualified Data.List as List
wenzelm@69248: import qualified Isabelle.Buffer as Buffer
wenzelm@69248: import qualified Isabelle.Markup as Markup
wenzelm@69248: import qualified Isabelle.XML as XML
wenzelm@69248: import qualified Isabelle.YXML as YXML
wenzelm@69248: 
wenzelm@69248: 
wenzelm@69248: data T =
wenzelm@69248:     Block Markup.T Bool Int [T]
wenzelm@69248:   | Break Int Int
wenzelm@69248:   | Str String
wenzelm@69248: 
wenzelm@69248: 
wenzelm@69248: {- output -}
wenzelm@69248: 
wenzelm@69248: output_spaces n = replicate n ' '
wenzelm@69248: 
wenzelm@69248: symbolic_text "" = []
wenzelm@69248: symbolic_text s = [XML.Text s]
wenzelm@69248: 
wenzelm@69248: symbolic_markup markup body =
wenzelm@69248:   if Markup.is_empty markup then body
wenzelm@69290:   else [XML.Elem (markup, body)]
wenzelm@69248: 
wenzelm@69248: symbolic :: T -> XML.Body
wenzelm@69248: symbolic (Block markup consistent indent prts) =
wenzelm@69248:   concatMap symbolic prts
wenzelm@69248:   |> symbolic_markup block_markup
wenzelm@69248:   |> symbolic_markup markup
wenzelm@69248:   where block_markup = if null prts then Markup.empty else Markup.block consistent indent
wenzelm@69290: symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))]
wenzelm@69248: symbolic (Str s) = symbolic_text s
wenzelm@69248: 
wenzelm@69248: formatted :: T -> String
wenzelm@69248: formatted = YXML.string_of_body . symbolic
wenzelm@69248: 
wenzelm@69248: unformatted :: T -> String
wenzelm@69248: unformatted prt = Buffer.empty |> out prt |> Buffer.content
wenzelm@69248:   where
wenzelm@69248:     out (Block markup _ _ prts) =
wenzelm@69248:       let (bg, en) = YXML.output_markup markup
wenzelm@69248:       in Buffer.add bg #> fold out prts #> Buffer.add en
wenzelm@69248:     out (Break _ wd) = Buffer.add (output_spaces wd)
wenzelm@69248:     out (Str s) = Buffer.add s
wenzelm@69248: 
wenzelm@69248: 
wenzelm@69248: {- derived operations to create formatting expressions -}
wenzelm@69248: 
wenzelm@69248: force_nat n | n < 0 = 0
wenzelm@69248: force_nat n = n
wenzelm@69248: 
wenzelm@69248: str :: String -> T
wenzelm@69248: str = Str
wenzelm@69248: 
wenzelm@69248: brk_indent :: Int -> Int -> T
wenzelm@69248: brk_indent wd ind = Break (force_nat wd) ind
wenzelm@69248: 
wenzelm@69248: brk :: Int -> T
wenzelm@69248: brk wd = brk_indent wd 0
wenzelm@69248: 
wenzelm@69248: fbrk :: T
wenzelm@69248: fbrk = str "\n"
wenzelm@69248: 
wenzelm@69248: breaks, fbreaks :: [T] -> [T]
wenzelm@69248: breaks = List.intersperse (brk 1)
wenzelm@69248: fbreaks = List.intersperse fbrk
wenzelm@69248: 
wenzelm@69248: blk :: (Int, [T]) -> T
wenzelm@69248: blk (indent, es) = Block Markup.empty False (force_nat indent) es
wenzelm@69248: 
wenzelm@69248: block :: [T] -> T
wenzelm@69248: block prts = blk (2, prts)
wenzelm@69248: 
wenzelm@69248: strs :: [String] -> T
wenzelm@69248: strs = block . breaks . map str
wenzelm@69248: 
wenzelm@69248: markup :: Markup.T -> [T] -> T
wenzelm@69248: markup m = Block m False 0
wenzelm@69248: 
wenzelm@69248: mark :: Markup.T -> T -> T
wenzelm@69248: mark m prt = if m == Markup.empty then prt else markup m [prt]
wenzelm@69248: 
wenzelm@69248: mark_str :: (Markup.T, String) -> T
wenzelm@69248: mark_str (m, s) = mark m (str s)
wenzelm@69248: 
wenzelm@69248: marks_str :: ([Markup.T], String) -> T
wenzelm@69248: marks_str (ms, s) = fold_rev mark ms (str s)
wenzelm@69248: 
wenzelm@69248: item :: [T] -> T
wenzelm@69248: item = markup Markup.item
wenzelm@69248: 
wenzelm@69248: text_fold :: [T] -> T
wenzelm@69248: text_fold = markup Markup.text_fold
wenzelm@69248: 
wenzelm@69248: keyword1, keyword2 :: String -> T
wenzelm@69248: keyword1 name = mark_str (Markup.keyword1, name)
wenzelm@69248: keyword2 name = mark_str (Markup.keyword2, name)
wenzelm@69248: 
wenzelm@69248: text :: String -> [T]
wenzelm@69248: text = breaks . map str . words
wenzelm@69248: 
wenzelm@69248: paragraph :: [T] -> T
wenzelm@69248: paragraph = markup Markup.paragraph
wenzelm@69248: 
wenzelm@69248: para :: String -> T
wenzelm@69248: para = paragraph . text
wenzelm@69248: 
wenzelm@69248: quote :: T -> T
wenzelm@69248: quote prt = blk (1, [str "\"", prt, str "\""])
wenzelm@69248: 
wenzelm@69248: cartouche :: T -> T
wenzelm@69248: cartouche prt = blk (1, [str "\92<open>", prt, str "\92<close>"])
wenzelm@69248: 
wenzelm@69248: separate :: String -> [T] -> [T]
wenzelm@69248: separate sep = List.intercalate [str sep, brk 1] . map single
wenzelm@69248: 
wenzelm@69248: commas :: [T] -> [T]
wenzelm@69248: commas = separate ","
wenzelm@69248: 
wenzelm@69248: enclose :: String -> String -> [T] -> T
wenzelm@69248: enclose lpar rpar prts = block (str lpar : prts ++ [str rpar])
wenzelm@69248: 
wenzelm@69248: enum :: String -> String -> String -> [T] -> T
wenzelm@69248: enum sep lpar rpar = enclose lpar rpar . separate sep
wenzelm@69248: 
wenzelm@69248: list :: String -> String -> [T] -> T
wenzelm@69248: list = enum ","
wenzelm@69248: 
wenzelm@69248: str_list :: String -> String -> [String] -> T
wenzelm@69248: str_list lpar rpar = list lpar rpar . map str
wenzelm@69248: 
wenzelm@69248: big_list :: String -> [T] -> T
wenzelm@69248: big_list name prts = block (fbreaks (str name : prts))
wenzelm@69248: \<close>
wenzelm@69248: 
wenzelm@69444: generate_file "Isabelle/Term.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Term.hs
wenzelm@69240:     Author:     Makarius
wenzelm@69240:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240: 
wenzelm@69240: Lambda terms, types, sorts.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
wenzelm@69240: -}
wenzelm@69240: 
wenzelm@69240: module Isabelle.Term (
wenzelm@69240:   Indexname,
wenzelm@69240: 
wenzelm@69240:   Sort, dummyS,
wenzelm@69240: 
wenzelm@69240:   Typ(..), dummyT, Term(..))
wenzelm@69240: where
wenzelm@69240: 
wenzelm@69240: type Indexname = (String, Int)
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: type Sort = [String]
wenzelm@69240: 
wenzelm@69240: dummyS :: Sort
wenzelm@69240: dummyS = [""]
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: data Typ =
wenzelm@69240:     Type (String, [Typ])
wenzelm@69240:   | TFree (String, Sort)
wenzelm@69240:   | TVar (Indexname, Sort)
wenzelm@69240:   deriving Show
wenzelm@69240: 
wenzelm@69240: dummyT :: Typ
wenzelm@69240: dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: data Term =
wenzelm@69240:     Const (String, Typ)
wenzelm@69240:   | Free (String, Typ)
wenzelm@69240:   | Var (Indexname, Typ)
wenzelm@69240:   | Bound Int
wenzelm@69240:   | Abs (String, Typ, Term)
wenzelm@69240:   | App (Term, Term)
wenzelm@69240:   deriving Show
wenzelm@69240: \<close>
wenzelm@69240: 
wenzelm@69444: generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Term_XML/Encode.hs
wenzelm@69240:     Author:     Makarius
wenzelm@69240:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240: 
wenzelm@69240: XML data representation of lambda terms.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
wenzelm@69240: -}
wenzelm@69240: 
wenzelm@69240: {-# LANGUAGE LambdaCase #-}
wenzelm@69240: 
wenzelm@69240: module Isabelle.Term_XML.Encode (sort, typ, term)
wenzelm@69240: where
wenzelm@69240: 
wenzelm@69240: import Isabelle.Library
wenzelm@69240: import qualified Isabelle.XML as XML
wenzelm@69240: import Isabelle.XML.Encode
wenzelm@69240: import Isabelle.Term
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: sort :: T Sort
wenzelm@69240: sort = list string
wenzelm@69240: 
wenzelm@69240: typ :: T Typ
wenzelm@69240: typ ty =
wenzelm@69240:   ty |> variant
wenzelm@69240:    [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
wenzelm@69240:     \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
wenzelm@69240:     \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
wenzelm@69240: 
wenzelm@69240: term :: T Term
wenzelm@69240: term t =
wenzelm@69240:   t |> variant
wenzelm@69240:    [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
wenzelm@69240:     \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
wenzelm@69240:     \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
wenzelm@69240:     \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
wenzelm@69240:     \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
wenzelm@69240:     \case { App a -> Just ([], pair term term a); _ -> Nothing }]
wenzelm@69240: \<close>
wenzelm@69240: 
wenzelm@69444: generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
wenzelm@69445: {-  Title:      Isabelle/Term_XML/Decode.hs
wenzelm@69240:     Author:     Makarius
wenzelm@69240:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69240: 
wenzelm@69240: XML data representation of lambda terms.
wenzelm@69280: 
wenzelm@69280: See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
wenzelm@69240: -}
wenzelm@69240: 
wenzelm@69240: module Isabelle.Term_XML.Decode (sort, typ, term)
wenzelm@69240: where
wenzelm@69240: 
wenzelm@69240: import Isabelle.Library
wenzelm@69240: import qualified Isabelle.XML as XML
wenzelm@69240: import Isabelle.XML.Decode
wenzelm@69240: import Isabelle.Term
wenzelm@69240: 
wenzelm@69240: 
wenzelm@69240: sort :: T Sort
wenzelm@69240: sort = list string
wenzelm@69240: 
wenzelm@69240: typ :: T Typ
wenzelm@69240: typ ty =
wenzelm@69240:   ty |> variant
wenzelm@69240:   [\([a], b) -> Type (a, list typ b),
wenzelm@69240:    \([a], b) -> TFree (a, sort b),
wenzelm@69240:    \([a, b], c) -> TVar ((a, int_atom b), sort c)]
wenzelm@69240: 
wenzelm@69240: term :: T Term
wenzelm@69240: term t =
wenzelm@69240:   t |> variant
wenzelm@69240:    [\([a], b) -> Const (a, typ b),
wenzelm@69240:     \([a], b) -> Free (a, typ b),
wenzelm@69240:     \([a, b], c) -> Var ((a, int_atom b), typ c),
wenzelm@69240:     \([a], []) -> Bound (int_atom a),
wenzelm@69240:     \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
wenzelm@69240:     \([], a) -> App (pair term term a)]
wenzelm@69240: \<close>
wenzelm@69240: 
wenzelm@69459: generate_file "Isabelle/UUID.hs" = \<open>
wenzelm@69459: {-  Title:      Isabelle/UUID.hs
wenzelm@69459:     Author:     Makarius
wenzelm@69459:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69459: 
wenzelm@69459: Universally unique identifiers.
wenzelm@69459: 
wenzelm@69459: See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
wenzelm@69459: -}
wenzelm@69459: 
wenzelm@69465: module Isabelle.UUID (
wenzelm@69465:     T,
wenzelm@69465:     parse_string, parse_bytes,
wenzelm@69465:     string, bytes,
wenzelm@69465:     random, random_string, random_bytes
wenzelm@69465:   )
wenzelm@69459: where
wenzelm@69459: 
wenzelm@69465: import Data.ByteString (ByteString)
wenzelm@69465: import qualified Data.ByteString
wenzelm@69459: import Data.UUID (UUID)
wenzelm@69459: import qualified Data.UUID as UUID
wenzelm@69459: import Data.UUID.V4 (nextRandom)
wenzelm@69459: 
wenzelm@69459: 
wenzelm@69462: type T = UUID
wenzelm@69462: 
wenzelm@69465: 
wenzelm@69465: {- parse -}
wenzelm@69465: 
wenzelm@69465: parse_string :: String -> Maybe T
wenzelm@69465: parse_string = UUID.fromString
wenzelm@69465: 
wenzelm@69465: parse_bytes :: ByteString -> Maybe T
wenzelm@69465: parse_bytes = UUID.fromASCIIBytes
wenzelm@69465: 
wenzelm@69465: 
wenzelm@69465: {- print -}
wenzelm@69465: 
wenzelm@69465: string :: T -> String
wenzelm@69465: string = UUID.toString
wenzelm@69465: 
wenzelm@69465: bytes :: T -> ByteString
wenzelm@69465: bytes = UUID.toASCIIBytes
wenzelm@69465: 
wenzelm@69465: 
wenzelm@69465: {- random id -}
wenzelm@69465: 
wenzelm@69462: random :: IO T
wenzelm@69459: random = nextRandom
wenzelm@69459: 
wenzelm@69459: random_string :: IO String
wenzelm@69465: random_string = string <$> random
wenzelm@69459: 
wenzelm@69465: random_bytes :: IO ByteString
wenzelm@69465: random_bytes = bytes <$> random
wenzelm@69459: \<close>
wenzelm@69459: 
wenzelm@69448: generate_file "Isabelle/Byte_Message.hs" = \<open>
wenzelm@69448: {-  Title:      Isabelle/Byte_Message.hs
wenzelm@69446:     Author:     Makarius
wenzelm@69446:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69446: 
wenzelm@69448: Byte-oriented messages.
wenzelm@69448: 
wenzelm@69448: See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
wenzelm@69448: and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
wenzelm@69446: -}
wenzelm@69446: 
wenzelm@69452: module Isabelle.Byte_Message (
wenzelm@69467:     write, write_line,
wenzelm@69467:     read, read_block, trim_line, read_line,
wenzelm@69476:     make_message, write_message, read_message,
wenzelm@69476:     make_line_message, write_line_message, read_line_message
wenzelm@69452:   )
wenzelm@69446: where
wenzelm@69446: 
wenzelm@69449: import Prelude hiding (read)
wenzelm@69454: import Data.Maybe
wenzelm@69446: import Data.ByteString (ByteString)
wenzelm@69446: import qualified Data.ByteString as ByteString
wenzelm@69446: import qualified Data.ByteString.UTF8 as UTF8
wenzelm@69446: import Data.Word (Word8)
wenzelm@69446: 
wenzelm@69448: import Control.Monad (when)
wenzelm@69446: import Network.Socket (Socket)
wenzelm@69446: import qualified Network.Socket as Socket
wenzelm@69446: import qualified Network.Socket.ByteString as ByteString
wenzelm@69446: 
wenzelm@69454: import Isabelle.Library hiding (trim_line)
wenzelm@69446: import qualified Isabelle.Value as Value
wenzelm@69446: 
wenzelm@69446: 
wenzelm@69452: {- output operations -}
wenzelm@69452: 
wenzelm@69452: write :: Socket -> [ByteString] -> IO ()
wenzelm@69452: write = ByteString.sendMany
wenzelm@69452: 
wenzelm@69452: newline :: ByteString
wenzelm@69452: newline = ByteString.singleton 10
wenzelm@69452: 
wenzelm@69467: write_line :: Socket -> ByteString -> IO ()
wenzelm@69467: write_line socket s = write socket [s, newline]
wenzelm@69467: 
wenzelm@69452: 
wenzelm@69452: {- input operations -}
wenzelm@69452: 
wenzelm@69449: read :: Socket -> Int -> IO ByteString
wenzelm@69452: read socket n = read_body 0 []
wenzelm@69449:   where
wenzelm@69449:     result = ByteString.concat . reverse
wenzelm@69452:     read_body len ss =
wenzelm@69449:       if len >= n then return (result ss)
wenzelm@69449:       else
wenzelm@69449:         (do
wenzelm@69449:           s <- ByteString.recv socket (min (n - len) 8192)
wenzelm@69449:           case ByteString.length s of
wenzelm@69449:             0 -> return (result ss)
wenzelm@69452:             m -> read_body (len + m) (s : ss))
wenzelm@69452: 
wenzelm@69452: read_block :: Socket -> Int -> IO (Maybe ByteString, Int)
wenzelm@69452: read_block socket n = do
wenzelm@69452:   msg <- read socket n
wenzelm@69452:   let len = ByteString.length msg
wenzelm@69452:   return (if len == n then Just msg else Nothing, len)
wenzelm@69449: 
wenzelm@69452: trim_line :: ByteString -> ByteString
wenzelm@69452: trim_line s =
wenzelm@69452:   if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s
wenzelm@69452:   else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s
wenzelm@69452:   else s
wenzelm@69452:   where
wenzelm@69452:     n = ByteString.length s
wenzelm@69452:     at = ByteString.index s
wenzelm@69449: 
wenzelm@69446: read_line :: Socket -> IO (Maybe ByteString)
wenzelm@69452: read_line socket = read_body []
wenzelm@69446:   where
wenzelm@69452:     result = trim_line . ByteString.pack . reverse
wenzelm@69452:     read_body bs = do
wenzelm@69446:       s <- ByteString.recv socket 1
wenzelm@69446:       case ByteString.length s of
wenzelm@69446:         0 -> return (if null bs then Nothing else Just (result bs))
wenzelm@69446:         1 ->
wenzelm@69446:           case ByteString.head s of
wenzelm@69446:             10 -> return (Just (result bs))
wenzelm@69452:             b -> read_body (b : bs)
wenzelm@69446: 
wenzelm@69448: 
wenzelm@69454: {- messages with multiple chunks (arbitrary content) -}
wenzelm@69454: 
wenzelm@69454: make_header :: [Int] -> [ByteString]
wenzelm@69454: make_header ns =
wenzelm@69454:   [UTF8.fromString (space_implode "," (map Value.print_int ns)), newline]
wenzelm@69454: 
wenzelm@69476: make_message :: [ByteString] -> [ByteString]
wenzelm@69476: make_message chunks = make_header (map ByteString.length chunks) ++ chunks
wenzelm@69476: 
wenzelm@69454: write_message :: Socket -> [ByteString] -> IO ()
wenzelm@69476: write_message socket = write socket . make_message
wenzelm@69454: 
wenzelm@69454: parse_header :: ByteString -> [Int]
wenzelm@69454: parse_header line =
wenzelm@69454:   let
wenzelm@69454:     res = map Value.parse_nat (space_explode ',' (UTF8.toString line))
wenzelm@69454:   in
wenzelm@69454:     if all isJust res then map fromJust res
wenzelm@69454:     else error ("Malformed message header: " ++ quote (UTF8.toString line))
wenzelm@69454: 
wenzelm@69454: read_chunk :: Socket -> Int -> IO ByteString
wenzelm@69454: read_chunk socket n = do
wenzelm@69454:   res <- read_block socket n
wenzelm@69454:   return $
wenzelm@69454:     case res of
wenzelm@69454:       (Just chunk, _) -> chunk
wenzelm@69454:       (Nothing, len) ->
wenzelm@69454:         error ("Malformed message chunk: unexpected EOF after " ++
wenzelm@69454:           show len ++ " of " ++ show n ++ " bytes")
wenzelm@69454: 
wenzelm@69454: read_message :: Socket -> IO (Maybe [ByteString])
wenzelm@69454: read_message socket = do
wenzelm@69454:   res <- read_line socket
wenzelm@69454:   case res of
wenzelm@69454:     Just line -> Just <$> mapM (read_chunk socket) (parse_header line)
wenzelm@69454:     Nothing -> return Nothing
wenzelm@69454: 
wenzelm@69454: 
wenzelm@69448: -- hybrid messages: line or length+block (with content restriction)
wenzelm@69448: 
wenzelm@69448: is_length :: ByteString -> Bool
wenzelm@69452: is_length msg =
wenzelm@69452:   not (ByteString.null msg) && ByteString.all (\b -> 48 <= b && b <= 57) msg
wenzelm@69446: 
wenzelm@69452: is_terminated :: ByteString -> Bool
wenzelm@69452: is_terminated msg =
wenzelm@69452:   not (ByteString.null msg) && (ByteString.last msg == 13 || ByteString.last msg == 10)
wenzelm@69448: 
wenzelm@69476: make_line_message :: ByteString -> [ByteString]
wenzelm@69476: make_line_message msg =
wenzelm@69476:   let n = ByteString.length msg in
wenzelm@69476:     if is_length msg || is_terminated msg then
wenzelm@69476:       error ("Bad content for line message:\n" ++ take 100 (UTF8.toString msg))
wenzelm@69476:     else
wenzelm@69476:       (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) ++
wenzelm@69476:       [msg, newline]
wenzelm@69448: 
wenzelm@69476: write_line_message :: Socket -> ByteString -> IO ()
wenzelm@69476: write_line_message socket = write socket . make_line_message
wenzelm@69448: 
wenzelm@69448: read_line_message :: Socket -> IO (Maybe ByteString)
wenzelm@69448: read_line_message socket = do
wenzelm@69446:   opt_line <- read_line socket
wenzelm@69446:   case opt_line of
wenzelm@69446:     Nothing -> return Nothing
wenzelm@69446:     Just line ->
wenzelm@69452:       case Value.parse_nat (UTF8.toString line) of
wenzelm@69446:         Nothing -> return $ Just line
wenzelm@69452:         Just n -> fmap trim_line . fst <$> read_block socket n
wenzelm@69446: \<close>
wenzelm@69446: 
wenzelm@69473: generate_file "Isabelle/Standard_Thread.hs" = \<open>
wenzelm@69473: {-  Title:      Isabelle/Standard_Thread.hs
wenzelm@69473:     Author:     Makarius
wenzelm@69473:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69473: 
wenzelm@69473: Standard thread operations.
wenzelm@69473: 
wenzelm@69473: See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.ML\<close>
wenzelm@69473: and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.scala\<close>.
wenzelm@69473: -}
wenzelm@69473: 
wenzelm@69473: {-# LANGUAGE NamedFieldPuns #-}
wenzelm@69473: 
wenzelm@69473: module Isabelle.Standard_Thread (
wenzelm@69473:   ThreadId, Result,
wenzelm@69494:   find_id,
wenzelm@69473:   properties, change_properties,
wenzelm@69499:   add_resource, del_resource, bracket_resource,
wenzelm@69497:   is_stopped, expose_stopped, stop,
wenzelm@69496:   my_uuid, stop_uuid,
wenzelm@69494:   Fork, fork_finally, fork)
wenzelm@69473: where
wenzelm@69473: 
wenzelm@69499: import Data.Unique
wenzelm@69473: import Data.Maybe
wenzelm@69473: import Data.IORef
wenzelm@69473: import System.IO.Unsafe
wenzelm@69473: 
wenzelm@69494: import qualified Data.List as List
wenzelm@69497: import Control.Monad (when, forM_)
wenzelm@69473: import Data.Map.Strict (Map)
wenzelm@69473: import qualified Data.Map.Strict as Map
wenzelm@69473: import Control.Exception.Base (SomeException)
wenzelm@69473: import Control.Exception as Exception
wenzelm@69473: import Control.Concurrent (ThreadId)
wenzelm@69473: import qualified Control.Concurrent as Concurrent
wenzelm@69473: import Control.Concurrent.Thread (Result)
wenzelm@69473: import qualified Control.Concurrent.Thread as Thread
wenzelm@69494: import qualified Isabelle.UUID as UUID
wenzelm@69473: import qualified Isabelle.Properties as Properties
wenzelm@69473: 
wenzelm@69473: 
wenzelm@69473: {- thread info -}
wenzelm@69473: 
wenzelm@69499: type Resources = Map Unique (IO ())
wenzelm@69499: data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool, resources :: Resources}
wenzelm@69473: type Infos = Map ThreadId Info
wenzelm@69473: 
wenzelm@69473: lookup_info :: Infos -> ThreadId -> Maybe Info
wenzelm@69494: lookup_info infos id = Map.lookup id infos
wenzelm@69494: 
wenzelm@69494: init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ())
wenzelm@69499: init_info id uuid infos = (Map.insert id (Info uuid [] False Map.empty) infos, ())
wenzelm@69473: 
wenzelm@69473: 
wenzelm@69473: {- global state -}
wenzelm@69473: 
wenzelm@69473: {-# NOINLINE global_state #-}
wenzelm@69473: global_state :: IORef Infos
wenzelm@69473: global_state = unsafePerformIO (newIORef Map.empty)
wenzelm@69473: 
wenzelm@69494: find_id :: UUID.T -> IO (Maybe ThreadId)
wenzelm@69494: find_id uuid = do
wenzelm@69494:   state <- readIORef global_state
wenzelm@69494:   return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state)
wenzelm@69494: 
wenzelm@69473: get_info :: ThreadId -> IO (Maybe Info)
wenzelm@69473: get_info id = do
wenzelm@69473:   state <- readIORef global_state
wenzelm@69473:   return $ lookup_info state id
wenzelm@69473: 
wenzelm@69499: map_info :: ThreadId -> (Info -> Info) -> IO (Maybe Info)
wenzelm@69473: map_info id f =
wenzelm@69473:   atomicModifyIORef' global_state
wenzelm@69473:     (\infos ->
wenzelm@69473:       case lookup_info infos id of
wenzelm@69499:         Nothing -> (infos, Nothing)
wenzelm@69499:         Just info ->
wenzelm@69499:           let info' = f info
wenzelm@69499:           in (Map.insert id info' infos, Just info'))
wenzelm@69473: 
wenzelm@69495: delete_info :: ThreadId -> IO ()
wenzelm@69495: delete_info id =
wenzelm@69495:   atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ()))
wenzelm@69495: 
wenzelm@69473: 
wenzelm@69473: {- thread properties -}
wenzelm@69473: 
wenzelm@69498: my_info :: IO (Maybe Info)
wenzelm@69473: my_info = do
wenzelm@69473:   id <- Concurrent.myThreadId
wenzelm@69498:   get_info id
wenzelm@69473: 
wenzelm@69473: properties :: IO Properties.T
wenzelm@69498: properties = maybe [] props <$> my_info
wenzelm@69473: 
wenzelm@69473: change_properties :: (Properties.T -> Properties.T) -> IO ()
wenzelm@69473: change_properties f = do
wenzelm@69473:   id <- Concurrent.myThreadId
wenzelm@69473:   map_info id (\info -> info {props = f (props info)})
wenzelm@69499:   return ()
wenzelm@69499: 
wenzelm@69499: 
wenzelm@69499: {- managed resources -}
wenzelm@69499: 
wenzelm@69499: add_resource :: IO () -> IO Unique
wenzelm@69499: add_resource resource = do
wenzelm@69499:   id <- Concurrent.myThreadId
wenzelm@69499:   u <- newUnique
wenzelm@69499:   map_info id (\info -> info {resources = Map.insert u resource (resources info)})
wenzelm@69499:   return u
wenzelm@69499: 
wenzelm@69499: del_resource :: Unique -> IO ()
wenzelm@69499: del_resource u = do
wenzelm@69499:   id <- Concurrent.myThreadId
wenzelm@69499:   map_info id (\info -> info {resources = Map.delete u (resources info)})
wenzelm@69499:   return ()
wenzelm@69499: 
wenzelm@69499: bracket_resource :: IO () -> IO a -> IO a
wenzelm@69499: bracket_resource resource body =
wenzelm@69499:   Exception.bracket (add_resource resource) del_resource (const body)
wenzelm@69473: 
wenzelm@69473: 
wenzelm@69473: {- stop -}
wenzelm@69473: 
wenzelm@69473: is_stopped :: IO Bool
wenzelm@69498: is_stopped = maybe False stopped <$> my_info
wenzelm@69473: 
wenzelm@69497: expose_stopped :: IO ()
wenzelm@69497: expose_stopped = do
wenzelm@69497:   stopped <- is_stopped
wenzelm@69497:   when stopped $ throw ThreadKilled
wenzelm@69497: 
wenzelm@69473: stop :: ThreadId -> IO ()
wenzelm@69499: stop id = do
wenzelm@69499:   info <- map_info id (\info -> info {stopped = True})
wenzelm@69499:   let ops = case info of Nothing -> []; Just Info{resources} -> map snd (Map.toDescList resources)
wenzelm@69499:   sequence_ ops
wenzelm@69473: 
wenzelm@69473: 
wenzelm@69496: {- UUID -}
wenzelm@69496: 
wenzelm@69498: my_uuid :: IO (Maybe UUID.T)
wenzelm@69498: my_uuid = fmap uuid <$> my_info
wenzelm@69496: 
wenzelm@69496: stop_uuid :: UUID.T -> IO ()
wenzelm@69496: stop_uuid uuid = do
wenzelm@69496:   id <- find_id uuid
wenzelm@69496:   forM_ id stop
wenzelm@69496: 
wenzelm@69496: 
wenzelm@69473: {- fork -}
wenzelm@69473: 
wenzelm@69494: type Fork a = (ThreadId, UUID.T, IO (Result a))
wenzelm@69494: 
wenzelm@69494: fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b)
wenzelm@69473: fork_finally body finally = do
wenzelm@69494:   uuid <- UUID.random
wenzelm@69473:   (id, result) <-
wenzelm@69473:     Exception.mask (\restore ->
wenzelm@69473:       Thread.forkIO
wenzelm@69473:         (Exception.try
wenzelm@69473:           (do
wenzelm@69473:             id <- Concurrent.myThreadId
wenzelm@69494:             atomicModifyIORef' global_state (init_info id uuid)
wenzelm@69495:             restore body)
wenzelm@69495:          >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res)))
wenzelm@69494:   return (id, uuid, result)
wenzelm@69494: 
wenzelm@69494: fork :: IO a -> IO (Fork a)
wenzelm@69473: fork body = fork_finally body Thread.result
wenzelm@69473: \<close>
wenzelm@69473: 
wenzelm@69455: generate_file "Isabelle/Server.hs" = \<open>
wenzelm@69455: {-  Title:      Isabelle/Server.hs
wenzelm@69455:     Author:     Makarius
wenzelm@69455:     LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69455: 
wenzelm@69455: TCP server on localhost.
wenzelm@69455: -}
wenzelm@69455: 
wenzelm@69465: module Isabelle.Server (
wenzelm@69465:   localhost_name, localhost, publish_text, publish_stdout,
wenzelm@69465:   server
wenzelm@69465: )
wenzelm@69465: where
wenzelm@69455: 
wenzelm@69465: import Data.ByteString (ByteString)
wenzelm@69465: import Control.Monad (forever, when)
wenzelm@69455: import qualified Control.Exception as Exception
wenzelm@69455: import Network.Socket (Socket)
wenzelm@69455: import qualified Network.Socket as Socket
wenzelm@69472: import qualified System.IO as IO
wenzelm@69455: 
wenzelm@69462: import Isabelle.Library
wenzelm@69462: import qualified Isabelle.UUID as UUID
wenzelm@69465: import qualified Isabelle.Byte_Message as Byte_Message
wenzelm@69473: import qualified Isabelle.Standard_Thread as Standard_Thread
wenzelm@69462: 
wenzelm@69462: 
wenzelm@69462: {- server address -}
wenzelm@69455: 
wenzelm@69463: localhost_name :: String
wenzelm@69463: localhost_name = "127.0.0.1"
wenzelm@69463: 
wenzelm@69455: localhost :: Socket.HostAddress
wenzelm@69455: localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
wenzelm@69455: 
wenzelm@69462: publish_text :: String -> String -> UUID.T -> String
wenzelm@69462: publish_text name address password =
wenzelm@69462:   "server " ++ quote name ++ " = " ++ address ++ " (password " ++ quote (show password) ++ ")"
wenzelm@69462: 
wenzelm@69462: publish_stdout :: String -> String -> UUID.T -> IO ()
wenzelm@69462: publish_stdout name address password = putStrLn (publish_text name address password)
wenzelm@69462: 
wenzelm@69462: 
wenzelm@69462: {- server -}
wenzelm@69462: 
wenzelm@69462: server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
wenzelm@69455: server publish handle =
wenzelm@69462:   Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
wenzelm@69455:   where
wenzelm@69465:     open :: IO (Socket, ByteString)
wenzelm@69455:     open = do
wenzelm@69466:       server_socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol
wenzelm@69466:       Socket.bind server_socket (Socket.SockAddrInet 0 localhost)
wenzelm@69466:       Socket.listen server_socket 50
wenzelm@69462: 
wenzelm@69466:       port <- Socket.socketPort server_socket
wenzelm@69462:       let address = localhost_name ++ ":" ++ show port
wenzelm@69462:       password <- UUID.random
wenzelm@69462:       publish address password
wenzelm@69455: 
wenzelm@69466:       return (server_socket, UUID.bytes password)
wenzelm@69462: 
wenzelm@69465:     loop :: Socket -> ByteString -> IO ()
wenzelm@69466:     loop server_socket password = forever $ do
wenzelm@69480:       (connection, _) <- Socket.accept server_socket
wenzelm@69473:       Standard_Thread.fork_finally
wenzelm@69465:         (do
wenzelm@69465:           line <- Byte_Message.read_line connection
wenzelm@69465:           when (line == Just password) $ handle connection)
wenzelm@69473:         (\finally -> do
wenzelm@69472:           Socket.close connection
wenzelm@69473:           case finally of
wenzelm@69472:             Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn
wenzelm@69472:             Right () -> return ())
wenzelm@69455:       return ()
wenzelm@69455: \<close>
wenzelm@69455: 
wenzelm@69662: export_generated_files
wenzelm@69628: 
wenzelm@69222: end