author | wenzelm |
Mon, 05 Nov 2018 15:04:31 +0100 | |
changeset 69239 | 6cd985a78d6e |
parent 69227 | 71b48b749836 |
child 69280 | e1d01b351724 |
permissions | -rw-r--r-- |
{- generated by Isabelle -} {- Title: Tools/Haskell/Buffer.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Efficient text buffers. -} module Isabelle.Buffer (T, empty, add, content) where newtype T = Buffer [String] empty :: T empty = Buffer [] add :: String -> T -> T add "" buf = buf add x (Buffer xs) = Buffer (x : xs) content :: T -> String content (Buffer xs) = concat (reverse xs)