Changeset 12783

Timestamp:

05.11.2009 16:19:05 (2 weeks ago)

Author:

raider

Message:

fixed some bugs. gtk prover gui almost working. moved GUIMVar to HTkUtils

Location:

trunk/GUI

Files:

• GraphTypes.hs (modified) (1 diff)
• GtkGenericATP.hs (modified) (5 diffs)
• GtkProverGUI.hs (modified) (4 diffs)
• HTkProverGUI.hs (modified) (2 diffs)
• HTkUtils.hs (modified) (2 diffs)

trunk/GUI/GraphTypes.hs

@@ -26 +26 @@
 
 import GUI.GraphAbstraction(GraphInfo, initGraph)
-import GUI.HTkProverGUI (GUIMVar)
+import GUI.HTkUtils (GUIMVar)
 import GUI.UDGUtils
 

trunk/GUI/GtkGenericATP.hs

@@ -22 +22 @@
 import Interfaces.GenericATPState
 
-import Control.Concurrent (forkIO, killThread, myThreadId)
+import Control.Concurrent (forkIO, killThread, yield)
 import Control.Concurrent.MVar
+import Control.Monad (unless, when)
 
 import Common.AS_Annotation as AS_Anno
@@ -95 +96 @@
 
     stateMVar <- newMVar initState
-    tid' <- myThreadId
-    threadId <- newMVar tid'
+    threadId <- newEmptyMVar
+    finished <- newEmptyMVar
 
     -- setting up lists
@@ -176 +177 @@
     -- show details of selected goal
     onClicked btnStop $ do
-      tryTakeMVar threadId >>=maybe (return ()) killThread
-      putMVar threadId tid'
+      tryTakeMVar threadId >>= maybe (error "MVar 'tId' not set") killThread
+      putMVar finished ()
 
     -- show details of selected goal
@@ -227 +228 @@
                               $ map AS_Anno.senAttr $ goalsList s
             opts = words opts'
-            afterEachProofAttempt = (\ gPSF nSen nextSen cfg@(retval,_) -> do
+            afterEachProofAttempt = \ gPSF nSen nextSen cfg@(retval,_) -> do
               cont <- goalProcessed stateMVar timeout opts numGoals prName
                                     gPSF nSen False cfg
@@ -233 +234 @@
                 ATPError m -> errorDialog "Error" m
                 _ -> return ()
-              postGUIAsync $ do
-                let progress = fromIntegral gPSF / fromIntegral numGoals
-                if cont then updat progress $ AS_Anno.senAttr $ fromJust nextSen
-                  else do
-                    switchAll True
-                    takeMVar threadId
-                    return ()
+              postGUISync $ do
                 s' <- readMVar stateMVar
                 update' s'
-              return cont)
+                let progress = fromIntegral gPSF / fromIntegral numGoals
+                when cont $ updat progress $ AS_Anno.senAttr $ fromJust nextSen
+                return cont
         updat 0 firstGoalName
-        switchAll False
-        mtid <- tryTakeMVar threadId
-        maybe (error "MVar was not set.") (\ _ -> return ()) mtid
         tid <- forkIO $ do
+          yield
           genericProveBatch False timeout opts inclProven saveBatch
             afterEachProofAttempt (atpInsertSentence atpFun) (runProver atpFun)
             prName thName s Nothing
-          return ()
-        putMVar threadId tid
+          b <- isEmptyMVar threadId
+          unless b $ putMVar finished ()
+        b <- tryPutMVar threadId tid
+        unless b $ error "MVar 'threadId' already set"
+        switchAll False
         forkIO_ $ do
-          putMVar threadId tid'
-          postGUISync $ do
+          takeMVar finished
+          tryTakeMVar threadId
+          postGUIAsync $ do
             switchAll True
             exit

trunk/GUI/GtkProverGUI.hs

@@ -158 +158 @@
 
     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
