Commit fe5f9554 authored by Michael Hanus's avatar Michael Hanus
Browse files

Small updates

parent 11427af6
......@@ -80,8 +80,8 @@ transDefaultRules verb moreopts _ prog = do
-- Filter proof obligations for determinism annotation w.r.t. to existence
-- of proof files:
filterProofObligation :: Int -> [String] -> [QName] -> IO [QName]
filterProofObligation verb prooffiles [] = return []
filterProofObligation verb prooffiles (qf@(qn,fn) : qfs) = do
filterProofObligation _ _ [] = return []
filterProofObligation verb prooffiles (qf@(_,fn) : qfs) = do
let hasdetproof = existsProofFor (determinismTheoremFor fn) prooffiles
when (hasdetproof && verb>0) $ putStrLn $
"Proofs for determinism property of " ++ showQName qf ++ " found:\n" ++
......
......@@ -7,7 +7,7 @@ Compile the model:
Fill the database:
> curry :l createData :eval createTestData :q
> curry :l CreateData :eval createTestData :q
Show the database with sqlite3:
......
......@@ -11,7 +11,7 @@ module Spicey (
nextController, nextControllerForData, confirmNextController,
confirmController, transactionController,
getControllerURL,getControllerParams, showControllerURL,
getForm, wDateType, wBoolean, wUncheckMaybe,
getForm, wDateType, wBoolean, wUncheckMaybe, wFloat,
displayError, cancelOperation,
renderWuiForm, renderLabels,
nextInProcessOr,
......@@ -24,13 +24,16 @@ module Spicey (
saveLastUrl, getLastUrl, getLastUrls
) where
import System
import Bootstrap3Style
import Char (isSpace,isDigit)
import HTML
import ReadNumeric
import KeyDatabase
import WUI
import ReadNumeric
import ReadShowTerm(readsQTerm)
import System
import Time
import WUI
import Routes
import Processes
import UserProcesses
......@@ -201,6 +204,26 @@ wUncheckMaybe defval wspec =
wspec
defval
--- A widget for editing floating point values.
wFloat :: WuiSpec Float
wFloat = transformWSpec (readFloat, show)
(wString `withCondition` (\s -> readMaybeFloat s /= Nothing))
where
readFloat s = maybe 0.0 id (readMaybeFloat s)
-- Read a float in a string.
-- Return Nothing is this is not a float string.
readMaybeFloat :: String -> Maybe Float
readMaybeFloat s =
if all isFloatChar s
then case readsQTerm s of
[(x,tail)] -> if all isSpace tail then Just x else Nothing
_ -> Nothing
else Nothing
where
isFloatChar c = isDigit c || c == '.'
stripSpaces = reverse . dropWhile isSpace . reverse . dropWhile isSpace
--------------------------------------------------------------------------
-- Define page layout of the application.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment