ConsistencyChecker.hs revision f153609d4ff5616d7caa410df605afcdfb9956df
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Consistency Checker GUI.
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Rainer Grabbe, Uni Bremen 2007
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : rainer@informatik.uni-bremen.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (uses uni, needs POSIX)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiGeneric GUI for consistency checker. Based upon genericATP GUI.
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskimodule GUI.ConsistencyChecker (ccgui) where
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport Common.Utils (getEnvSave)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Control.Exception as Exception
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Control.Concurrent as Conc
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederimport SpinButton
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Messages
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport TextDisplay
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport Separator
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport XSelection
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiimport ScrollBar
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- ** Constants
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Default time limit for the GUI mode prover in seconds.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiguiDefaultTimeLimit :: Int
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiguiDefaultTimeLimit = 10
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- ** Defining the view
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Colors used by the GUI to indicate the status of a spec.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata CheckStatusColour
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- | Consistent
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- | Time-consistent
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | Inconsistent
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- | Not checked
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving (Bounded,Enum,Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Generates a ('CheckStatusColour', 'String') tuple representing a consistent
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski specification status.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederstatusConsistent :: (CheckStatusColour, String)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederstatusConsistent = (Green, "Consistent")
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Generates a ('CheckStatusColour', 'String') tuple representing a time
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski consistentProved specification status.
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederstatusTConsistent :: (CheckStatusColour, String)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederstatusTConsistent = (Brown, "t-consistent")
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- | Generates a ('CheckStatusColour', 'String') tuple representing an
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder inconsistent specification status. -}
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederstatusInconsistent :: (CheckStatusColour, String)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederstatusInconsistent = (Red, "Inconsistent")
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Generates a ('CheckStatusColour', 'String') tuple representing an open (not
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder yet checked) specification status.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederstatusNotChecked :: (CheckStatusColour, String)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederstatusNotChecked = (Black, "Not checked")
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Generates a ('CheckStatusColour', 'String') tuple representing a running
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski specification status.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederstatusRunning :: (CheckStatusColour, String)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederstatusRunning = (Blue, "Running")
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder{- | stores widgets of an options frame and the frame itself -}
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederdata OpFrame = OpFrame
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder { of_Frame :: Frame
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , of_timeSpinner :: SpinButton
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , of_timeEntry :: Entry Int
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , of_optionsEntry :: Entry String }
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- * GUI Implementation
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- ** Utility Functions
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Retrieves the value of the time limit 'Entry'. Ignores invalid input.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetValueSafe :: Int -- ^ default time limt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Entry Int -- ^ time limit 'Entry'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> IO Int -- ^ user-requested time limit or default in case of a
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -- parse error
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetValueSafe defaultTimeLimit timeEntry =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Exception.catchJust Exception.userErrors ((getValue timeEntry) :: IO Int)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (const $ return defaultTimeLimit)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | Text displayed by the batch mode window.
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederbatchInfoText :: Int -- ^ batch time limt
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -> Int -- ^ total number of goals
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -> Int -- ^ number of that have been processed
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederbatchInfoText tl gTotal gDone =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let totalSecs = (gTotal - gDone) * tl
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (remMins,secs) = divMod totalSecs 60
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (hours,mins) = divMod remMins 60
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski "Batch mode running.\n" ++
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski show gDone ++ "/" ++ show gTotal ++ " goals processed.\n" ++
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski "At most " ++ show hours ++ "h " ++ show mins ++ "m " ++ show secs ++
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski "s remaining."
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski-- ** Callbacks
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Depending on the first argument all entries in a ListBox are selected
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski or deselected
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederdoSelectAllEntries :: Bool -- ^ indicates wether all entries should be selected
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- or deselected
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> ListBox a -> IO ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederdoSelectAllEntries selectAll lb =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if selectAll then selectionRange (0 :: Int) EndOfText lb >> return () else
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder clearSelection lb
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- !! updateDisplay
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedernewOptionsFrame :: Container par =>
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder par -- ^ the parent container
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> (Entry Int -> Spin -> IO a)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- ^ Function called by pressing one spin button
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> Bool -- ^ extra options input line
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> IO OpFrame
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedernewOptionsFrame con updateFn isExtraOps = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder right <- newFrame con []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- contents of newOptionsFrame
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder l1 <- newLabel right [text "Options:"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack l1 [Anchor NorthWest]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder opFrame <- newFrame right []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack opFrame [Expand On, Fill X, Anchor North]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder spacer <- newLabel opFrame [text " "]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack spacer [Side AtLeft]
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder opFrame2 <- newVBox opFrame []
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder pack opFrame2 [Expand On, Fill X, Anchor NorthWest]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder timeLimitFrame <- newFrame opFrame2 []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack timeLimitFrame [Expand On, Fill X, Anchor West]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder l2 <- newLabel timeLimitFrame [text "TimeLimit"]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack l2 [Side AtLeft]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- extra HBox for time limit display
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder timeLimitLine <- newHBox timeLimitFrame []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack timeLimitLine [Expand On, Side AtRight, Anchor East]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (timeEntry :: Entry Int) <- newEntry timeLimitLine [width 18,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder HTk.value guiDefaultTimeLimit]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack timeEntry []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski timeSpinner <- newSpinButton timeLimitLine (updateFn timeEntry) []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack timeSpinner []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder l3 <- newLabel opFrame2 [text "Extra Options:"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski when isExtraOps $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack l3 [Anchor West]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (optionsEntry :: Entry String) <- newEntry opFrame2 [width 37]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski when isExtraOps $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack optionsEntry [Fill X, PadX (cm 0.1)]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return OpFrame
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { of_Frame = right
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , of_timeSpinner = timeSpinner
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , of_timeEntry = timeEntry
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , of_optionsEntry = optionsEntry }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- ** Main GUI
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Invokes the consistency checker GUI. Users may start the batch prover run on
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski all goals, or use a detailed GUI for proving each goal manually.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederccgui :: IO ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- create initial backing data structure
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- !! test value
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let batchTLimit = (20 :: Integer)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- !! test stub
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let specName = "Foo bar spec name"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- !! still need to know why the left listbox is too small in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- x-direction (has too much space)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- main window
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski main <- createToplevel [text $ specName ++ " - Concistency Checker"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack main [Expand On, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- VBox for the whole window
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski b <- newVBox main []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack b [Expand On, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- HBox for the upper part (specs on the left, options/results on the right)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski b2 <- newHBox b []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack b2 [Expand On, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski left <- newVBox b2 []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack left [Expand On, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski l0 <- newLabel left [text "Specifications:"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack l0 [Anchor NorthWest]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lbFrame <- newFrame left []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack lbFrame [Expand On, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lb <- newListBox lbFrame
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , exportSelection False
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , selectMode Multiple, height 15] :: IO (ListBox String)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack lb [Expand On, Side AtLeft, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sb <- newScrollBar lbFrame []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack sb [Expand On, Side AtRight, Fill Y, Anchor West]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lb # scrollbar Vertical sb
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lb # HTk.value ["1", "2", "7", "33"] -- !! test
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder selHBox <- newHBox left []
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder pack selHBox [Expand Off, Fill None, Anchor West]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski selectAllButton <- newButton selHBox [text "Select all"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack selectAllButton []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deselectAllButton <- newButton selHBox [text "Deselect all"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack deselectAllButton []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski selectUncheckedButton <- newButton left
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder [text "Select unchecked specifications"]
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder pack selectUncheckedButton [Anchor West]
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder right <- newVBox b2 []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack right [Expand Off, Fill Y, Anchor NorthWest]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- !! some functionality is still missing. ;)
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -- right frame (options/results)
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder OpFrame { of_Frame = opRight
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , of_timeSpinner = timeSpinner
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder , of_timeEntry = timeEntry
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder , of_optionsEntry = optionsEntry}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <- newOptionsFrame right
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (\ timeEntry sp -> synchronize main
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack opRight [Expand Off, Fill Both]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- buttons for options
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski buttonsHb1 <- newHBox right []
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder pack buttonsHb1 [Anchor NorthEast]
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder saveCheckButton <- newButton buttonsHb1 [text $ "Save check info"]
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder pack saveCheckButton []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski stopButton <- newButton buttonsHb1 [text "Stop"]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pack stopButton []
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder runButton <- newButton buttonsHb1 [text "Check"]
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder pack runButton []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let vspacing = cm 0.2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- status lines
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski stBox <- newVBox right []
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder pack stBox [Fill X]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski l1 <- newLabel stBox [text "Status:"]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder pack l1 [Anchor West]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder statusLabel <- newLabel stBox [text "(dummy) current state"]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack statusLabel [Anchor West, PadX (cm 0.5)]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vsp1 <- newSpace stBox vspacing []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder l2 <- newLabel stBox [text "Sublogic of currently selected specifications:"]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack l2 [Anchor West]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sublogicLabel <- newLabel stBox [text "(dummy) some sublogic"]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack sublogicLabel [Anchor West, PadX (cm 0.5)]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vsp2 <- newSpace stBox vspacing []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder l3 <- newLabel stBox [text "Current specification"]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack l3 [Anchor West]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder specLabel <- newLabel stBox [text "(dummy) some spec"]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack specLabel [Anchor West, PadX (cm 0.5)]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder vsp3 <- newSpace stBox vspacing []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- consistency checker frame
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder conCheckFrame <- newFrame right []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack conCheckFrame [Fill Both, Anchor NorthWest]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder l4 <- newLabel conCheckFrame
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder [text ("Select a specific consistency checker:")]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pack l4 [Anchor West]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder conCheckIFrame <- newFrame conCheckFrame []
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski pack conCheckIFrame [Fill Both, Anchor NorthWest, PadX (cm 0.5)]
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder conCheckLb <- newListBox conCheckIFrame
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder [ HTk.value ([] :: [String])
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder , exportSelection False
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder , selectMode Browse
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , height 4 ] :: IO (ListBox String)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack conCheckLb [Expand On, Fill Both, Side AtLeft]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder conCheckSb <- newScrollBar conCheckIFrame []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack conCheckSb [Fill Y, Side AtRight]
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski conCheckLb # scrollbar Vertical conCheckSb
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder moreButton <- newButton right [text "More fine grained selection..."]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack moreButton [Side AtBottom, Anchor East]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sp1_1 <- newSpace b (cm 0.15) []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pack sp1_1 [Expand Off, Fill X, Side AtBottom]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder newHSeparator b
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski sp1_2 <- newSpace b (cm 0.15) []
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pack sp1_2 [Expand Off, Fill X, Side AtBottom]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder -- bottom frame (help/show/exit buttons)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski bottom <- newHBox b []
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pack bottom [Expand Off, Fill Both]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski helpButton <- newButton bottom [text "Help"]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pack helpButton [PadX (cm 0.3), IPadX (cm 0.1)]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski showSumButton <- newButton bottom [text "Show summary"]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pack showSumButton [PadX (cm 0.3)]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski exitButton <- newButton bottom [text "Close"]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pack exitButton [PadX (cm 0.3), IPadX (cm 0.1)]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski saveCheckButton <- newButton buttonsHb1 [text $ "Save check info"]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pack saveCheckButton []
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski stopButton <- newButton buttonsHb1 [text "Stop"]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder pack stopButton []
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski runButton <- newButton buttonsHb1 [text "Check"]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let specWids = map EnW [saveCheckButton, runButton, moreButton]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski wids = [EnW lb, EnW conCheckLb] ++ specWids ++ map EnW
a938729e277da5c7742bb88946ab2c150416fd5dTill Mossakowski [ selectAllButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , deselectAllButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , selectUncheckedButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , showSumButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , exitButton ]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski enableWidsUponSelection lb specWids
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski disable stopButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski putWinOnTop main
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- MVars for thread-safe communication
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski mVar_batchId <- Conc.newEmptyMVar :: IO (Conc.MVar Conc.ThreadId)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski windowDestroyedMVar <- Conc.newEmptyMVar :: IO (Conc.MVar ())
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (selectGoal, _) <- bindSimple lb (ButtonPress (Just 1))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski selectAll <- clicked selectAllButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski deselectAll <- clicked deselectAllButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski selectUnchecked <- clicked selectUncheckedButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski runCheck <- clicked runButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski stopCheck <- clicked stopButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski help <- clicked helpButton
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski showSummary <- clicked showSumButton
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder exit <- clicked exitButton
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder (closeWindow,_) <- bindSimple main Destroy
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -- event handlers (much to do!!)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- !! mvars missing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ((selectGoal >>> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski enableWidsUponSelection lb specWids
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder +> (help >>> do
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder createTextDisplay ("Help")
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("No help available yet.")
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder [size (80, 30)]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder +> (showSummary >>> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder createTextSaveDisplay
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("Status Summary of all checked specifications")
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("nothing yet")
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder +> (deselectAll >>> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder doSelectAllEntries False lb
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder disableWids specWids
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder +> (selectAll >>> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder doSelectAllEntries True lb
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder enableWids specWids
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder +> (runCheck >>> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder disableWids wids
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder enable stopButton
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski +> (stopCheck >>> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder enableWids wids
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder disable stopButton
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sync ( (exit >>> destroy main)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder +> (closeWindow >>> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder destroy main)