{- |
Module      :  ./GUI/GtkConsistencyChecker.hs
Description :  Gtk GUI for the consistency checker
Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  raider@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

This module provides a GUI for the consistency checker.
-}

module GUI.GtkConsistencyChecker where

import Graphics.UI.Gtk

import GUI.GtkUtils
import qualified GUI.Glade.NodeChecker as ConsistencyChecker
import GUI.GraphTypes

import Static.DevGraph
import Static.DgUtils
import Static.PrintDevGraph ()
import Static.GTheory
import Static.History

import Interfaces.GenericATPState (guiDefaultTimeLimit)

import Logic.Grothendieck
import Logic.Comorphism (AnyComorphism (..))

import Comorphisms.LogicGraph (logicGraph)

import Common.LibName (LibName)
import Common.Result

import Control.Concurrent (forkIO, killThread)
import Control.Concurrent.MVar
import Control.Monad (foldM_, join, when)

import Proofs.AbstractState
import Proofs.ConsistencyCheck

import Data.Graph.Inductive.Graph (LNode)
import qualified Data.Map as Map
import Data.List
import Data.Maybe

data Finder = Finder { Finder -> String
fName :: String
                     , Finder -> G_cons_checker
finder :: G_cons_checker
                     , Finder -> [AnyComorphism]
comorphism :: [AnyComorphism]
                     , Finder -> Int
selected :: Int }

instance Eq Finder where
  == :: Finder -> Finder -> Bool
(==) (Finder { fName :: Finder -> String
fName = String
n1, comorphism :: Finder -> [AnyComorphism]
comorphism = [AnyComorphism]
c1 })
       (Finder { fName :: Finder -> String
fName = String
n2, comorphism :: Finder -> [AnyComorphism]
comorphism = [AnyComorphism]
c2 }) = String
n1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
n2 Bool -> Bool -> Bool
&& [AnyComorphism]
c1 [AnyComorphism] -> [AnyComorphism] -> Bool
forall a. Eq a => a -> a -> Bool
== [AnyComorphism]
c2

data FNode = FNode { FNode -> String
name :: String
                   , FNode -> LNode DGNodeLab
node :: LNode DGNodeLab
                   , FNode -> G_sublogics
sublogic :: G_sublogics
                   , FNode -> ConsistencyStatus
cStatus :: ConsistencyStatus }

-- | Get a markup string containing name and color
instance Show FNode where
  show :: FNode -> String
show FNode { name :: FNode -> String
name = String
n, cStatus :: FNode -> ConsistencyStatus
cStatus = ConsistencyStatus
s } =
    "<span color=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ConsistencyStatus -> String
cStatusToColor ConsistencyStatus
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\">" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ConsistencyStatus -> String
cStatusToPrefix ConsistencyStatus
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++
    "</span>"

instance Eq FNode where
  == :: FNode -> FNode -> Bool
(==) f1 :: FNode
f1 f2 :: FNode
f2 = FNode -> FNode -> Ordering
forall a. Ord a => a -> a -> Ordering
compare FNode
f1 FNode
f2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord FNode where
  compare :: FNode -> FNode -> Ordering
compare (FNode { name :: FNode -> String
name = String
n1, cStatus :: FNode -> ConsistencyStatus
cStatus = ConsistencyStatus
s1 })
          (FNode { name :: FNode -> String
name = String
n2, cStatus :: FNode -> ConsistencyStatus
cStatus = ConsistencyStatus
s2 }) = case ConsistencyStatus -> ConsistencyStatus -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ConsistencyStatus
s1 ConsistencyStatus
s2 of
    EQ -> String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare String
n1 String
n2
    c :: Ordering
c -> Ordering
c

-- | Displays the consistency checker window
showConsistencyChecker :: Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyChecker :: Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyChecker mn :: Maybe Int
mn gi :: GInfo
gi@(GInfo { libName :: GInfo -> LibName
libName = LibName
ln }) le :: LibEnv
le =
  case Maybe Int
mn of
    Nothing -> Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyCheckerMain Maybe Int
mn GInfo
gi LibEnv
le
    Just n :: Int
n -> let
      dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
      lbl :: DGNodeLab
lbl = DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
n
      in if case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl of
        Just (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) -> ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
sens
        Nothing -> Bool
True
        then do
          String -> String -> IO ()
infoDialogExt "No sentences" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Node " String -> ShowS
forall a. [a] -> [a] -> [a]
++
            DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ " has no sentences and is thus trivially consistent"
          Result LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result LibEnv -> IO (Result LibEnv))
-> Result LibEnv -> IO (Result LibEnv)
forall a b. (a -> b) -> a -> b
$ LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return LibEnv
le
        else Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyCheckerMain Maybe Int
mn GInfo
gi LibEnv
le

-- | Displays the consistency checker window
showConsistencyCheckerMain :: Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyCheckerMain :: Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)
showConsistencyCheckerMain mn :: Maybe Int
mn (GInfo { libName :: GInfo -> LibName
libName = LibName
ln }) le :: LibEnv
le = do
  MVar LibEnv
wait <- IO (MVar LibEnv)
forall a. IO (MVar a)
newEmptyMVar
  MVar LibEnv -> Maybe Int -> LibName -> LibEnv -> IO ()
showConsistencyCheckerAux MVar LibEnv
wait Maybe Int
mn LibName
ln LibEnv
le
  LibEnv
le' <- MVar LibEnv -> IO LibEnv
forall a. MVar a -> IO a
takeMVar MVar LibEnv
wait
  Result LibEnv -> IO (Result LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result LibEnv -> IO (Result LibEnv))
