--- a/src/Tools/Haskell/Haskell.thy Sun Aug 22 21:39:57 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Sun Aug 22 21:58:29 2021 +0200
@@ -221,8 +221,6 @@
module Isabelle.Library (
(|>), (|->), (#>), (#->),
- the, the_default,
-
fold, fold_rev, single, map_index, get_index, separate,
StringLike, STRING (..), TEXT (..), BYTES (..),
@@ -258,17 +256,6 @@
(f #-> g) x = x |> f |-> g
-{- options -}
-
-the :: Maybe a -> a
-the (Just x) = x
-the Nothing = error "the Nothing"
-
-the_default :: a -> Maybe a -> a
-the_default x Nothing = x
-the_default _ (Just y) = y
-
-
{- lists -}
fold :: (a -> b -> b) -> [a] -> b -> b
@@ -1113,7 +1100,7 @@
Range, no_range, no_range_position, range_position, range
) where
-import Data.Maybe (isJust)
+import Data.Maybe (isJust, fromMaybe)
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Bytes as Bytes
import qualified Isabelle.Value as Value
@@ -1220,10 +1207,10 @@
{- markup properties -}
get_string :: Properties.T -> Bytes -> Bytes
-get_string props name = the_default "" (Properties.get_value Just props name)
+get_string props name = fromMaybe "" (Properties.get_value Just props name)
get_int :: Properties.T -> Bytes -> Int
-get_int props name = the_default 0 (Properties.get_value Value.parse_int props name)
+get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)
of_properties :: Properties.T -> T
of_properties props =
@@ -1412,6 +1399,8 @@
)
where
+import Data.Maybe (fromJust)
+
import Isabelle.Library
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Value as Value
@@ -1482,7 +1471,7 @@
option f (Just x) = [node (f x)]
variant :: [V a] -> T a
-variant fs x = [tagged (the (get_index (\f -> f x) fs))]
+variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
\<close>
generate_file "Isabelle/XML/Decode.hs" = \<open>