src/Tools/Haskell/Properties.hs
author wenzelm
Fri, 23 Nov 2018 16:43:11 +0100
changeset 69334 6b49700da068
parent 69280 e1d01b351724
permissions -rw-r--r--
clarified font_domain: strict excludes e.g. space character;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69227
71b48b749836 tuned message (e.g. see Options.save_prefs);
wenzelm
parents: 69226
diff changeset
     1
{- generated by Isabelle -}
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
     2
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     3
{-  Title:      Tools/Haskell/Properties.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     4
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     5
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     6
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     7
Property lists.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69227
diff changeset
     8
e1d01b351724 more formal references;
wenzelm
parents: 69227
diff changeset
     9
See also "$ISABELLE_HOME/src/Pure/General/properties.ML".
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    10
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    11
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    12
module Isabelle.Properties (Entry, T, defined, get, put, remove)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    13
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    14
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    15
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    16
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    17
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    18
type Entry = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    19
type T = [Entry]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    20
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    21
defined :: T -> String -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    22
defined props name = any (\(a, _) -> a == name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    23
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    24
get :: T -> String -> Maybe String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    25
get props name = List.lookup name props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    26
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    27
put :: Entry -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    28
put entry props = entry : remove (fst entry) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    29
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    30
remove :: String -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    31
remove name props =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    32
  if defined props name then filter (\(a, _) -> a /= name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    33
  else props