# HG changeset patch
# User wenzelm
# Date 1545144620 -3600
# Node ID 1690ba936016b4392d398ad06aad8227cc904d1f
# Parent  d93fe3557a98ff1cef9f5681ab13c1a15a8f785b
more Isabelle/Haskell operations;

diff -r d93fe3557a98 -r 1690ba936016 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