{- |

Module : $Header$

Copyright : (c) K. Luettich, Rene Wagner, Uni Bremen 2002-2005

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (imports HTk)

Utilities on top of HTk

-}

module GUI.HTkUtils

( LBGoalView (..)

, LBStatusIndicator (..)

, EnableWid (..)

, GUIMVar

, listBox

, errorMess

, confirmMess

, messageMess

, askFileNameAndSave

, createTextSaveDisplay

, newFileDialogStr

, fileDialogStr

, displayTheory

, displayTheoryWithWarning

, populateGoalsListBox

, indicatorFromProofStatus

, indicatorFromBasicProof

, indicatorString

, enableWids

, disableWids

, enableWidsUponSelection

, module HTk.Toplevel.HTk

, module HTk.Toolkit.ScrollBox

, module HTk.Toolkit.SimpleForm

, module HTk.Toolkit.TextDisplay

) where

import System.Directory

import Util.Messages

import HTk.Toplevel.HTk hiding (x, y)

import HTk.Toolkit.ScrollBox

import HTk.Toolkit.SimpleForm

import HTk.Toolkit.TextDisplay

import HTk.Toolkit.FileDialog

import Logic.Prover

import Static.GTheory

import Common.DocUtils

import Control.Concurrent.MVar

-- ** some types

-- | Type for storing the proof management window

type GUIMVar = MVar (Maybe Toplevel)

-- | create a window with title and list of options, return selected option

listBox :: String -> [String] -> IO (Maybe Int)

listBox title entries =

do

main <- createToplevel [text title]

lb <- newListBox main [value entries, bg "white", size (100, 39)] ::

IO (ListBox String)

pack lb [Side AtLeft, Expand On, Fill Both]

scb <- newScrollBar main []

pack scb [Side AtRight, Fill Y]

lb # scrollbar Vertical scb

(press, _) <- bindSimple lb (ButtonPress (Just 1))

(closeWindow,_) <- bindSimple main Destroy

sync ( (press >>> do

sel <- getSelection lb

destroy main

return (case sel of

Just [i] -> Just i

_ -> Nothing) )

+> (closeWindow >>> do

destroy main

return Nothing ))

-- |

-- Display some (longish) text in an uneditable, scrollable editor.

-- Returns immediately-- the display is forked off to separate thread.

createTextSaveDisplayExt :: String -- ^ title of the window

-> String -- ^ default filename for saving the text

-> String -- ^ text to be displayed

-> [Config Editor] -- ^ configuration options for

-- the text editor

-> IO() -- ^ action to be executed when

-- the window is closed

-> IO (Toplevel,Editor) -- ^ the window in which

-- the text is displayed

createTextSaveDisplayExt title fname txt conf upost =

do win <- createToplevel [text title]

b <- newFrame win [relief Groove, borderwidth (cm 0.05)]

t <- newLabel b [text title, font (Helvetica, Roman, 18::Int)]

q <- newButton b [text "Close", width 12]

s <- newButton b [text "Save", width 12]

(sb, ed) <- newScrollBox b (\p-> newEditor p conf) []

ed # state Disabled

pack b [Side AtTop, Fill Both,Expand On]

pack t [Side AtTop, Expand Off, PadY 10]

pack sb [Side AtTop, Expand On,Fill Both]

pack ed [Side AtTop, Expand On, Fill Both]

pack q [Side AtRight, PadX 8, PadY 5]

pack s [Side AtLeft, PadX 5, PadY 5]

ed # state Normal

ed # value txt

ed # state Disabled

forceFocus ed

(editClicked, _) <- bindSimple ed (ButtonPress (Just 1))

quit <- clicked q

save <- clicked s

spawnEvent (forever (quit >>> do destroy win; upost

+>

save >>> do disableButs q s

askFileNameAndSave fname txt

enableButs q s

done

+>

editClicked >>> forceFocus ed))

return (win, ed)

where disableButs b1 b2 = do disable b1

disable b2

enableButs b1 b2 = do enable b1

enable b2

-- |

-- Display some (longish) text in an uneditable, scrollable editor.

-- Simplified version of createTextSaveDisplayExt

createTextSaveDisplay :: String -- ^ title of the window

-> String -- ^ default filename for saving the text

-> String -- ^ text to be displayed

-> IO()

createTextSaveDisplay t f txt =

do createTextSaveDisplayExt t f txt [size(100,44)] done; done

--- added by KL

-- |

-- opens a FileDialog and saves to the selected file if OK is clicked

-- otherwise nothing happens

askFileNameAndSave :: String -- ^ default filename for saving the text