-> Result LibEnv -> IO (Result LibEnv)
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe LibEnv -> Result LibEnv
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe LibEnv -> Result LibEnv) -> Maybe LibEnv -> Result LibEnv
forall a b. (a -> b) -> a -> b
$ LibEnv -> Maybe LibEnv
forall a. a -> Maybe a
Just LibEnv
le'

-- | Displays the consistency checker window
showConsistencyCheckerAux
  :: MVar LibEnv -> Maybe Int -> LibName -> LibEnv -> IO ()
showConsistencyCheckerAux :: MVar LibEnv -> Maybe Int -> LibName -> LibEnv -> IO ()
showConsistencyCheckerAux res :: MVar LibEnv
res mn :: Maybe Int
mn ln :: LibName
ln le :: LibEnv
le = IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  Builder
builder <- (String, String) -> IO Builder
getGTKBuilder (String, String)
ConsistencyChecker.get
  -- get objects
  Window
window <- Builder -> (GObject -> Window) -> String -> IO Window
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Window
forall obj. GObjectClass obj => obj -> Window
castToWindow "NodeChecker"
  Button
btnClose <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnClose"
  Button
btnResults <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnResults"
  -- get nodes view and buttons
  TreeView
trvNodes <- Builder -> (GObject -> TreeView) -> String -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvNodes"
  Button
btnNodesAll <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesAll"
  Button
btnNodesNone <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesNone"
  Button
btnNodesInvert <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesInvert"
  Button
btnNodesUnchecked <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesUnchecked"
  Button
btnNodesTimeout <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesTimeout"
  CheckButton
cbInclThms <- Builder -> (GObject -> CheckButton) -> String -> IO CheckButton
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> CheckButton
forall obj. GObjectClass obj => obj -> CheckButton
castToCheckButton "cbInclThms"
  -- get checker view and buttons
  ComboBox
cbComorphism <- Builder -> (GObject -> ComboBox) -> String -> IO ComboBox
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> ComboBox
forall obj. GObjectClass obj => obj -> ComboBox
castToComboBox "cbComorphism"
  Label
lblSublogic <- Builder -> (GObject -> Label) -> String -> IO Label
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Label
forall obj. GObjectClass obj => obj -> Label
castToLabel "lblSublogic"
  SpinButton
sbTimeout <- Builder -> (GObject -> SpinButton) -> String -> IO SpinButton
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> SpinButton
forall obj. GObjectClass obj => obj -> SpinButton
castToSpinButton "sbTimeout"
  Button
btnCheck <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnCheck"
  Button
btnStop <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnStop"
  TreeView
trvFinder <- Builder -> (GObject -> TreeView) -> String -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvFinder"

  Window -> String -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window "Consistency Checker"
  SpinButton -> Double -> IO ()
forall self. SpinButtonClass self => self -> Double -> IO ()
spinButtonSetValue SpinButton
sbTimeout (Double -> IO ()) -> Double -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
guiDefaultTimeLimit

  let widgets :: [Widget]
widgets = [ SpinButton -> Widget
forall o. WidgetClass o => o -> Widget
toWidget SpinButton
sbTimeout
                , ComboBox -> Widget
forall o. WidgetClass o => o -> Widget
toWidget ComboBox
cbComorphism
                , Label -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Label
lblSublogic ]
      checkWidgets :: [Widget]
checkWidgets = [Widget]
widgets [Widget] -> [Widget] -> [Widget]
forall a. [a] -> [a] -> [a]
++ [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnClose
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesAll
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesNone
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesInvert
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesUnchecked
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesTimeout
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnResults ]
      switch :: Bool -> IO ()
switch b :: Bool
b = do
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
b

  Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop Bool
False
  Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
False

  MVar ThreadId
threadId <- IO (MVar ThreadId)
forall a. IO (MVar a)
newEmptyMVar
  MVar ()
wait <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
  MVar (IO ())
mView <- IO (MVar (IO ()))
forall a. IO (MVar a)
newEmptyMVar

  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
      nodes :: [LNode DGNodeLab]
nodes = DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg
      selNodes :: [FNode] -> ([FNode], [FNode])
selNodes = (FNode -> Bool) -> [FNode] -> ([FNode], [FNode])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ (FNode { node :: FNode -> LNode DGNodeLab
node = (_, l :: DGNodeLab
l)}) -> case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
l of
        Just (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) -> ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
sens
        Nothing -> Bool
True)
      sls :: [G_sublogics]
sls = (G_theory -> G_sublogics) -> [G_theory] -> [G_sublogics]
forall a b. (a -> b) -> [a] -> [b]
map G_theory -> G_sublogics
sublogicOfTh ([G_theory] -> [G_sublogics]) -> [G_theory] -> [G_sublogics]
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> Maybe G_theory)
-> [LNode DGNodeLab] -> [G_theory]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (LNode DGNodeLab -> DGNodeLab)
-> LNode DGNodeLab
-> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd) [LNode DGNodeLab]
nodes
      (emptyNodes :: [FNode]
emptyNodes, others :: [FNode]
others) = [FNode] -> ([FNode], [FNode])
selNodes
        ([FNode] -> ([FNode], [FNode])) -> [FNode] -> ([FNode], [FNode])
forall a b. (a -> b) -> a -> b
$ ((LNode DGNodeLab, G_sublogics) -> FNode)
-> [(LNode DGNodeLab, G_sublogics)] -> [FNode]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: LNode DGNodeLab
n@(_, l :: DGNodeLab
l), s :: G_sublogics
s) -> String
-> LNode DGNodeLab -> G_sublogics -> ConsistencyStatus -> FNode
FNode (DGNodeLab -> String
getDGNodeName DGNodeLab
l) LNode DGNodeLab
n G_sublogics
s
               (ConsistencyStatus -> FNode) -> ConsistencyStatus -> FNode
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> ConsistencyStatus
getConsistencyOf DGNodeLab
l)
        ([(LNode DGNodeLab, G_sublogics)] -> [FNode])
