{-# LANGUAGE ExistentialQuantification #-}
module GUI.HTkUtils
( LBGoalView (..)
, LBStatusIndicator (..)
, EnableWid (..)
, GUIMVar
, listBox
, errorMess
, confirmMess
, messageMess
, askFileNameAndSave
, createTextSaveDisplay
, newFileDialogStr
, fileDialogStr
, displayTheoryWithWarning
, populateGoalsListBox
, indicatorFromProofStatus
, indicatorFromBasicProof
, indicatorString
, enableWids
, disableWids
, enableWidsUponSelection
, module X
) where
import System.Directory
import Util.Messages
import HTk.Toplevel.HTk as X hiding (x, y)
import HTk.Toolkit.ScrollBox as X
import HTk.Toolkit.SimpleForm as X
import HTk.Toolkit.TextDisplay as X
import HTk.Toolkit.FileDialog
import Logic.Prover
import Static.GTheory
import Common.DocUtils
import Control.Concurrent.MVar
type GUIMVar = MVar (Maybe Toplevel)
listBox :: String -> [String] -> IO (Maybe Int)
listBox :: String -> [String] -> IO (Maybe Int)
listBox title :: String
title entries :: [String]
entries =
do
Toplevel
main <- [Config Toplevel] -> IO Toplevel
createToplevel [String -> Config Toplevel
forall w v. HasText w v => v -> Config w
text String
title]
ListBox String
lb <- Toplevel -> [Config (ListBox String)] -> IO (ListBox String)
forall par a.
(Container par, GUIValue a) =>
par -> [Config (ListBox a)] -> IO (ListBox a)
newListBox Toplevel
main [[String] -> Config (ListBox String)
forall w v. HasValue w v => v -> Config w
value [String]
entries, String -> Config (ListBox String)
forall c w. (ColourDesignator c, HasColour w) => c -> Config w
bg "white", Size -> Config (ListBox String)
forall w. HasSize w => Size -> Config w
size (100, 39)] ::
IO (ListBox String)
ListBox String -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack ListBox String
lb [SideSpec -> PackOption
Side SideSpec
AtLeft, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
Both]
ScrollBar
scb <- Toplevel -> [Config ScrollBar] -> IO ScrollBar
forall par.
Container par =>
par -> [Config ScrollBar] -> IO ScrollBar
newScrollBar Toplevel
main []
ScrollBar -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack ScrollBar
scb [SideSpec -> PackOption
Side SideSpec
AtRight, FillSpec -> PackOption
Fill FillSpec
Y]
ListBox String
lb ListBox String -> Config (ListBox String) -> IO (ListBox String)
forall a b. a -> (a -> b) -> b
# Orientation -> ScrollBar -> Config (ListBox String)
forall w. HasScroller w => Orientation -> ScrollBar -> Config w
scrollbar Orientation
Vertical ScrollBar
scb
(press :: Event ()
press, _) <- ListBox String -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple ListBox String
lb (Maybe Int -> WishEventType
ButtonPress (Int -> Maybe Int
forall a. a -> Maybe a
Just 1))
(closeWindow :: Event ()
closeWindow, _) <- Toplevel -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple Toplevel
main WishEventType
Destroy
Event (Maybe Int) -> IO (Maybe Int)
forall a. Event a -> IO a
sync ( (Event ()
press Event () -> IO (Maybe Int) -> Event (Maybe Int)
forall a b. Event a -> IO b -> Event b
>>> do
Maybe [Int]
sel <- ListBox String -> IO (Maybe [Int])
forall w i. HasSelectionBaseIndex w i => w -> IO (Maybe i)
getSelection ListBox String
lb
Toplevel -> IO ()
forall o. Destroyable o => o -> IO ()
destroy Toplevel
main
Maybe Int -> IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (case Maybe [Int]
sel of
Just [i :: Int
i] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
_ -> Maybe Int
forall a. Maybe a
Nothing) )
Event (Maybe Int) -> Event (Maybe Int) -> Event (Maybe Int)
forall a. Event a -> Event a -> Event a
+> (Event ()
closeWindow Event () -> IO (Maybe Int) -> Event (Maybe Int)
forall a b. Event a -> IO b -> Event b
>>> do
Toplevel -> IO ()
forall o. Destroyable o => o -> IO ()
destroy Toplevel
main
Maybe Int -> IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing ))
createTextSaveDisplayExt :: String
-> String
-> String
-> [Config Editor]
-> IO ()
-> IO (Toplevel, Editor)
createTextSaveDisplayExt :: String
-> String
-> String
-> [Config Editor]
-> IO ()
-> IO (Toplevel, Editor)
createTextSaveDisplayExt title :: String
title fname :: String
fname txt :: String
txt conf :: [Config Editor]
conf upost :: IO ()
upost =
do Toplevel
win <- [Config Toplevel] -> IO Toplevel
createToplevel [String -> Config Toplevel
forall w v. HasText w v => v -> Config w
text String
title]
Frame
b <- Toplevel -> [Config Frame] -> IO Frame
forall par. Container par => par -> [Config Frame] -> IO Frame
newFrame Toplevel
win [Relief -> Config Frame
forall w. HasBorder w => Relief -> Config w
relief Relief
Groove, Distance -> Config Frame
forall w. HasBorder w => Distance -> Config w
borderwidth (Double -> Distance
cm 0.05)]
Label
t <- Frame -> [Config Label] -> IO Label
forall par. Container par => par -> [Config Label] -> IO Label
newLabel Frame
b [String -> Config Label
forall w v. HasText w v => v -> Config w
text String
title, (FontFamily, FontSlant, Int) -> Config Label
forall w f. (HasFont w, FontDesignator f) => f -> Config w
font (FontFamily
Helvetica, FontSlant
Roman, 18 :: Int)]
Button
q <- Frame -> [Config Button] -> IO Button
forall par. Container par => par -> [Config Button] -> IO Button
newButton Frame
b [String -> Config Button
forall w v. HasText w v => v -> Config w
text "Close", Distance -> Config Button
forall w. HasSize w => Distance -> Config w
width 12]
Button
s <- Frame -> [Config Button] -> IO Button
forall par. Container par => par -> [Config Button] -> IO Button
newButton Frame
b [String -> Config Button
forall w v. HasText w v => v -> Config w
text "Save", Distance -> Config Button
forall w. HasSize w => Distance -> Config w
width 12]
(sb :: ScrollBox Editor
sb, ed :: Editor
ed) <- Frame
-> (Frame -> IO Editor)
-> [Config (ScrollBox Editor)]
-> IO (ScrollBox Editor, Editor)
forall wid par.
(Widget wid, HasScroller wid, Container par) =>
par
-> (Frame -> IO wid)
-> [Config (ScrollBox wid)]
-> IO (ScrollBox wid, wid)
newScrollBox Frame
b (Frame -> [Config Editor] -> IO Editor
forall par. Container par => par -> [Config Editor] -> IO Editor
`newEditor` [Config Editor]
conf) []
Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Disabled
Frame -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Frame
b [SideSpec -> PackOption
Side SideSpec
AtTop, FillSpec -> PackOption
Fill FillSpec
Both, Toggle -> PackOption
Expand Toggle
On]
Label -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Label
t [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
Off, Distance -> PackOption
PadY 10]
ScrollBox Editor -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack ScrollBox Editor
sb [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
Both]
Editor -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Editor
ed [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
Both]
Button -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Button
q [SideSpec -> PackOption
Side SideSpec
AtRight, Distance -> PackOption
PadX 8, Distance -> PackOption
PadY 5]
Button -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Button
s [SideSpec -> PackOption
Side SideSpec
AtLeft, Distance -> PackOption
PadX 5, Distance -> PackOption
PadY 5]
Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Normal
Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# String -> Config Editor
forall w v. HasValue w v => v -> Config w
value String
txt
Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Disabled
Editor -> IO ()
forall w. Widget w => w -> IO ()
forceFocus Editor
ed
(editClicked :: Event ()
editClicked, _) <- Editor -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple Editor
ed (Maybe Int -> WishEventType
ButtonPress (Int -> Maybe Int
forall a. a -> Maybe a
Just 1))
Event ()
quit <- Button -> IO (Event ())
forall w. HasCommand w => w -> IO (Event ())
clicked Button
q
Event ()
save <- Button -> IO (Event ())
forall w. HasCommand w => w -> IO (Event ())
clicked Button
s
IO ()
_ <- Event () -> IO (IO ())
spawnEvent (Event () -> IO (IO ())) -> Event () -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ Event () -> Event ()
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (Event () -> Event ()) -> Event () -> Event ()
forall a b. (a -> b) -> a -> b
$ Event ()
quit Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> (Toplevel -> IO ()
forall o. Destroyable o => o -> IO ()
destroy Toplevel
win IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
upost)
Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
save Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> do
Button -> Config Button
forall a b. (HasEnable a, HasEnable b) => a -> b -> IO b
disableButs Button
q Button
s
String -> String -> IO ()
askFileNameAndSave String
fname String
txt
Button -> Config Button
forall a b. (HasEnable a, HasEnable b) => a -> b -> IO b
enableButs Button
q Button
s
IO ()
forall (m :: * -> *). Monad m => m ()
done
Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
editClicked Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> Editor -> IO ()
forall w. Widget w => w -> IO ()
forceFocus Editor
ed
(Toplevel, Editor) -> IO (Toplevel, Editor)
forall (m :: * -> *) a. Monad m => a -> m a
return (Toplevel
win, Editor
ed)
where disableButs :: a -> b -> IO b
disableButs b1 :: a
b1 b2 :: b
b2 = Config a
forall w. HasEnable w => Config w
disable a
b1 IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> IO b
forall w. HasEnable w => Config w
disable b
b2
enableButs :: a -> b -> IO b
enableButs b1 :: a
b1 b2 :: b
b2 = Config a
forall w. HasEnable w => Config w
enable a
b1 IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> IO b
forall w. HasEnable w => Config w
enable b
b2
createTextSaveDisplay :: String
-> String
-> String
-> IO ()
createTextSaveDisplay :: String -> String -> String -> IO ()
createTextSaveDisplay t :: String
t f :: String
f txt :: String
txt = do
String
-> String
-> String
-> [Config Editor]
-> IO ()
-> IO (Toplevel, Editor)
createTextSaveDisplayExt String
t String
f String
txt [Size -> Config Editor
forall w. HasSize w => Size -> Config w
size (100, 44)] IO ()
forall (m :: * -> *). Monad m => m ()
done
IO ()
forall (m :: * -> *). Monad m => m ()
done
askFileNameAndSave :: String
-> String
-> IO ()
askFileNameAndSave :: String -> String -> IO ()
askFileNameAndSave defFN :: String
defFN txt :: String
txt =
do String
curDir <- IO String
getCurrentDirectory
Event (Maybe String)
selev <- String -> String -> IO (Event (Maybe String))
newFileDialogStr "Save file" (String
curDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ '/' Char -> String -> String
forall a. a -> [a] -> [a]
: String
defFN)
Maybe String
mfile <- Event (Maybe String) -> IO (Maybe String)
forall a. Event a -> IO a
sync Event (Maybe String)
selev
IO () -> (String -> IO ()) -> Maybe String -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall (m :: * -> *). Monad m => m ()
done String -> IO ()
saveFile Maybe String
mfile
where saveFile :: String -> IO ()
saveFile fp :: String
fp = String -> String -> IO ()
writeFile String
fp String
txt
displayTheoryWithWarning :: String
-> String
-> String
-> G_theory
-> IO ()
displayTheoryWithWarning :: String -> String -> String -> G_theory -> IO ()
displayTheoryWithWarning kind :: String
kind thname :: String
thname warningTxt :: String
warningTxt gth :: G_theory
gth =
let str :: String
str = String
warningTxt String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_theory -> String -> String
forall a. Pretty a => a -> String -> String
showDoc G_theory
gth "\n"
title :: String
title = String
kind String -> String -> String
forall a. [a] -> [a] -> [a]
++ " of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thname
in String -> String -> String -> IO ()
createTextSaveDisplay String
title (String
thname String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".dol") String
str
data LBStatusIndicator = LBIndicatorProved
| LBIndicatorProvedInconsistent
| LBIndicatorDisproved
| LBIndicatorOpen
| LBIndicatorGuessed
| LBIndicatorConjectured
| LBIndicatorHandwritten
indicatorString :: LBStatusIndicator
-> String
indicatorString :: LBStatusIndicator -> String
indicatorString i :: LBStatusIndicator
i = case LBStatusIndicator
i of
LBIndicatorProved -> "[+]"
LBIndicatorProvedInconsistent -> "[*]"
LBIndicatorDisproved -> "[-]"
LBIndicatorOpen -> "[ ]"
LBIndicatorGuessed -> "[.]"
LBIndicatorConjectured -> "[:]"
LBIndicatorHandwritten -> "[/]"
data LBGoalView = LBGoalView {
LBGoalView -> LBStatusIndicator
statIndicator :: LBStatusIndicator,
LBGoalView -> String
goalDescription :: String
}
populateGoalsListBox :: ListBox String
-> [LBGoalView]
-> IO ()
populateGoalsListBox :: ListBox String -> [LBGoalView] -> IO ()
populateGoalsListBox lb :: ListBox String
lb v :: [LBGoalView]
v = do
Maybe [Int]
selectedOld <- ListBox String -> IO (Maybe [Int])
forall w i. HasSelectionBaseIndex w i => w -> IO (Maybe i)
getSelection ListBox String
lb :: IO (Maybe [Int])
ListBox String
lb ListBox String -> Config (ListBox String) -> IO (ListBox String)
forall a b. a -> (a -> b) -> b
# [String] -> Config (ListBox String)
forall w v. HasValue w v => v -> Config w
value ([LBGoalView] -> [String]
toString [LBGoalView]
v)
IO () -> ([Int] -> IO ()) -> Maybe [Int] -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Int -> IO (ListBox String)) -> [Int] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int -> Config (ListBox String)
forall w i. HasSelectionIndex w i => i -> Config w
`selection` ListBox String
lb)) Maybe [Int]
selectedOld
where
toString :: [LBGoalView] -> [String]
toString = (LBGoalView -> String) -> [LBGoalView] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ LBGoalView {statIndicator :: LBGoalView -> LBStatusIndicator
statIndicator = LBStatusIndicator
i, goalDescription :: LBGoalView -> String
goalDescription = String
d} ->
LBStatusIndicator -> String
indicatorString LBStatusIndicator
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
d)
indicatorFromProofStatus :: ProofStatus a
-> LBStatusIndicator
indicatorFromProofStatus :: ProofStatus a -> LBStatusIndicator
indicatorFromProofStatus st :: ProofStatus a
st = case ProofStatus a -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus a
st of
Proved c :: Bool
c -> if Bool
c then LBStatusIndicator
LBIndicatorProved else LBStatusIndicator
LBIndicatorProvedInconsistent
Disproved -> LBStatusIndicator
LBIndicatorDisproved
Open _ -> LBStatusIndicator
LBIndicatorOpen
indicatorFromBasicProof :: BasicProof
-> LBStatusIndicator
indicatorFromBasicProof :: BasicProof -> LBStatusIndicator
indicatorFromBasicProof p :: BasicProof
p = case BasicProof
p of
BasicProof _ st :: ProofStatus proof_tree
st -> ProofStatus proof_tree -> LBStatusIndicator
forall a. ProofStatus a -> LBStatusIndicator
indicatorFromProofStatus ProofStatus proof_tree
st
Guessed -> LBStatusIndicator
LBIndicatorGuessed
Conjectured -> LBStatusIndicator
LBIndicatorConjectured
Handwritten -> LBStatusIndicator
LBIndicatorHandwritten
data EnableWid = forall wid . HasEnable wid => EnW wid
enableWids :: [EnableWid] -> IO ()
enableWids :: [EnableWid] -> IO ()
enableWids = (EnableWid -> IO ()) -> [EnableWid] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((EnableWid -> IO ()) -> [EnableWid] -> IO ())
-> (EnableWid -> IO ()) -> [EnableWid] -> IO ()
forall a b. (a -> b) -> a -> b
$ \ ew :: EnableWid
ew -> case EnableWid
ew of
EnW w :: wid
w -> Config wid
forall w. HasEnable w => Config w
enable wid
w IO wid -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
disableWids :: [EnableWid] -> IO ()
disableWids :: [EnableWid] -> IO ()
disableWids = (EnableWid -> IO ()) -> [EnableWid] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((EnableWid -> IO ()) -> [EnableWid] -> IO ())
-> (EnableWid -> IO ()) -> [EnableWid] -> IO ()
forall a b. (a -> b) -> a -> b
$ \ ew :: EnableWid
ew -> case EnableWid
ew of
EnW w :: wid
w -> Config wid
forall w. HasEnable w => Config w
disable wid
w IO wid -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
enableWidsUponSelection :: ListBox String -> [EnableWid] -> IO ()
enableWidsUponSelection :: ListBox String -> [EnableWid] -> IO ()
enableWidsUponSelection lb :: ListBox String
lb goalSpecificWids :: [EnableWid]
goalSpecificWids =
(ListBox String -> IO (Maybe [Int])
forall w i. HasSelectionBaseIndex w i => w -> IO (Maybe i)
getSelection ListBox String
lb :: IO (Maybe [Int])) IO (Maybe [Int]) -> (Maybe [Int] -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
IO () -> ([Int] -> IO ()) -> Maybe [Int] -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([EnableWid] -> IO ()
disableWids [EnableWid]
goalSpecificWids)
(IO () -> [Int] -> IO ()
forall a b. a -> b -> a
const (IO () -> [Int] -> IO ()) -> IO () -> [Int] -> IO ()
forall a b. (a -> b) -> a -> b
$ [EnableWid] -> IO ()
enableWids [EnableWid]
goalSpecificWids)