-> String -- ^ text to be saved

-> IO ()

askFileNameAndSave defFN txt =

do curDir <- getCurrentDirectory

selev <- newFileDialogStr "Save file" (curDir++'/':defFN)

mfile <- sync selev

maybe done saveFile mfile

where saveFile fp = writeFile fp txt

-- | displays a theory in a window

displayTheory :: String -- ^ kind of theory

-> String -- ^ name of theory

-> G_theory -> IO ()

displayTheory kind thname gth =

let str = showDoc gth "\n"

title = kind ++ " of " ++ thname

in createTextSaveDisplay title (thname++".het") str

{- | returns a window displaying the given theory and the given

warning text.

-}

displayTheoryWithWarning :: String -- ^ kind of theory

-> String -- ^ name of theory

-> String -- ^ warning text

-> G_theory -- ^ to be shown theory

-> IO ()

displayTheoryWithWarning kind thname warningTxt gth =

let str = warningTxt ++ (showDoc gth "\n")

title = kind ++ " of " ++ thname

in createTextSaveDisplay title (thname++".het") str

--- added by RW

{- |

Represents the state of a goal in a 'ListBox' that uses 'populateGoalsListBox'

-}

data LBStatusIndicator = LBIndicatorProved

| LBIndicatorProvedInconsistent

| LBIndicatorDisproved

| LBIndicatorOpen

| LBIndicatorGuessed

| LBIndicatorConjectured

| LBIndicatorHandwritten

-- |

-- Converts a 'LBStatusIndicator' into a short 'String' representing it in

-- a 'ListBox'

indicatorString :: LBStatusIndicator

-> String

indicatorString i = case i of

LBIndicatorProved -> "[+]"

LBIndicatorProvedInconsistent -> "[*]"

LBIndicatorDisproved -> "[-]"

LBIndicatorOpen -> "[ ]"

LBIndicatorGuessed -> "[.]"

LBIndicatorConjectured -> "[:]"

LBIndicatorHandwritten -> "[/]"

-- |

-- Represents a goal in a 'ListBox' that uses 'populateGoalsListBox'

data LBGoalView = LBGoalView { -- | status indicator

statIndicator :: LBStatusIndicator,

-- | description

goalDescription :: String

}

-- |

-- Populates a 'ListBox' with goals. After the initial call to this function

-- the number of goals is assumed to remain constant in ensuing calls.

populateGoalsListBox :: ListBox String -- ^ listbox

-> [LBGoalView] -- ^ list of goals

-- length must remain constant after the first call

-> IO ()

populateGoalsListBox lb v = do

selectedOld <- (getSelection lb) :: IO (Maybe [Int])

lb # value (toString v)

maybe (return ()) (mapM_ (\n -> selection n lb)) selectedOld

where

toString = map (\ LBGoalView {statIndicator = i, goalDescription = d} ->

(indicatorString i) ++ (' ' : d))

-- | Converts a 'Logic.Prover.ProofStatus' into a 'LBStatusIndicator'

indicatorFromProofStatus :: ProofStatus a

-> LBStatusIndicator

indicatorFromProofStatus st = case goalStatus st of

Proved mc -> maybe LBIndicatorProved

(\ c -> if c then LBIndicatorProved

else LBIndicatorProvedInconsistent)

mc

Disproved -> LBIndicatorDisproved

Open _ -> LBIndicatorOpen

-- | Converts a 'BasicProof' into a 'LBStatusIndicator'

indicatorFromBasicProof :: BasicProof

-> LBStatusIndicator

indicatorFromBasicProof p = case p of

BasicProof _ st -> indicatorFromProofStatus st

Guessed -> LBIndicatorGuessed

Conjectured -> LBIndicatorConjectured

Handwritten -> LBIndicatorHandwritten

-- | existential type for widgets that can be enabled and disabled

data EnableWid = forall wid . HasEnable wid => EnW wid

enableWids :: [EnableWid] -> IO ()

enableWids = mapM_ ( \ ew -> case ew of EnW w -> enable w >> return ())

disableWids :: [EnableWid] -> IO ()

disableWids = mapM_ ( \ ew -> case ew of EnW w -> disable w >> return ())

-- | enables widgets only if at least one entry is selected in the listbox,

-- otherwise the widgets are disabled

enableWidsUponSelection :: ListBox String -> [EnableWid] -> IO ()

enableWidsUponSelection lb goalSpecificWids =

do sel <- (getSelection lb) :: IO (Maybe [Int])

maybe (disableWids goalSpecificWids)

(const $ enableWids goalSpecificWids)

sel