Changeset 12779

Timestamp:

04.11.2009 03:14:21 (3 weeks ago)

Author:

raider

Message:

changed selection mode of list for gtk. removed old files. implemented gtk prover gui, is working now, but still has some bugs (interactive test 3 is not working). added some datatypes for prover windows to gtk utils.

Location:

trunk/GUI

Files:

• ConsistencyChecker.hs (deleted)
• Glade/ConsistencyChecker.glade (modified) (4 diffs)
• Glade/GenericATP.glade (modified) (2 diffs)
• Glade/ProverGUI.glade (modified) (2 diffs)
• GtkConsistencyChecker.hs (modified) (7 diffs)
• GtkGenericATP.hs (modified) (11 diffs)
• GtkProverGUI.hs (modified) (8 diffs)
• GtkTextView.hs (deleted)
• GtkUtils.hs (modified) (7 diffs)
• HTkGenericATP.hs (modified) (1 diff)

trunk/GUI/Glade/ConsistencyChecker.glade

@@ -277 +277 @@
                             <property name="label" translatable="yes">No sublogic</property>
                             <property name="use_markup">True</property>
+                            <property name="selectable">True</property>
+                            <property name="max_width_chars">30</property>
                           </widget>
                         </child>
@@ -293 +295 @@
                   </widget>
                   <packing>
+                    <property name="expand">False</property>
                     <property name="position">1</property>
                   </packing>
@@ -311 +314 @@
                             <property name="visible">True</property>
                             <property name="xalign">0</property>
+                            <property name="yalign">0</property>
                             <property name="label" translatable="yes">No path selected</property>
-                            <property name="wrap">True</property>
                             <property name="selectable">True</property>
                           </widget>
@@ -330 +333 @@
                   </widget>
                   <packing>
+                    <property name="expand">False</property>
                     <property name="position">2</property>
                   </packing>

trunk/GUI/Glade/GenericATP.glade

@@ -90 +90 @@
                                     <property name="can_focus">True</property>
                                     <property name="invisible_char">&#x25CF;</property>
-                                    <property name="adjustment">20 0 40 1 0 0</property>
+                                    <property name="adjustment">20 1 3600 1 0 0</property>
                                   </widget>
                                   <packing>
@@ -148 +148 @@
                                 <property name="can_focus">True</property>
                                 <property name="receives_default">False</property>
-                                <property name="active">True</property>
                                 <property name="draw_indicator">True</property>
                               </widget>

trunk/GUI/Glade/ProverGUI.glade

@@ -241 +241 @@
                             <property name="label" translatable="yes">No sublogic given</property>
                             <property name="use_markup">True</property>
+                            <property name="selectable">True</property>
                           </widget>
                         </child>
@@ -277 +278 @@
                             <property name="visible">True</property>
                             <property name="xalign">0</property>
+                            <property name="yalign">0</property>
                             <property name="label" translatable="yes">No path selected</property>
-                            <property name="wrap">True</property>
                             <property name="selectable">True</property>
                           </widget>

trunk/GUI/GtkConsistencyChecker.hs

@@ -51 +51 @@
 import Data.Maybe
 
-data Finder = Finder { fname :: String
+data Finder = Finder { fName :: String
                      , finder :: G_cons_checker
-                     , comorphs :: [AnyComorphism]
+                     , comorphism :: [AnyComorphism]
                      , selected :: Int }
 
@@ -125 +125 @@
   spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit
 
-  let widgets = [ toWidget trvFinder
-                , toWidget btnFineGrained
+  let widgets = [ toWidget btnFineGrained
                 , toWidget sbTimeout
                 , toWidget lblComorphism
-                , toWidget lblSublogic
-                ]
+                , toWidget lblSublogic ]
       checkWidgets = widgets ++ [ toWidget btnClose
-                                , toWidget trvNodes
                                 , toWidget btnNodesAll
                                 , toWidget btnNodesNone
@@ -138 +135 @@
                                 , toWidget btnNodesUnchecked
                                 , toWidget btnNodesTimeout
-                                , toWidget btnResults
-                                ]
+                                , toWidget btnResults ]
       switch b = do
         widgetSetSensitive btnStop $ not b
@@ -167 +163 @@
     $ map (\ (n@(_,l),s) -> FNode (getDGNodeName l) n s CSUnchecked)
     $ zip nodes sls
-  listFinder <- setListData trvFinder fname []
+  listFinder <- setListData trvFinder fName []
 
   -- setup view selection actions
-  let update = do mf <- getSelectedSingle trvFinder listFinder
-                  case mf of
-                    Just (_,f) -> do
-                      case comorphs f !! selected f of
-                        Comorphism cid ->
-                          let cName = language_name cid
-                              dName = drop 1 $ dropWhile (/= ';') cName
-                          in labelSetLabel lblComorphism
-                            $ if null dName then "identity" else dName
-                      widgetSetSensitive btnCheck True
-                    Nothing -> do
-                      labelSetLabel lblComorphism "No path selected"
-                      widgetSetSensitive btnCheck False
+  let update = do
+        mf <- getSelectedSingle trvFinder listFinder
+        case mf of
+          Just (_,f) -> do
+            case comorphism f !! selected f of
+              Comorphism cid ->let cN = language_name cid
+                                   dN = drop 1 $ dropWhile (/= ';') cN in
+                labelSetLabel lblComorphism $ if null dN then "identity" else dN
+            widgetSetSensitive btnCheck True
+          Nothing -> do
+            labelSetLabel lblComorphism "No path selected"
+            widgetSetSensitive btnCheck False
   setListSelectorSingle trvFinder update
 
-  selection <- setListSelectorMultiple trvNodes btnNodesAll btnNodesNone
-                 btnNodesInvert $ updateNodes trvNodes listNodes
-                                    (\ s -> do
-                                       labelSetLabel lblSublogic $ show s
-                                       updateFinder trvFinder listFinder s)
-                                    (do labelSetLabel lblSublogic "No sublogic"
-                                        listStoreClear listFinder
-                                        activate widgets False
-                                        widgetSetSensitive btnCheck False)
-                                    (do activate widgets True
-                                        widgetSetSensitive btnCheck False)
+  setListSelectorMultiple trvNodes btnNodesAll btnNodesNone btnNodesInvert
+    $ updateNodes trvNodes listNodes
+    (\ s -> do labelSetLabel lblSublogic $ show s
+               updateFinder trvFinder listFinder s)
+    (do labelSetLabel lblSublogic "No sublogic"
+        listStoreClear listFinder
+        activate widgets False
+        widgetSetSensitive btnCheck False)
+    (do activate widgets True; widgetSetSensitive btnCheck False)
 
   -- bindings
   let selectWith f = do
-        mModel <- treeViewGetModel trvNodes
-        case mModel of
-          Nothing -> return ()
-          Just m -> do
-            writeIORef selection []
-            selector <- treeViewGetSelection trvNodes
-            treeModelForeach m $ \ iter -> do
-              path@(row:[]) <- treeModelGetPath m iter
-              (FNode { status = s }) <- listStoreGetValue listNodes row
-              if f s then do
-                  treeSelectionSelectIter selector iter
-                  modifyIORef selection (path:)
-                else treeSelectionUnselectIter selector iter
-              return False
+        model <- treeViewGetModel trvNodes
+        sel <- treeViewGetSelection trvNodes
+        treeModelForeach (fromJust model) $ \ i -> do
+          (row:[]) <- treeModelGetPath (fromJust model) i
+          (FNode { status = s }) <- listStoreGetValue listNodes row
+          (if f s then treeSelectionSelectIter else treeSelectionUnselectIter)
+            sel i
+          return False
 
   onClicked btnNodesUnchecked $ selectWith (== CSUnchecked)
@@ -276 +263 @@
                   let n = getPName cc
                       f = Map.findWithDefault (Finder n cc [] 0) n m in
-                  Map.insert n (f { comorphs = c : comorphs f}) m
+                  Map.insert n (f { comorphism = c : comorphism f}) m
                 ) Map.empty
                 $ getConsCheckers $ findComorphismPaths logicGraph sl)
@@ -287 +274 @@
 check :: LibName -> LibEnv -> DGraph -> Finder -> Int
       -> (Double -> String -> IO ()) -> [(Int,FNode)] -> IO [(Int, FNode)]
-check ln le dg (Finder { finder = cc, comorphs = cs, selected = i}) timeout
+check ln le dg (Finder { finder = cc, comorphism = cs, selected = i}) timeout
       update nodes = do
   let count' = fromIntegral $ length nodes
@@ -306 +293 @@
                (\ (n,_,c) -> n ++ ": " ++ show c) $ concatMap expand paths
       case ret of
-        Just (_,(n,_,c)) -> case findIndex ((n ==) . fname) paths of
-          Just i -> let f = paths !! i in case findIndex (c ==) $ comorphs f of
-            Just i' -> do
-              listStoreSetValue list i $ f { selected = i' }
-              treeSelectionSelectPath selector [i]
-              unlock
-            Nothing -> return ()
+        Just (_,(n,_,c)) -> case findIndex ((n ==) . fName) paths of
+          Just i -> let f = paths !! i in
+            case findIndex (c ==) $ comorphism f of
+              Just i' -> do
+                listStoreSetValue list i $ f { selected = i' }
+                treeSelectionSelectPath selector [i]
+                unlock
+              Nothing -> return ()
           Nothing -> return ()
         Nothing -> return ()
 
 expand :: Finder -> [(String, G_cons_checker, AnyComorphism)]
-expand (Finder { fname = n, finder = cc, comorphs = cs }) =
+expand (Finder { fName = n, finder = cc, comorphism = cs }) =
   map (\ c -> (n,cc,c)) cs
 

trunk/GUI/GtkGenericATP.hs

@@ -12 +12 @@
 -}
 
-module GUI.GtkGenericATP (genericATPgui) where
+module GUI.GtkGenericATP ( genericATPgui ) where
 
 import Graphics.UI.Gtk
@@ -36 +36 @@
 
 import Logic.Prover
-
-data Goal = Goal { name :: String
-                 , status :: GStatus }
-
-data GStatus = GOpen
-             | GTimeout
-             | GDisproved
-             | GInconsistent
-             | GProved
-               deriving (Eq, Ord)
-
-instance Show Goal where
-  show (Goal { name = n, status = s }) = spanString s $ statusToPrefix s ++ n
-
-statusToColor :: GStatus -> String
-statusToColor s = case s of
-  GOpen         -> "black"
-  GProved       -> "green"
-  GDisproved    -> "red"
-  GTimeout      -> "blue"
-  GInconsistent -> "orange"
-
-statusToPrefix :: GStatus -> String
-statusToPrefix s = case s of
-  GOpen         -> "[ ] "
-  GProved       -> "[+] "
-  GDisproved    -> "[-] "
-  GTimeout      -> "[t] "
-  GInconsistent -> "[*] "
-
-spanString :: GStatus -> String -> String
-spanString s m = "<span color=\"" ++ statusToColor s ++ "\">" ++ m ++ "</span>"
-
-instance Show GStatus where
-  show GProved       = spanString GProved       "Proved"
-  show GInconsistent = spanString GInconsistent "Proved (Theory inconsistent!)"
-  show GDisproved    = spanString GDisproved    "Disproved"
-  show GOpen         = spanString GOpen         "Open"
-  show GTimeout      = spanString GTimeout      "Open (Timeout!)"
 
 genericATPgui :: (Ord proof_tree, Ord sentence)
@@ -117 +78 @@
     windowSetTitle window $ prName ++ ": " ++ thName
 
-    let widgets = [ toWidget trvGoals        , toWidget btnClose
+    let widgets = [ toWidget btnClose        , toWidget btnShowDetails
                   , toWidget btnHelp         , toWidget btnSaveConfig
                   , toWidget sbTimeout       , toWidget entryOptions
                   , toWidget cbIncludeProven , toWidget btnProveSelected
                   , toWidget btnProveSelected, toWidget btnProveAll
-                  , toWidget lblStatus       , toWidget trvAxioms
-                  , toWidget btnSaveProblem  , toWidget btnShowDetails
-                  ]
+                  , toWidget lblStatus       , toWidget btnSaveProblem ]
         switch = activate widgets
         switchAll b = do
@@ -140 +99 @@
 
     -- setting up lists
-    listGoals <- setListData trvGoals show $
-      map (\ g -> let n = AS_Anno.senAttr g
-                      cfg = Map.findWithDefault (error "Config not found!") n
-                              $ configsMap initState
-                  in Goal { name = n
-                          , status = toGStatus cfg }) initGoals
+    listGoals <- setListData trvGoals show $ toGoals initState
     listAxioms <- setListData trvAxioms id []
 
@@ -161 +115 @@
       -- setting new selected goal
       mSelected <- getSelectedSingle trvGoals listGoals
-      let s = maybe s' (\ (_, Goal { name = n }) -> s' { currentGoal = Just n})
+      let s = maybe s' (\ (_, Goal { gName = n }) -> s' { currentGoal = Just n})
                     mSelected
       putMVar stateMVar s