-> [(LNode DGNodeLab, G_sublogics)] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab]
-> [G_sublogics] -> [(LNode DGNodeLab, G_sublogics)]
forall a b. [a] -> [b] -> [(a, b)]
zip [LNode DGNodeLab]
nodes [G_sublogics]
sls

  -- setup data
  ListStore FNode
listNodes <- TreeView -> (FNode -> String) -> [FNode] -> IO (ListStore FNode)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvNodes FNode -> String
forall a. Show a => a -> String
show ([FNode] -> IO (ListStore FNode))
-> [FNode] -> IO (ListStore FNode)
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort [FNode]
others
  ListStore Finder
listFinder <- TreeView -> (Finder -> String) -> [Finder] -> IO (ListStore Finder)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvFinder Finder -> String
fName []

  -- setup comorphism combobox
  ComboBox -> IO (ListStore ComboBoxText)
forall self.
ComboBoxClass self =>
self -> IO (ListStore ComboBoxText)
comboBoxSetModelText ComboBox
cbComorphism
  ConnectId ComboBox
shC <- ComboBox
-> Signal ComboBox (IO ()) -> IO () -> IO (ConnectId ComboBox)
forall object callback.
object
-> Signal object callback -> callback -> IO (ConnectId object)
after ComboBox
cbComorphism Signal ComboBox (IO ())
forall self. ComboBoxClass self => Signal self (IO ())
changed
    (IO () -> IO (ConnectId ComboBox))
-> IO () -> IO (ConnectId ComboBox)
forall a b. (a -> b) -> a -> b
$ TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism TreeView
trvFinder ListStore Finder
listFinder ComboBox
cbComorphism

  -- setup view selection actions
  let update :: IO ()
update = do
        Maybe (Int, Finder)
mf <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
        TreeView
-> ListStore Finder -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism TreeView
trvFinder ListStore Finder
listFinder ComboBox
cbComorphism ConnectId ComboBox
shC
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe (Int, Finder) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Int, Finder)
mf
  TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvFinder IO ()
update

  let upd :: IO ()
upd = TreeView
-> ListStore FNode
-> (Bool -> G_sublogics -> IO ())
-> IO ()
-> IO ()
-> IO ()
updateNodes TreeView
trvNodes ListStore FNode
listNodes
        (\ b :: Bool
b s :: G_sublogics
s -> do
           Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblSublogic (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
s
           TreeView -> ListStore Finder -> Bool -> G_sublogics -> IO ()
updateFinder TreeView
trvFinder ListStore Finder
listFinder Bool
b G_sublogics
s)
        (do
          Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblSublogic "No sublogic"
          ListStore Finder -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore Finder
listFinder
          [Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
False
          Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
False)
        ([Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
True IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
True)

  ConnectId TreeSelection
shN <- TreeView
-> Button
-> Button
-> Button
-> IO ()
-> IO (ConnectId TreeSelection)
setListSelectorMultiple TreeView
trvNodes Button
btnNodesAll Button
btnNodesNone
    Button
btnNodesInvert IO ()
upd

  -- bindings
  let selectWithAux :: (FNode -> Bool) -> IO b -> IO b
selectWithAux f :: FNode -> Bool
f u :: IO b
u = do
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shN
        TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvNodes
        TreeSelection -> IO ()
forall self. TreeSelectionClass self => self -> IO ()
treeSelectionSelectAll TreeSelection
sel
        [TreePath]
rs <- TreeSelection -> IO [TreePath]
forall self. TreeSelectionClass self => self -> IO [TreePath]
treeSelectionGetSelectedRows TreeSelection
sel
        (TreePath -> IO ()) -> [TreePath] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ ~p :: TreePath
p@(row :: Int
row : []) -> do
          FNode
fn <- ListStore FNode -> Int -> IO FNode
forall a. ListStore a -> Int -> IO a
listStoreGetValue ListStore FNode
listNodes Int
row
          (if FNode -> Bool
f FNode
fn then TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath else TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionUnselectPath)
            TreeSelection
sel TreePath
p) [TreePath]
rs
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shN
        IO b
u
      selectWith :: (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith f :: ConsistencyStatus -> Bool
f = (FNode -> Bool) -> IO b -> IO b
forall b. (FNode -> Bool) -> IO b -> IO b
selectWithAux ((FNode -> Bool) -> IO b -> IO b)
-> (FNode -> Bool) -> IO b -> IO b
forall a b. (a -> b) -> a -> b
$ ConsistencyStatus -> Bool
f (ConsistencyStatus -> Bool)
-> (FNode -> ConsistencyStatus) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> ConsistencyStatus
cStatus

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnNodesUnchecked
    (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ (ConsistencyStatus -> Bool) -> IO () -> IO ()
forall b. (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith (ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked "") IO ()
upd
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnNodesTimeout (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ (ConsistencyStatus -> Bool) -> IO () -> IO ()
forall b. (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith (ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSTimeout "") IO ()
upd

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnResults (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView MVar (IO ())
mView "Models" ListStore FNode
listNodes [FNode]
emptyNodes
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnClose (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnStop (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar ThreadId -> IO ThreadId
forall a. MVar a -> IO a
takeMVar MVar ThreadId
threadId IO ThreadId -> (ThreadId -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ThreadId -> IO ()
killThread IO () -> (() -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnCheck (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
    [Widget] -> Bool -> IO ()
activate [Widget]
checkWidgets Bool
False
    Int
timeout <- SpinButton -> IO Int
forall self. SpinButtonClass self => self -> IO Int
spinButtonGetValueAsInt SpinButton
sbTimeout
    Bool
inclThms <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbInclThms
    (updat :: Double -> String -> IO ()
updat, pexit :: IO ()
pexit) <- String -> String -> IO (Double -> String -> IO (), IO ())
progressBar "Checking consistency" "please wait..."
    [(Int, FNode)]
nodes' <- TreeView -> ListStore FNode -> IO [(Int, FNode)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
trvNodes ListStore FNode
listNodes
    Maybe (Int, Finder)
mf <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
    Finder
f <- case Maybe (Int, Finder)
mf of
      Nothing -> String -> IO Finder
forall a. HasCallStack => String -> a
error "Consistency checker: internal error"
      Just (_, f :: Finder
f) -> Finder -> IO Finder
forall (m :: * -> *) a. Monad m => a -> m a
return Finder
f
    Bool -> IO ()
switch Bool
False
    ThreadId
tid <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ do
      Bool
-> Bool
-> LibName
-> LibEnv
-> DGraph
-> Finder
-> Int
-> ListStore FNode
-> (Double -> String -> IO ())
-> [(Int, FNode)]
-> IO ()
check Bool
False Bool
inclThms LibName
ln LibEnv
le DGraph
dg Finder
f Int
timeout ListStore FNode
listNodes Double -> String -> IO ()
updat [(Int, FNode)]
nodes'
      MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait ()
    MVar ThreadId -> ThreadId -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ThreadId
threadId ThreadId
tid
    IO () -> IO ()
forkIO_ (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
wait
      IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Bool -> IO ()
switch Bool
True
        MVar ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar ThreadId
threadId
        MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView MVar (IO ())
mView "Results of consistency check" ListStore FNode
listNodes [FNode]
emptyNodes
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shN
        TreeView -> ListStore FNode -> IO ()
sortNodes TreeView
trvNodes ListStore FNode
listNodes
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shN
        IO ()
upd
        [Widget] -> Bool -> IO ()
activate [Widget]
checkWidgets Bool
True
        IO ()
pexit

  Window -> IO () -> IO (ConnectId Window)
forall w. WidgetClass w => w -> IO () -> IO (ConnectId w)
onDestroy Window
window (IO () -> IO (ConnectId Window)) -> IO () -> IO (ConnectId Window)
forall a b. (a -> b) -> a -> b
$ do
    [FNode]
nodes' <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
listNodes
    let changes :: [DGChange]
changes = ([DGChange] -> FNode -> [DGChange])
-> [DGChange] -> [FNode] -> [DGChange]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ cs :: [DGChange]
cs (FNode { node :: FNode -> LNode DGNodeLab
node = (i :: Int
i, l :: DGNodeLab
l), cStatus :: FNode -> ConsistencyStatus
cStatus = ConsistencyStatus
s }) ->
                      if (\ st :: SType
st -> SType
st SType -> SType -> Bool
forall a. Eq a => a -> a -> Bool
/= SType
CSConsistent Bool -> Bool -> Bool
&& SType
st SType -> SType -> Bool
forall a. Eq a => a -> a -> Bool
/= SType
CSInconsistent)
                         (SType -> Bool) -> SType -> Bool
forall a b. (a -> b) -> a -> b
$ ConsistencyStatus -> SType
sType ConsistencyStatus
s then [DGChange]
cs
                        else
                          let n :: LNode DGNodeLab
n = (Int
i, if ConsistencyStatus -> SType
sType ConsistencyStatus
s SType -> SType -> Bool
forall a. Eq a => a -> a -> Bool
== SType
CSInconsistent then
                                        String -> DGNodeLab -> DGNodeLab
markNodeInconsistent "" DGNodeLab
l
                                        else String -> DGNodeLab -> DGNodeLab
markNodeConsistent "" DGNodeLab
l)
                          in DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
l LNode DGNodeLab
n DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
cs
                    ) [] [FNode]
nodes'
        dg' :: DGraph
dg' = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
    MVar LibEnv -> LibEnv -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar LibEnv
res (LibEnv -> IO ()) -> LibEnv -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "Consistency") DGraph
dg') LibEnv
le

  (FNode -> Bool) -> IO () -> IO ()
forall b. (FNode -> Bool) -> IO b -> IO b
selectWithAux ((FNode -> Bool)
-> (Int -> FNode -> Bool) -> Maybe Int -> FNode -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked "") (ConsistencyStatus -> Bool)
-> (FNode -> ConsistencyStatus) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> ConsistencyStatus
cStatus)
          (\ n :: Int
n -> (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) (Int -> Bool) -> (FNode -> Int) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> Int
forall a b. (a, b) -> a
fst (LNode DGNodeLab -> Int)
-> (FNode -> LNode DGNodeLab) -> FNode -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> LNode DGNodeLab
node) Maybe Int
mn) IO ()
upd
  Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window

sortNodes :: TreeView -> ListStore FNode -> IO ()
sortNodes :: TreeView -> ListStore FNode -> IO ()
sortNodes trvNodes :: TreeView
trvNodes listNodes :: ListStore FNode
listNodes = do
  [(Int, FNode)]
sel <- TreeView -> ListStore FNode -> IO [(Int, FNode)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
trvNodes ListStore FNode
listNodes
  [FNode]
nodes <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
listNodes
  let sn :: [FNode]
sn = [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort [FNode]
nodes
  ListStore FNode -> [FNode] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore FNode
listNodes [FNode]
sn
  TreeSelection
selector <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvNodes
  ((Int, FNode) -> IO ()) -> [(Int, FNode)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (_, FNode { name :: FNode -> String
name = String
n }) -> TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
selector
      [Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error "Node not found!") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ (FNode -> Bool) -> [FNode] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (FNode -> String) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> String
name) [FNode]
sn]
    ) [(Int, FNode)]
sel

-- | Called when node selection is changed. Updates finder list
updateNodes :: TreeView -> ListStore FNode -> (Bool -> G_sublogics -> IO ())
            -> IO () -> IO () -> IO ()
updateNodes :: TreeView
-> ListStore FNode
-> (Bool -> G_sublogics -> IO ())
-> IO ()
-> IO ()
-> IO ()
updateNodes view :: TreeView
view listNodes :: ListStore FNode
listNodes update :: Bool -> G_sublogics -> IO ()
update lock :: IO ()
lock unlock :: IO ()
unlock = do
  [(Int, FNode)]
nodes <- TreeView -> ListStore FNode -> IO [(Int, FNode)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
view ListStore FNode
listNodes
  if [(Int, FNode)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, FNode)]
nodes then IO ()
lock
    else let sls :: [G_sublogics]
sls = ((Int, FNode) -> G_sublogics) -> [(Int, FNode)] -> [G_sublogics]
forall a b. (a -> b) -> [a] -> [b]
map (FNode -> G_sublogics
sublogic (FNode -> G_sublogics)
-> ((Int, FNode) -> FNode) -> (Int, FNode) -> G_sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, FNode) -> FNode
forall a b. (a, b) -> b
snd) [(Int, FNode)]
nodes in
      IO () -> (G_sublogics -> IO ()) -> Maybe G_sublogics -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
lock (\ sl :: G_sublogics
sl -> IO ()
unlock IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> G_sublogics -> IO ()
update ([(Int, FNode)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, FNode)]
nodes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1) G_sublogics
sl)
            (Maybe G_sublogics -> IO ()) -> Maybe G_sublogics -> IO ()
forall a b. (a -> b) -> a -> b
$ (Maybe G_sublogics -> G_sublogics -> Maybe G_sublogics)
-> Maybe G_sublogics -> [G_sublogics] -> Maybe G_sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ ma :: Maybe G_sublogics
ma b :: G_sublogics
b -> case Maybe G_sublogics
ma of
                      Just a :: G_sublogics
a -> G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics G_sublogics
b G_sublogics
a
                      Nothing -> Maybe G_sublogics
forall a. Maybe a
Nothing) (G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just (G_sublogics -> Maybe G_sublogics)
-> G_sublogics -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ [G_sublogics] -> G_sublogics
forall a. [a] -> a
head [G_sublogics]
sls) ([G_sublogics] -> Maybe G_sublogics)
-> [G_sublogics] -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ [G_sublogics] -> [G_sublogics]
forall a. [a] -> [a]
tail [G_sublogics]
sls

-- | Update the list of finder
updateFinder :: TreeView -> ListStore Finder -> Bool -> G_sublogics -> IO ()
updateFinder :: TreeView -> ListStore Finder -> Bool -> G_sublogics -> IO ()
updateFinder view :: TreeView
view list :: ListStore Finder
list useNonBatch :: Bool
useNonBatch sl :: G_sublogics
sl = do
  [Finder]
old <- ListStore Finder -> IO [Finder]
forall a. ListStore a -> IO [a]
listStoreToList ListStore Finder
list
  [(G_cons_checker, AnyComorphism)]
cs <- [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers ([AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths LogicGraph
logicGraph G_sublogics
sl
  let new :: [Finder]
new = Map String Finder -> [Finder]
forall k a. Map k a -> [a]
Map.elems (Map String Finder -> [Finder]) -> Map String Finder -> [Finder]
forall a b. (a -> b) -> a -> b
$ ((G_cons_checker, AnyComorphism)
 -> Map String Finder -> Map String Finder)
-> Map String Finder
-> [(G_cons_checker, AnyComorphism)]
-> Map String Finder
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (cc :: G_cons_checker
cc, c :: AnyComorphism
c) m :: Map String Finder
m ->
              let n :: String
n = G_cons_checker -> String
getCcName G_cons_checker
cc
                  f :: Finder
f = Finder -> String -> Map String Finder -> Finder
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> G_cons_checker -> [AnyComorphism] -> Int -> Finder
Finder String
n G_cons_checker
cc [] 0) String
n Map String Finder
m
              in String -> Finder -> Map String Finder -> Map String Finder
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
n (Finder
f { comorphism :: [AnyComorphism]
comorphism = AnyComorphism
c AnyComorphism -> [AnyComorphism] -> [AnyComorphism]
forall a. a -> [a] -> [a]
: Finder -> [AnyComorphism]
comorphism Finder
f}) Map String Finder
m) Map String Finder
forall k a. Map k a
Map.empty
              ([(G_cons_checker, AnyComorphism)] -> Map String Finder)
-> [(G_cons_checker, AnyComorphism)] -> Map String Finder
forall a b. (a -> b) -> a -> b
$ (if Bool
useNonBatch then [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a. a -> a
id else ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter (G_cons_checker -> Bool
getCcBatch (G_cons_checker -> Bool)
-> ((G_cons_checker, AnyComorphism) -> G_cons_checker)
-> (G_cons_checker, AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_cons_checker, AnyComorphism) -> G_cons_checker
forall a b. (a, b) -> a
fst))
              [(G_cons_checker, AnyComorphism)]
cs
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Finder]
old [Finder] -> [Finder] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Finder]
new) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    -- update list and try to select previous finder
    Maybe (Int, Finder)
selected' <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore Finder
list
    TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
view
    ListStore Finder -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore Finder
list
    (Finder -> IO Int) -> [Finder] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ListStore Finder -> Finder -> IO Int
forall a. ListStore a -> a -> IO Int
listStoreAppend ListStore Finder
list) ([Finder] -> IO ()) -> [Finder] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Finder] -> [Finder] -> [Finder]
mergeFinder [Finder]
old [Finder]
new
    IO () -> ((Int, Finder) -> IO ()) -> Maybe (Int, Finder) -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TreeView -> IO ()
selectFirst TreeView
view)
      (\ (_, f :: Finder
f) -> let i :: Maybe Int
i = (Finder -> Bool) -> [Finder] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((Finder -> String
fName Finder
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (Finder -> String) -> Finder -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finder -> String
fName) [Finder]
new in
        IO () -> (Int -> IO ()) -> Maybe Int -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TreeView -> IO ()
selectFirst TreeView
view) (TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
sel (TreePath -> IO ()) -> (Int -> TreePath) -> Int -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> TreePath -> TreePath
forall a. a -> [a] -> [a]
: [])) Maybe Int
i
      ) Maybe (Int, Finder)
selected'

-- | Try to select previous selected comorphism if possible
mergeFinder :: [Finder] -> [Finder] -> [Finder]
mergeFinder :: [Finder] -> [Finder] -> [Finder]
mergeFinder old :: [Finder]
old new :: [Finder]
new = let m' :: Map String Finder
m' = [(String, Finder)] -> Map String Finder
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, Finder)] -> Map String Finder)
-> [(String, Finder)] -> Map String Finder
forall a b. (a -> b) -> a -> b
$ (Finder -> (String, Finder)) -> [Finder] -> [(String, Finder)]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: Finder
f -> (Finder -> String
fName Finder
f, Finder
f)) [Finder]
new in
  Map String Finder -> [Finder]