-      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
+      treeSelectionSelectAll sel
+      rs <- treeSelectionGetSelectedRows sel
+      mapM_ ( \ p@(row:[]) -> do
+        i <- listStoreGetValue listGoals row
+        let isOpen st = let thst = thmStatus st in
+              null thst || case maximum $ map snd thst of
+                BasicProof _ pst -> isOpenGoal $ goalStatus pst
+                _ -> False
+        (if isOpen $ fromJust $ OMap.lookup (gName i) $ goalMap s
+          then treeSelectionSelectPath else treeSelectionUnselectPath) sel p) rs
       update s
 
@@ -175 +174 @@
     setListSelectorMultiple trvAxioms btnAxiomsAll btnAxiomsNone btnAxiomsInvert
       $ modifyMVar_ state update
+
     onClicked btnAxiomsFormer $ modifyMVar_ state $ \ s -> do
-      aM <- axiomMap 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
+      treeSelectionSelectAll sel
+      rs <- treeSelectionGetSelectedRows sel
+      mapM_ ( \ p@(row:[]) -> do
+        i <- listStoreGetValue listAxioms row
+        (if wasTheorem $ fromJust $ OMap.lookup (stripPrefixAxiom i) axioms
+          then treeSelectionUnselectPath else treeSelectionSelectPath) sel p) rs
       update s
 
@@ -199 +194 @@
     onClicked btnClose $ widgetDestroy window
 
-    onClicked btnShowTheory $
-      displayTheoryWithWarning "Theory" thName warn th
-
-    onClicked btnShowSelectedTheory $ do
-      s <- readMVar state
-      displayTheoryWithWarning "Selected Theory" thName warn $ selectedTheory s
+    onClicked btnShowTheory $ displayTheoryWithWarning "Theory" thName warn th
+
+    onClicked btnShowSelectedTheory $ readMVar state >>=
+      displayTheoryWithWarning "Selected Theory" thName warn . selectedTheory
 
     onClicked btnDisplay $ readMVar state >>= displayGoals
 
-    onClicked btnProofDetails $ do
-      s <- readMVar state
-      forkIO_ $ doShowProofDetails s
+    onClicked btnProofDetails $ forkIO_ $ readMVar state >>= doShowProofDetails
 
     onClicked btnProve $ do
@@ -351 +342 @@
   axioms <- getSelectedMultiple axs listAxs
   theorems <- getSelectedMultiple ths listThs
-  return s { includedAxioms   = map snd axioms
+  return s { includedAxioms   = map (stripPrefixAxiom . snd) axioms
            , includedTheorems = map snd theorems }
+
+stripPrefixAxiom :: String -> String
+stripPrefixAxiom a = case stripPrefix "(Th) " a of
+  Just a' -> a'
+  Nothing -> a
 
 -- | Called whenever a prover is selected from the "Pick Theorem Prover" list.

trunk/GUI/HTkProverGUI.hs

@@ -43 +43 @@
 
 -- * Proof Management GUI
-
--- ** some types
-
--- | Type for storing the proof management window
-type GUIMVar = Conc.MVar (Maybe Toplevel)
 
 -- ** Defining the view
@@ -331 +326 @@
                 closing the window; while the window is open it is filled with
                 the Toplevel -}
-    -> IO (Result.Result G_theory)
+  -> IO (Result.Result G_theory)
 proofManagementGUI lid prGuiAcs
                    thName warningTxt th

trunk/GUI/HTkUtils.hs

@@ -15 +15 @@
   , LBStatusIndicator (..)
   , EnableWid (..)
+  , GUIMVar
   , listBox
   , errorMess
@@ -51 +52 @@
 
 import Common.DocUtils
+
+import Control.Concurrent.MVar
+
+
+-- ** some types
+
+-- | Type for storing the proof management window
+type GUIMVar = MVar (Maybe Toplevel)
 
 -- | create a window with title and list of options, return selected option