@@ -221 +175 @@
 
     -- show details of selected goal
-    onClicked btnStop $ tryTakeMVar threadId >>=maybe (return ()) killThread
+    onClicked btnStop $ do
+      tryTakeMVar threadId >>=maybe (return ()) killThread
+      putMVar threadId tid'
 
     -- show details of selected goal
@@ -277 +233 @@
                 ATPError m -> errorDialog "Error" m
                 _ -> return ()
-              postGUISync $ do
+              postGUIAsync $ do
                 let progress = fromIntegral gPSF / fromIntegral numGoals
                 if cont then updat progress $ AS_Anno.senAttr $ fromJust nextSen
@@ -286 +242 @@
                 s' <- readMVar stateMVar
                 update' s'
-                return cont)
+              return cont)
         updat 0 firstGoalName
         switchAll False
@@ -367 +323 @@
   let newGoals = goalsList s
       oldGoals = foldl (\ gs g -> (g, length gs):gs) [] oldGoals'
-  mapM_ (\ g -> do
-      let n = AS_Anno.senAttr g
-          (g', idx) = fromMaybe (error "Goal not found!")
-                        $ find (\ (Goal { name = n' }, _) -> n == n') oldGoals
-          cfg = Map.findWithDefault (error "Config not found!") n $ configsMap s
-      listStoreSetValue listGoals idx $ g' { status = toGStatus cfg }
+  mapM_ (\ g' -> do
+      let n = AS_Anno.senAttr g'
+          (g, idx) = fromMaybe (error "Goal not found!")
+                        $ find (\ (Goal { gName = n' }, _) -> n == n') oldGoals
+          c = Map.findWithDefault (error "Config not found!") n $ configsMap s
+      listStoreSetValue listGoals idx $ g { gStatus = genericConfigToGStatus c }
     ) newGoals
 
@@ -378 +334 @@
   selected <- getSelectedSingle trvGoals listGoals
   case selected of
-    Just (_, Goal { name = n, status = stat }) -> do
+    Just (_, Goal { gName = n, gStatus = stat }) -> do
       let cfg = Map.findWithDefault (error "GUI.GenericATP.updateDisplay") n
                   $ configsMap s
@@ -396 +352 @@
 setExtraOpts opts c = c { extraOpts = opts }
 
--- | Converts a ProofStatus into a GStatus
-toGStatus :: GenericConfig proof_tree -> GStatus
-toGStatus cfg = case goalStatus $ proofStatus cfg of
-  Proved (Just True) -> GProved
-  Proved _           -> GInconsistent
-  Disproved          -> GDisproved
-  Open _             -> if timeLimitExceeded cfg then GTimeout else GOpen
+toGoals :: GenericState sign sentence proof_tree pst -> [Goal]
+toGoals s = map (\ g ->
+  let n = AS_Anno.senAttr g
+      c = Map.findWithDefault (error "Config not found!") n $ configsMap s
+  in Goal { gName = n, gStatus = genericConfigToGStatus c }) $ goalsList s

trunk/GUI/GtkProverGUI.hs

@@ -12 +12 @@
 -}
 
-module GUI.GtkProverGUI
-  (showProverGUI)
-  where
+module GUI.GtkProverGUI ( showProverGUI ) where
 
 import Graphics.UI.Gtk
@@ -21 +19 @@
 import GUI.GtkUtils
 import qualified GUI.Glade.ProverGUI as ProverGUI
+import GUI.HTkProofDetails -- not implemented in Gtk
 
 import Common.AS_Annotation as AS_Anno
 import qualified Common.Doc as Pretty
-import qualified Common.Result as Result
+import Common.Result
 import qualified Common.OrderedMap as OMap
 import Common.ExtSign
 
+import Control.Monad ((<=<))
 import Control.Concurrent.MVar
 
@@ -40 +40 @@
 import Static.GTheory
 
-import Monad (when)
-
-import Data.IORef
 import qualified Data.Map as Map
 import Data.List
+import Data.Maybe ( fromJust, fromMaybe, isJust )
+
+data GProver = GProver { pName :: String
+                       , prover :: G_prover
+                       , comorphism :: [AnyComorphism]
+                       , selected :: Int }
 
 {- ProverGUI -}
 
 -- | Displays the consistency checker window
-showProverGUI ::
-  (Logic lid sublogics basic_spec sentence symb_items symb_map_items
-         sign morphism symbol raw_symbol proof_tree)
+showProverGUI :: Logic lid sublogics basic_spec sentence symb_items
+                       symb_map_items sign morphism symbol raw_symbol proof_tree
   => lid
   -> ProofActions lid sentence -- ^ record of possible GUI actions
@@ -60 +62 @@
   -> [(G_prover,AnyComorphism)] -- ^ list of suitable comorphisms to provers
                                 -- for sublogic of G_theory
-  -> IO (Result.Result G_theory)
-showProverGUI lid prGuiAcs thName warningTxt th knownProvers comorphList = do
+  -> IO (Result G_theory)
+showProverGUI lid prGuiAcs thName warn th knownProvers comorphList = do
   initState <- (initialState lid thName th knownProvers comorphList
                 >>= recalculateSublogicF prGuiAcs)
@@ -106 +108 @@
 
     -- set list data
-    listProvers <- setListData trvProvers id $ Map.keys $ proversMap initState
-    listGoals <- setListData trvGoals id $ OMap.keys $ goalMap initState
-    listAxioms <- setListData trvAxioms id
-                    $ map (\ (k,s) -> if wasTheorem s then "(Th) " ++ k else k)
-                    $ OMap.toList axioms
-    listTheorems <- setListData trvTheorems (id) $ OMap.keys $ goalMap initState
+    listProvers <- setListData trvProvers pName []
+    listGoals <- setListData trvGoals show $ toGoals initState
+    listAxioms <- setListData trvAxioms id $ toAxioms axioms
+    listTheorems <- setListData trvTheorems id $ toTheorem initState
+
+    let noProver = [ toWidget btnFineGrained
+                   , toWidget btnProve
+                   , toWidget lblComorphism
+                   , toWidget lblSublogic ]
+        noAxiom = [ toWidget btnAxiomsAll
+                  , toWidget btnAxiomsNone
+                  , toWidget btnAxiomsInvert
+                  , toWidget btnAxiomsFormer ]
+        noTheory = [ toWidget btnTheoremsAll
+                   , toWidget btnTheoremsNone
+                   , toWidget btnTheoremsInvert ]
+        noGoal = [ toWidget btnGoalsAll
+                 , toWidget btnGoalsNone
+                 , toWidget btnGoalsInvert
+                 , toWidget btnGoalsSelectOpen ]
+        prove = noProver ++ noAxiom ++ noTheory ++ noGoal ++
+                [ toWidget btnShowTheory
+                , toWidget btnShowSelectedTheory
+                , toWidget btnClose
+                , toWidget btnProofDetails
+                , toWidget btnDisplay ]
+        update s' = do
+          s <- updateGoals trvGoals listGoals =<<
+               updateComorphism lblComorphism trvProvers listProvers =<<
+               updateProver trvProvers listProvers =<<
+               updateSublogic lblSublogic prGuiAcs knownProvers =<<
+               setSelectedGoals trvGoals listGoals =<<
+               setSelectedSens trvAxioms listAxioms trvTheorems listTheorems s'
+          activate noProver
+            (isJust (selectedProver s) && not (null $ selectedGoals s))
+          return s
+
+    activate noGoal (not $ OMap.null $ goalMap initState)
+    activate noAxiom (not $ OMap.null axioms)
+    activate noTheory (not $ OMap.null $ goalMap initState)
 
     -- setup provers list
-    setListSelectorSingle trvProvers $ modifyMVar_ state
-                                     $ selectProver trvProvers listProvers
-    setSelectedProver trvProvers initState
-
-    let update = updateStatusSublogic lblSublogic trvGoals listGoals trvAxioms
-                   listAxioms trvTheorems listTheorems trvProvers listProvers
-                   prGuiAcs knownProvers
-        action = modifyMVar_ state $ update
+    setListSelectorSingle trvProvers $ modifyMVar_ state $
+      update <=< setSelectedProver trvProvers listProvers
 
     -- setup goal list
-    selectedGoals' <- setListSelectorMultiple trvGoals btnGoalsAll btnGoalsNone
-                        btnGoalsInvert action
-    onClicked btnGoalsSelectOpen $ modifyMVar_ state $ (\ s -> do
-      (Just model) <- treeViewGetModel trvGoals
-      selector <- treeViewGetSelection trvGoals
-      let
-        isOpen st =
-          let thst = thmStatus st
-          in if null thst
-            then True
-            else case maximum $ map snd $ thst of
+    setListSelectorMultiple trvGoals btnGoalsAll btnGoalsNone btnGoalsInvert $
+      modifyMVar_ state update
+
+    onClicked btnGoalsSelectOpen $ modifyMVar_ state $ \ s -> do
+      model <- treeViewGetModel trvGoals
+      sel <- treeViewGetSelection trvGoals
+      let isOpen st = let thst = thmStatus st in
+            null thst || case maximum $ map snd thst of
               BasicProof _ pst -> isOpenGoal $ goalStatus pst
               _ -> False
-        select iter = do
-          (row:[]) <- treeModelGetPath model iter
-          key <- listStoreGetValue listGoals row
-          if maybe (error "goal lookup") isOpen $ OMap.lookup key $ goalMap s
-            then do
-              modifyIORef selectedGoals' ((row:[]):)
-              treeSelectionSelectIter selector iter
-            else treeSelectionUnselectIter selector iter
-          return False
-      writeIORef selectedGoals' []
-      treeModelForeach model select
-      s' <- update s
-      return s')
+      treeModelForeach (fromJust model) $ \ i -> do
+        (row:[]) <- treeModelGetPath (fromJust model) i
+        key <- listStoreGetValue listGoals row
+        (if isOpen $ fromJust $ OMap.lookup (gName key) $ goalMap s
+          then treeSelectionSelectIter else treeSelectionUnselectIter) sel i
+        return False
+      update s
 
     -- setup axioms list
-    selectedAxioms <- setListSelectorMultiple trvAxioms btnAxiomsAll
-                        btnAxiomsNone btnAxiomsInvert action
-    onClicked btnAxiomsFormer $ modifyMVar_ state $ (\ s -> do
+    setListSelectorMultiple trvAxioms btnAxiomsAll btnAxiomsNone btnAxiomsInvert
+      $ modifyMVar_ state update
+    onClicked btnAxiomsFormer $ modifyMVar_ state $ \ s -> do
       aM <- axiomMap s
-      (Just model) <- treeViewGetModel trvAxioms
-      selector <- treeViewGetSelection trvAxioms
-      let
-        isNotFormerTheorem st = not $ wasTheorem st
-        select iter = do
-          (row:[]) <- treeModelGetPath model iter
-          key <- listStoreGetValue listAxioms row
-          k <- case stripPrefix "(Th) " key of
-            Just k -> return k
-            Nothing -> return key
-          if maybe (error "axiom lookup") isNotFormerTheorem $ OMap.lookup k aM
-            then do
-              modifyIORef selectedAxioms ((row:[]):)
-              treeSelectionSelectIter selector iter
-            else treeSelectionUnselectIter selector iter
-          return False
-      writeIORef selectedAxioms []
-      treeModelForeach model select
-      s' <- update s
-      return s')
+      model <- treeViewGetModel trvAxioms
+      sel <- treeViewGetSelection trvAxioms
+      treeModelForeach (fromJust model) $ \ i -> do
+        (row:[]) <- treeModelGetPath (fromJust model) i
+        key <- listStoreGetValue listAxioms row
+        k <- case stripPrefix "(Th) " key of
+          Just k -> return k
+          Nothing -> return key
+        (if not $ wasTheorem $ fromJust $ OMap.lookup k aM
+          then treeSelectionSelectIter else treeSelectionUnselectIter) sel i
+        return False
+      update s
+
+    modifyMVar_ state $ update <=< updateProver trvProvers listProvers
 
     -- setup theorems list
     setListSelectorMultiple trvTheorems btnTheoremsAll btnTheoremsNone
-                            btnTheoremsInvert action
+                            btnTheoremsInvert $ modifyMVar_ state update
 
     -- button bindings
@@ -185 +200 @@
 
     onClicked btnShowTheory $
-      displayTheoryWithWarning "Theory" thName warningTxt th
+      displayTheoryWithWarning "Theory" thName warn th
 
     onClicked btnShowSelectedTheory $ do
       s <- readMVar state
-      displayTheoryWithWarning "Selected Theory" thName warningTxt
-                               (selectedTheory s)
-
-    onClicked btnDisplay $ do
+      displayTheoryWithWarning "Selected Theory" thName warn $ selectedTheory s
+
+    onClicked btnDisplay $ readMVar state >>= displayGoals
+
+    onClicked btnProofDetails $ do
       s <- readMVar state
-      displayGoals s
-
-    onClicked btnProofDetails $ return ()
-
-    onClicked btnProve $ return ()
-
-    onClicked btnFineGrained $ forkIO_ $ modifyMVar_ state $ (\ s -> do
-      let s' = s { proverRunning = True }
-      prState <- update s'
-      Result.Result ds ms'' <- fineGrainedSelectionF prGuiAcs prState
-      s'' <- case ms'' of
-        Nothing -> do
-          -- Is error needed?
-          --errorDialog "Error" (showRelDiags 2 ds)
-          return s'
-        Just res -> return res
-      return s'' { proverRunning = False
-                 , accDiags = accDiags s'' ++ ds })
+      forkIO_ $ doShowProofDetails s
+
+    onClicked btnProve $ do
+      activate prove False
+      forkIOWithPostProcessing (readMVar state >>= proveF prGuiAcs)
+        $ \ (Result ds ms) -> do
+            s <- case ms of
+              Nothing -> do
+                errorDialog "Error" (showRelDiags 2 ds)
+                takeMVar state
+              Just res -> do
+                takeMVar state
+                return res
+            activate prove True
+            putMVar state =<< update s { proverRunning = False
+                                       , accDiags = accDiags s ++ ds}
+
+    onClicked btnFineGrained $ modifyMVar_ state $ \ s -> do
+      mp <- fineGrainedSelection trvProvers listProvers
+      update <=< updateProver trvProvers listProvers
+        $ maybe s (\ p -> s { selectedProver = Just $ pName p }) mp
 
     onDestroy window $ putMVar wait ()
@@ -218 +237 @@
 
   _ <- takeMVar wait
-  return $ Result.Result { Result.diags = []
-                         , Result.maybeResult = Nothing }
+  s <- takeMVar state
+  case theory s of
+    G_theory lidT sigT indT sensT _ -> do
+      gMap <- coerceThSens (logicId s) lidT "ProverGUI last coerce" $ goalMap s
+      return Result { diags = accDiags s
+                    , maybeResult = Just $ G_theory lidT sigT indT
+                                             (Map.union sensT gMap) startThId }
 
 -- | Called whenever the button "Display" is clicked.
-displayGoals ::
-  (Logic lid sublogics basic_spec sentence symb_items symb_map_items
-         sign morphism symbol raw_symbol proof_tree)
-  => ProofState lid sentence
-  -> IO ()
+displayGoals :: Logic lid sublogics basic_spec sentence symb_items
+                      symb_map_items sign morphism symbol raw_symbol proof_tree
+             => ProofState lid sentence -> IO ()
 displayGoals s = case theory s of
   G_theory lid1 (ExtSign sig1 _) _ _ _ -> do
     let thName = theoryName s
-        goalsText s' = show $ Pretty.vsep $
-                       map (print_named lid1 .
-                            AS_Anno.mapNamed (simplify_sen lid1 sig1)) $
-                       toNamedList s'
+        goalsText = show . Pretty.vsep
+          . map (print_named lid1 . AS_Anno.mapNamed (simplify_sen lid1 sig1))
+          . toNamedList
         sens = selectedGoalMap s
     sens' <- coerceThSens (logicId s) lid1 "" sens
@@ -239 +260 @@
              $ Just (thName ++ "-goals.txt")
 
-setSelectedProver ::
-     TreeView
-  -> ProofState lid sentence
-  -> IO ()
-setSelectedProver view s = do
+fineGrainedSelection :: TreeView -> ListStore GProver -> IO (Maybe GProver)
+fineGrainedSelection view list = do
+  ps <- listStoreToList list
   selector <- treeViewGetSelection view
-  let ind = case selectedProver s of
-              Just sp -> findIndex (==sp) $ Map.keys (proversMap s)
-              Nothing -> Nothing
-  maybe (return ()) (\i -> treeSelectionSelectPath selector [i]) ind
-
-updateStatusSublogic ::
-     Label -- ^ sublogic label
-  -> TreeView -- ^ goals list
-  -> ListStore String -- ^ goals list
-  -> TreeView -- ^ axioms list
-  -> ListStore String -- ^ axioms list store
-  -> TreeView -- ^ theorems list
-  -> ListStore String -- ^ theorems list store
-  -> TreeView -- ^ provers list
-  -> ListStore String -- ^ provers list store
-  -> ProofActions lid sentence -- ^ record of possible GUI actions
-  -> KnownProvers.KnownProversMap -- ^ map of known provers
-  -> ProofState lid sentence
-  -> IO (ProofState lid sentence)
-updateStatusSublogic lbl gls listGls axs listAxs ths listThs prs listPrs
-  prGuiAcs knownProvers s' = do
-  s'' <- updateStateGetSelectedSens axs listAxs ths listThs s'
-  s''' <- updateStateGetSelectedGoals gls listGls s''
-  s <- recalculateSublogicF prGuiAcs $ (s''' {proversMap = knownProvers})
-  setSublogic lbl $ show $ sublogicOfTheory s
-  when (Map.keys (proversMap s') /= Map.keys (proversMap s))
-       (do updateListData listPrs $ Map.keys $ proversMap s'
-           setSelectedProver prs s)
-  return s{ selectedProver =
-              maybe Nothing (\ sp -> find (==sp) $ Map.keys (proversMap s))
-                    (selectedProver s) }
-
-updateStateGetSelectedGoals ::
-     TreeView
-  -> ListStore String
-  -> ProofState lid sentence
-  -> IO (ProofState lid sentence)
-updateStateGetSelectedGoals view listGoals s = do
-  selector <- treeViewGetSelection view
-  rows <- treeSelectionGetSelectedRows selector
-  goals <- mapM (\ (row:[]) -> listStoreGetValue listGoals row) rows
-  return s { selectedGoals = goals }
-
-updateStateGetSelectedSens ::
-     TreeView -- ^ axioms listbox
-  -> ListStore String
-  -> TreeView -- ^ theorems listbox
-  -> ListStore String
-  -> ProofState lid sentence
-  -> IO (ProofState lid sentence)
-updateStateGetSelectedSens axs listAxs ths listThs s = do
-  selectorAxs <- treeViewGetSelection axs
-  selectorThs <- treeViewGetSelection ths
-  rowsAxs <- treeSelectionGetSelectedRows selectorAxs
-  rowsThs <- treeSelectionGetSelectedRows selectorThs
-  axioms <- mapM (\ (row:[]) -> listStoreGetValue listAxs row) rowsAxs
-  theorems <- mapM (\ (row:[]) -> listStoreGetValue listThs row) rowsThs
-  return s { includedAxioms   = axioms
-           , includedTheorems = theorems }
+  if null ps then error "Cant make selection without sublogic!"
+    else do
+      ret <- listChoiceAux "Choose a translation"
+               (\ (n,_,c) -> n ++ ": " ++ show c) $ concatMap expand ps
+      case ret of
+        Just (_,(n,_,c)) -> case findIndex ((n ==) . pName) ps of
+          Just i -> let p = ps !! i in case findIndex (c ==) $ comorphism p of
+            Just i' -> do
+              let p' = p { selected = i' }
+              listStoreSetValue list i p'
+              treeSelectionSelectPath selector [i]
+              return $ Just p'
+            Nothing -> error "can't find selected comorphism"
+          Nothing -> error "can't find selected prover"
+        Nothing -> return Nothing
+
+expand :: GProver -> [(String, G_prover, AnyComorphism)]
+expand (GProver { pName = n, prover = p, comorphism = cs }) =
+  map (\ c -> (n, p, c)) cs
+
+updateSublogic :: Label -> ProofActions lid sentence
+               -> KnownProvers.KnownProversMap -> ProofState lid sentence
+               -> IO (ProofState lid sentence)
+updateSublogic lbl prGuiAcs knownProvers s' = do
+  s <- recalculateSublogicF prGuiAcs s' { proversMap = knownProvers }
+  labelSetLabel lbl $ show $ sublogicOfTheory s
+  return s
+
+updateComorphism :: Label -> TreeView -> ListStore GProver
+                 -> ProofState lid sentence -> IO (ProofState lid sentence)
+updateComorphism lbl trvProvers listProvers s = do
+  mprover <- getSelectedSingle trvProvers listProvers
+  case mprover of
+    Just (_, p) -> case comorphism p !! selected p of
+      Comorphism cid -> let dN = drop 1 $ dropWhile (/= ';') $ language_name cid
+        in labelSetLabel lbl $ if null dN then "identity" else dN
+    Nothing -> return ()
+  return s
+
+updateProver :: TreeView -> ListStore GProver -> ProofState lid sentence
+             -> IO (ProofState lid sentence)
+updateProver trvProvers listProvers s = do
+  let new = toProvers s
+  old <- listStoreToList listProvers
+  let prvs = map (\ p -> case find ((pName p ==) . pName) old of
+          Nothing -> p
+          Just p' -> let oldC = comorphism p' !! selected p' in
+            p { selected = fromMaybe 0 $ findIndex (== oldC) $ comorphism p }
+        ) new
+      selFirst = do
+        selectFirst trvProvers
+        setSelectedProver trvProvers listProvers s
+  updateListData listProvers prvs
+  case selectedProver s of
+    Just p -> case findIndex ((p ==) . pName) prvs of
+      Just i -> do
+        sel <- treeViewGetSelection trvProvers
+        treeSelectionSelectPath sel [i]
+        return s
+      Nothing -> selFirst
+    Nothing -> selFirst
+
+updateGoals :: TreeView -> ListStore Goal -> ProofState lid sentence
+            -> IO (ProofState lid sentence)
+updateGoals trvGoals listGoals s = do
+  updateListData listGoals $ toGoals s
+  model <- treeViewGetModel trvGoals
+  sel <- treeViewGetSelection trvGoals
+  treeModelForeach (fromJust model) $ \ i -> do
+    (row:[]) <- treeModelGetPath (fromJust model) i
+    g <- listStoreGetValue listGoals row
+    (if any (gName g ==) $ selectedGoals s
+      then treeSelectionSelectIter else treeSelectionUnselectIter) sel i
+    return False
+  return s
+
+setSelectedGoals :: TreeView -> ListStore Goal -> ProofState lid sentence
+                 -> IO (ProofState lid sentence)
+setSelectedGoals trvGoals listGoals s = do
+  goals <- getSelectedMultiple trvGoals listGoals
+  return s { selectedGoals = map (gName . snd) goals }
+
+setSelectedSens :: TreeView -> ListStore String -> TreeView -> ListStore String
+                -> ProofState lid sentence -> IO (ProofState lid sentence)
+setSelectedSens axs listAxs ths listThs s = do
+  axioms <- getSelectedMultiple axs listAxs
+  theorems <- getSelectedMultiple ths listThs
+  return s { includedAxioms   = map snd axioms
+           , includedTheorems = map snd theorems }
 
 -- | Called whenever a prover is selected from the "Pick Theorem Prover" list.
-selectProver ::
-     TreeView
-  -> ListStore String
-  -> ProofState lid sentence
-  -> IO (ProofState lid sentence)
-selectProver view listPrs s = do
-  selector <- treeViewGetSelection view
-  ((row:[]):[]) <- treeSelectionGetSelectedRows selector
-  prover <- listStoreGetValue listPrs row
-  return s { selectedProver = Just prover }
-
--- | Called to set sublogic label
-setSublogic :: Label -> String -> IO ()
-setSublogic label text = labelSetLabel label $ "<b>" ++ text ++ "</b>"
-
+setSelectedProver :: TreeView -> ListStore GProver -> ProofState lid sentence
+                  -> IO (ProofState lid sentence)
+setSelectedProver trvProvers listProvers s = do
+  mprover <- getSelectedSingle trvProvers listProvers
+  return s { selectedProver = maybe Nothing (Just . pName . snd) mprover }
+
+toAxioms :: ThSens sentence (AnyComorphism, BasicProof) -> [String]
+toAxioms =
+  map (\ (k,s) -> if wasTheorem s then "(Th) " ++ k else k) . OMap.toList
+
+toGoals :: ProofState lid sentence -> [Goal]
+toGoals = map toGoal . OMap.toList . goalMap
+  where toGoal (n, st) = let ts = thmStatus st in
+          Goal { gName = n
+               , gStatus = if null ts then GOpen
+                           else basicProofToGStatus $ maximum $ map snd ts }
+
+toTheorem :: ProofState lid sentence -> [String]
+toTheorem = OMap.keys . goalMap
+
+toProvers :: ProofState lid sentence -> [GProver]
+toProvers = Map.elems . foldr (\ (p', c) m ->
+    let n = getPName p'
+        p = Map.findWithDefault (GProver n p' [] 0) n m in
+    Map.insert n (p { comorphism = c : comorphism p}) m
+  ) Map.empty . comorphismsToProvers

trunk/GUI/GtkUtils.hs

@@ -72 +72 @@
 
   , activate
+
+  -- * Datatypes and functions for prover
+  , Goal (..)
+  , GStatus (..)
+  , proofStatusToGStatus
+  , basicProofToGStatus
+  , genericConfigToGStatus
   )
   where
@@ -80 +87 @@
 import qualified GUI.Glade.Utils as Utils
 
-import Static.GTheory (G_theory)
+import Static.GTheory
+
 import Common.DocUtils (showDoc)
 
@@ -91 +99 @@
 import System.IO (hFlush, hClose, hPutStr, openTempFile)
 
-import Data.IORef
+import Logic.Prover
+
+import Interfaces.GenericATPState
 
 -- | Returns a GladeXML Object of a xmlstring.
@@ -501 +511 @@
 -- | Setup list with multiple selection
 setListSelectorMultiple :: TreeView -> Button -> Button -> Button -> IO ()
-                        -> IO (IORef [TreePath])
+                        -> IO ()
 setListSelectorMultiple view btnAll btnNone btnInvert action = do
   selector <- treeViewGetSelection view
   treeSelectionSetMode selector SelectionMultiple
-  ioRefSelection <- newIORef ([] :: [TreePath])
 
   -- setup selector
-  onCursorChanged view $ do
-    s' <- treeSelectionGetSelectedRows selector
-    s <- readIORef ioRefSelection
-    let newSelection = [ x | x <- s', notElem x s]
-                    ++ [ x | x <- s, notElem x s']
-    writeIORef ioRefSelection newSelection
-    treeSelectionUnselectAll selector
-    mapM_ (treeSelectionSelectPath selector) newSelection
-    action
+  onCursorChanged view action
 
   treeSelectionSelectAll selector
 
   -- setup buttons
-  onClicked btnAll $ do selectAll view ioRefSelection; action
-  onClicked btnNone $ do selectNone view ioRefSelection; action
-  onClicked btnInvert $ do selectInvert view ioRefSelection; action
-
-  return ioRefSelection
+  onClicked btnAll $ do selectAll view; action
+  onClicked btnNone $ do selectNone view; action
+  onClicked btnInvert $ do selectInvert view; action
+  return ()
 
 -- | Selects the first item if possible
@@ -542 +542 @@
           path <- treeModelGetPath model iter
           treeViewSetCursor view path Nothing
+
+-- | Select all rows
+selectAll :: TreeView -> IO ()
+selectAll view = treeViewGetSelection view >>= treeSelectionSelectAll
+
+-- | Deselect all rows
+selectNone :: TreeView -> IO ()
+selectNone view = treeViewGetSelection view >>= treeSelectionUnselectAll
+
+-- | Invert selection of list
+selectInvert :: TreeView -> IO ()
+selectInvert view = do
+  sel <- treeViewGetSelection view
+  selected <- treeSelectionGetSelectedRows sel
+  treeSelectionSelectAll sel
+  rows <- treeSelectionGetSelectedRows sel
+  mapM_ (\ row -> (if elem row selected
+      then treeSelectionUnselectPath else treeSelectionSelectPath) sel row
+    ) rows
 
 -- | Get selected item
@@ -571 +590 @@
   return $ zip rows items
 
--- | Select all rows
-selectAll :: TreeView -> IORef [TreePath] -> IO ()
-selectAll view ioRefSelection = do
-  selector <- treeViewGetSelection view
-  treeSelectionSelectAll selector
-  s <- treeSelectionGetSelectedRows selector
-  writeIORef ioRefSelection s
-
--- | Deselect all rows
-selectNone :: TreeView -> IORef [TreePath] -> IO ()
-selectNone view ioRefSelection = do
-  selector <- treeViewGetSelection view
-  treeSelectionUnselectAll selector
-  writeIORef ioRefSelection []
-
--- | Invert selection of list
-selectInvert :: TreeView -> IORef [TreePath] -> IO ()
-selectInvert view ioRefSelection = do
-  selector <- treeViewGetSelection view
-  old <- treeSelectionGetSelectedRows selector
-  treeSelectionSelectAll selector
-  mapM_ (treeSelectionUnselectPath selector) old
-  new <- treeSelectionGetSelectedRows selector
-  writeIORef ioRefSelection new
-
 -- | Sets data of list
 setListData :: TreeView -> (a -> String) -> [a] -> IO (ListStore a)
@@ -619 +613 @@
 activate :: [Widget] -> Bool -> IO ()
 activate widgets active = mapM_ (\ w -> widgetSetSensitive w active) widgets
+
+
+-- * Datatypes and functions for prover
+
+data Goal = Goal { gName :: String
+                 , gStatus :: GStatus }
+
+data GStatus = GOpen
+             | GTimeout
+             | GDisproved
+             | GInconsistent
+             | GProved
+             | GGuessed
+             | GConjectured
+             | GHandwritten
+               deriving (Eq, Ord)
+
+instance Show Goal where
+  show (Goal { gName = n, gStatus = s }) = spanString s $ statusToPrefix s ++ n
+
+statusToColor :: GStatus -> String
+statusToColor s = case s of
+  GOpen         -> "black"
+  GProved       -> "green"
+  GDisproved    -> "red"
+  GTimeout      -> "blue"
+  GInconsistent -> "orange"
+  GGuessed      -> "darkgreen"
+  GConjectured  -> "darkgreen"
+  GHandwritten  -> "darkgreen"
+
+statusToPrefix :: GStatus -> String
+statusToPrefix s = case s of
+  GOpen         -> "[ ] "
+  GProved       -> "[+] "
+  GDisproved    -> "[-] "
+  GTimeout      -> "[t] "
+  GInconsistent -> "[*] "
+  GGuessed      -> "[.] "
+  GConjectured  -> "[:] "
+  GHandwritten  -> "[/] "
+
+spanString :: GStatus -> String -> String
+spanString s m = "<span color=\"" ++ statusToColor s ++ "\">" ++ m ++ "</span>"
+
+instance Show GStatus where
+  show GProved       = spanString GProved       "Proved"
+  show GInconsistent = spanString GInconsistent "Proved by contradiction"
+  show GDisproved    = spanString GDisproved    "Disproved"
+  show GOpen         = spanString GOpen         "Open"
+  show GTimeout      = spanString GTimeout      "Open (Timeout!)"
+  show GGuessed      = spanString GGuessed      "Guessed"
+  show GConjectured  = spanString GConjectured  "Conjectured"
+  show GHandwritten  = spanString GHandwritten  "Handwritten"
+
+-- | Converts a ProofStatus into a GStatus
+proofStatusToGStatus :: forall a . ProofStatus a -> GStatus
+proofStatusToGStatus p = case goalStatus p  of
+  Proved (Just True) -> GProved
+  Proved _           -> GInconsistent
+  Disproved          -> GDisproved
+  Open _             -> GOpen
+
+-- | Converts a BasicProof into a GStatus
+basicProofToGStatus :: BasicProof -> GStatus
+basicProofToGStatus p = case p of
+  BasicProof _ st -> proofStatusToGStatus st
+  Guessed         -> GGuessed
+  Conjectured     -> GConjectured
+  Handwritten     -> GHandwritten
+
+-- | Converts a GenericConfig into a GStatus
+genericConfigToGStatus :: GenericConfig a -> GStatus
+genericConfigToGStatus cfg = case proofStatusToGStatus $ proofStatus cfg of
+  GOpen -> if timeLimitExceeded cfg then GTimeout else GOpen
+  s     -> s

trunk/GUI/HTkGenericATP.hs

@@ -86 +86 @@
 -}
 statusProvedButInconsistent :: (ProofStatusColour, String)
-statusProvedButInconsistent = (Brown, "Proved (Theory inconsistent!)")
+statusProvedButInconsistent = (Brown, "Proved by contradiction")
 
 {- |