forall k a. Map k a -> [a]
Map.elems (Map String Finder -> [Finder]) -> Map String Finder -> [Finder]
forall a b. (a -> b) -> a -> b
$ (Map String Finder -> Finder -> Map String Finder)
-> Map String Finder -> [Finder] -> Map String Finder
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map String Finder
m (Finder { fName :: Finder -> String
fName = String
n, comorphism :: Finder -> [AnyComorphism]
comorphism = [AnyComorphism]
cc, selected :: Finder -> Int
selected = Int
i}) ->
      case String -> Map String Finder -> Maybe Finder
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
n Map String Finder
m of
        Nothing -> Map String Finder
m
        Just f :: Finder
f@(Finder { comorphism :: Finder -> [AnyComorphism]
comorphism = [AnyComorphism]
cc' }) -> let c :: AnyComorphism
c = [AnyComorphism]
cc [AnyComorphism] -> Int -> AnyComorphism
forall a. [a] -> Int -> a
!! Int
i in
          String -> Finder -> Map String Finder -> Map String Finder
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
n (Finder
f { selected :: Int
selected = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> [AnyComorphism] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex AnyComorphism
c [AnyComorphism]
cc' }) Map String Finder
m
    ) Map String Finder
m' [Finder]
old

check :: Bool -> Bool -> LibName -> LibEnv -> DGraph -> Finder -> Int
      -> ListStore FNode -> (Double -> String -> IO ()) -> [(Int, FNode)]
      -> IO ()
check :: Bool
-> Bool
-> LibName
-> LibEnv
-> DGraph
-> Finder
-> Int
-> ListStore FNode
-> (Double -> String -> IO ())
-> [(Int, FNode)]
-> IO ()
check dispr :: Bool
dispr inclThms :: Bool
inclThms ln :: LibName
ln le :: LibEnv
le dg :: DGraph
dg (Finder _ cc :: G_cons_checker
cc cs :: [AnyComorphism]
cs i :: Int
i) timeout :: Int
timeout listNodes :: ListStore FNode
listNodes update :: Double -> String -> IO ()
update
  nodes :: [(Int, FNode)]
nodes = let
    count' :: Double
count' = Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Double) -> Int -> Double
forall a b. (a -> b) -> a -> b
$ [(Int, FNode)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, FNode)]
nodes
    c :: AnyComorphism
c = [AnyComorphism]
cs [AnyComorphism] -> Int -> AnyComorphism
forall a. [a] -> Int -> a
!! Int
i in
  (Double -> (Int, FNode) -> IO Double)
-> Double -> [(Int, FNode)] -> IO ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (\ count :: Double
count (row :: Int
row, fn :: FNode
fn@(FNode { name :: FNode -> String
name = String
n', node :: FNode -> LNode DGNodeLab
node = LNode DGNodeLab
n })) -> do
           IO () -> IO ()
forall a. IO a -> IO a
postGUISync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Double -> String -> IO ()
update (Double
count Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
count') String
n'
           ConsistencyStatus
res <- Bool
-> G_cons_checker
-> AnyComorphism
-> LibName
-> LibEnv
-> DGraph
-> LNode DGNodeLab
-> Int
-> IO ConsistencyStatus
consistencyCheck Bool
inclThms G_cons_checker
cc AnyComorphism
c LibName
ln LibEnv
le DGraph
dg LNode DGNodeLab
n Int
timeout
           let res' :: ConsistencyStatus
res' = if Bool
dispr then ConsistencyStatus -> ConsistencyStatus
cInvert ConsistencyStatus
res else ConsistencyStatus
res
           IO () -> IO ()
forall a. IO a -> IO a
postGUISync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ListStore FNode -> Int -> FNode -> IO ()
forall a. ListStore a -> Int -> a -> IO ()
listStoreSetValue ListStore FNode
listNodes Int
row FNode
fn { cStatus :: ConsistencyStatus
cStatus = ConsistencyStatus
res' }
           Double -> IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> IO Double) -> Double -> IO Double
forall a b. (a -> b) -> a -> b
$ Double
count Double -> Double -> Double
forall a. Num a => a -> a -> a
+ 1) 0 [(Int, FNode)]
nodes

updateComorphism :: TreeView -> ListStore Finder -> ComboBox
                 -> ConnectId ComboBox -> IO ()
updateComorphism :: TreeView
-> ListStore Finder -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism view :: TreeView
view list :: ListStore Finder
list cbComorphism :: ComboBox
cbComorphism sh :: ConnectId ComboBox
sh = do
  ConnectId ComboBox -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId ComboBox
sh
  ListStore ComboBoxText
model <- ComboBox -> IO (ListStore ComboBoxText)
forall self.
ComboBoxClass self =>
self -> IO (ListStore ComboBoxText)
comboBoxGetModelText ComboBox
cbComorphism
  ListStore ComboBoxText -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore ComboBoxText
model
  Maybe (Int, Finder)
mfinder <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore Finder
list
  case Maybe (Int, Finder)
mfinder of
    Just (_, f :: Finder
f) -> do
      (ComboBoxText -> IO Int) -> [ComboBoxText] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ComboBox -> ComboBoxText -> IO Int
forall self. ComboBoxClass self => self -> ComboBoxText -> IO Int
comboBoxAppendText ComboBox
cbComorphism) ([ComboBoxText] -> IO ()) -> [ComboBoxText] -> IO ()
forall a b. (a -> b) -> a -> b
$ Finder -> [ComboBoxText]
expand Finder
f
      ComboBox -> Int -> IO ()
forall self. ComboBoxClass self => self -> Int -> IO ()
comboBoxSetActive ComboBox
cbComorphism (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$ Finder -> Int
selected Finder
f
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  ConnectId ComboBox -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId ComboBox
sh

expand :: Finder -> [ComboBoxText]
expand :: Finder -> [ComboBoxText]
expand = [AnyComorphism] -> [ComboBoxText]
forall a. Show a => [a] -> [ComboBoxText]
toComboBoxText ([AnyComorphism] -> [ComboBoxText])
-> (Finder -> [AnyComorphism]) -> Finder -> [ComboBoxText]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finder -> [AnyComorphism]
comorphism

setSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism view :: TreeView
view list :: ListStore Finder
list cbComorphism :: ComboBox
cbComorphism = do
  Maybe (Int, Finder)
mfinder <- TreeView -> ListStore Finder -> IO (Maybe (Int, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore Finder
list
  case Maybe (Int, Finder)
mfinder of
    Just (i :: Int
i, f :: Finder
f) -> do
      Int
sel <- ComboBox -> IO Int
forall self. ComboBoxClass self => self -> IO Int
comboBoxGetActive ComboBox
cbComorphism
      ListStore Finder -> Int -> Finder -> IO ()
forall a. ListStore a -> Int -> a -> IO ()
listStoreSetValue ListStore Finder
list Int
i Finder
f { selected :: Int
selected = Int
sel }
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Displays the model view window
showModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> [FNode]
                 -> IO ()
showModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelViewAux lock :: MVar (IO ())
lock title :: String
title list :: ListStore FNode
list other :: [FNode]
other = do
  Builder
builder <- (String, String) -> IO Builder
getGTKBuilder (String, String)
ConsistencyChecker.get
  -- get objects
  Window
window <- Builder -> (GObject -> Window) -> String -> IO Window
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Window
forall obj. GObjectClass obj => obj -> Window
castToWindow "ModelView"
  Button
btnClose <- Builder -> (GObject -> Button) -> String -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnResClose"
  Frame
frNodes <- Builder -> (GObject -> Frame) -> String -> IO Frame
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Frame
forall obj. GObjectClass obj => obj -> Frame
castToFrame "frResNodes"
  TreeView
trvNodes <- Builder -> (GObject -> TreeView) -> String -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvResNodes"
  TextView
tvModel <- Builder -> (GObject -> TextView) -> String -> IO TextView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TextView
forall obj. GObjectClass obj => obj -> TextView
castToTextView "tvResModel"

  Window -> String -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window String
title

  -- setup text view
  TextBuffer
buffer <- TextView -> IO TextBuffer
forall self. TextViewClass self => self -> IO TextBuffer
textViewGetBuffer TextView
tvModel
  TextBuffer -> String -> IO ()
forall self string.
(TextBufferClass self, GlibString string) =>
self -> string -> IO ()
textBufferInsertAtCursor TextBuffer
buffer ""

  TextTagTable
tagTable <- TextBuffer -> IO TextTagTable
forall self. TextBufferClass self => self -> IO TextTagTable
textBufferGetTagTable TextBuffer
buffer
  TextTag
font <- Maybe ComboBoxText -> IO TextTag
textTagNew Maybe ComboBoxText
forall a. Maybe a
Nothing
  TextTag -> [AttrOp TextTag] -> IO ()
forall o. o -> [AttrOp o] -> IO ()
set TextTag
font [ Attr TextTag String
forall self string.
(TextTagClass self, GlibString string) =>
Attr self string
textTagFont Attr TextTag String -> String -> AttrOp TextTag
forall o a b. ReadWriteAttr o a b -> b -> AttrOp o
:= "FreeMono" ]
  TextTagTable -> TextTag -> IO ()
forall self tag.
(TextTagTableClass self, TextTagClass tag) =>
self -> tag -> IO ()
textTagTableAdd TextTagTable
tagTable TextTag
font
  TextIter
start <- TextBuffer -> IO TextIter
forall self. TextBufferClass self => self -> IO TextIter
textBufferGetStartIter TextBuffer
buffer
  TextIter
end <- TextBuffer -> IO TextIter
forall self. TextBufferClass self => self -> IO TextIter
textBufferGetEndIter TextBuffer
buffer
  TextBuffer -> TextTag -> TextIter -> TextIter -> IO ()
forall self tag.
(TextBufferClass self, TextTagClass tag) =>
self -> tag -> TextIter -> TextIter -> IO ()
textBufferApplyTag TextBuffer
buffer TextTag
font TextIter
start TextIter
end

  -- setup list view
  let filterNodes :: [FNode] -> [FNode]
filterNodes = (FNode -> Bool) -> [FNode] -> [FNode]
forall a. (a -> Bool) -> [a] -> [a]
filter ((ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
/= SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked "") (ConsistencyStatus -> Bool)
-> (FNode -> ConsistencyStatus) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> ConsistencyStatus
cStatus)

  [FNode]
nodes <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
list
  ListStore FNode
listNodes <- TreeView -> (FNode -> String) -> [FNode] -> IO (ListStore FNode)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvNodes FNode -> String
forall a. Show a => a -> String
show ([FNode] -> IO (ListStore FNode))
-> [FNode] -> IO (ListStore FNode)
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort ([FNode] -> [FNode]) -> [FNode] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
filterNodes ([FNode] -> [FNode]) -> [FNode] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [FNode]
other [FNode] -> [FNode] -> [FNode]
forall a. [a] -> [a] -> [a]
++ [FNode]
nodes

  TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvNodes (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ do
    Maybe (Int, FNode)
mn <- TreeView -> ListStore FNode -> IO (Maybe (Int, FNode))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvNodes ListStore FNode
listNodes
    case Maybe (Int, FNode)
mn of
      Nothing -> TextBuffer -> String -> IO ()
forall self string.
(TextBufferClass self, GlibString string) =>
self -> string -> IO ()
textBufferSetText TextBuffer
buffer ""
      Just (_, n :: FNode
n) -> TextBuffer -> String -> IO ()
forall self string.
(TextBufferClass self, GlibString string) =>
self -> string -> IO ()
textBufferSetText TextBuffer
buffer (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ ConsistencyStatus -> String
forall a. Show a => a -> String
show (ConsistencyStatus -> String) -> ConsistencyStatus -> String
forall a b. (a -> b) -> a -> b
$ FNode -> ConsistencyStatus
cStatus FNode
n

  -- setup actions
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnClose (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
  Window -> IO () -> IO (ConnectId Window)
forall w. WidgetClass w => w -> IO () -> IO (ConnectId w)
onDestroy Window
window (IO () -> IO (ConnectId Window)) -> IO () -> IO (ConnectId Window)
forall a b. (a -> b) -> a -> b
$ MVar (IO ()) -> IO (IO ())
forall a. MVar a -> IO a
takeMVar MVar (IO ())
lock IO (IO ()) -> (IO () -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO () -> IO () -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

  MVar (IO ()) -> IO () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (IO ())
lock (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Maybe (Int, FNode)
sel' <- TreeView -> ListStore FNode -> IO (Maybe (Int, FNode))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvNodes ListStore FNode
listNodes
    TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvNodes
    [FNode]
nodes'' <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
list
    let nodes' :: [FNode]
nodes' = [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort ([FNode] -> [FNode]) -> [FNode] -> [FNode]
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
filterNodes [FNode]
nodes''
    ListStore FNode -> [FNode] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore FNode
listNodes ([FNode] -> IO ()) -> [FNode] -> IO ()
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort ([FNode]
other [FNode] -> [FNode] -> [FNode]
forall a. [a] -> [a] -> [a]
++ [FNode]
nodes')
    IO () -> (Int -> IO ()) -> Maybe Int -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TreeView -> IO ()
selectFirst TreeView
trvNodes) (TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
sel (TreePath -> IO ()) -> (Int -> TreePath) -> Int -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> TreePath -> TreePath
forall a. a -> [a] -> [a]
: []))
      (Maybe Int -> IO ()) -> Maybe Int -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int
-> ((Int, FNode) -> Maybe Int) -> Maybe (Int, FNode) -> Maybe Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe Int
forall a. Maybe a
Nothing (\ (_, n :: FNode
n) -> (FNode -> Bool) -> [FNode] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((FNode -> String
name FNode
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (FNode -> String) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> String
name) [FNode]
nodes') Maybe (Int, FNode)
sel'

  TreeView -> IO ()
selectFirst TreeView
trvNodes

  Window -> Int -> Int -> IO ()
forall self. WidgetClass self => self -> Int -> Int -> IO ()
widgetSetSizeRequest Window
window 800 600
  Frame -> Int -> Int -> IO ()
forall self. WidgetClass self => self -> Int -> Int -> IO ()
widgetSetSizeRequest Frame
frNodes 250 (-1)

  Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window

-- | Displays the model view window
showModelView :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelView lock :: MVar (IO ())
lock title :: String
title list :: ListStore FNode
list other :: [FNode]
other = do
  Bool
isNotOpen <- MVar (IO ()) -> IO Bool
forall a. MVar a -> IO Bool
isEmptyMVar MVar (IO ())
lock
  if Bool
isNotOpen then MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
showModelViewAux MVar (IO ())
lock String
title ListStore FNode
list [FNode]
other
    else IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (MVar (IO ()) -> IO (IO ())
forall a. MVar a -> IO a
readMVar MVar (IO ())
lock)