more Isabelle/Haskell operations;
authorwenzelm
Tue, 18 Dec 2018 15:50:20 +0100
changeset 69477 1690ba936016
parent 69476 d93fe3557a98
child 69478 c505f251f352
child 69480 2cc9212342a7
more Isabelle/Haskell operations;
src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Dec 16 14:34:12 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Tue Dec 18 15:50:20 2018 +0100
@@ -25,7 +25,7 @@
 
   fold, fold_rev, single, map_index, get_index,
 
-  quote, space_implode, commas, commas_quote, cat_lines,
+  proper_string, quote, space_implode, commas, commas_quote, cat_lines,
   space_explode, split_lines, trim_line, clean_name)
 where
 
@@ -91,6 +91,9 @@
 
 {- strings -}
 
+proper_string :: String -> Maybe String
+proper_string s = if null s then Nothing else Just s
+
 quote :: String -> String
 quote s = "\"" ++ s ++ "\""
 
@@ -222,7 +225,7 @@
 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/properties.ML\<close>.
 -}
 
-module Isabelle.Properties (Entry, T, defined, get, put, remove)
+module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
 where
 
 import qualified Data.List as List
@@ -237,6 +240,12 @@
 get :: T -> String -> Maybe String
 get props name = List.lookup name props
 
+get_value :: (String -> Maybe a) -> T -> String -> Maybe a
+get_value parse props name =
+  case get props name of
+    Nothing -> Nothing
+    Just s -> parse s
+
 put :: Entry -> T -> T
 put entry props = entry : remove (fst entry) props