Changeset 11229

Timestamp:

07.01.2009 14:11:49 (10 months ago)

Author:

rpascanu

Message:

Changes to GUI to use common datatypes in Interfaces

Location:

trunk

Files:

• GUI/GraphDisplay.hs (modified) (4 diffs)
• GUI/GraphLogic.hs (modified) (26 diffs)
• GUI/GraphMenu.hs (modified) (11 diffs)
• GUI/GraphTypes.hs (modified) (7 diffs)
• GUI/History.hs (modified) (1 diff)
• GUI/ShowGraph.hs (modified) (2 diffs)
• GUI/ShowLibGraph.hs (modified) (5 diffs)
• Interfaces/History.hs (modified) (1 diff)
• PGIP/DataTypesUtils.hs (modified) (1 diff)
• PGIP/DgCommands.hs (modified) (4 diffs)
• Proofs/InferBasic.hs (modified) (10 diffs)

trunk/GUI/GraphDisplay.hs

@@ -44 +44 @@
 import Control.Concurrent.MVar
 
+import Interfaces.DataTypes
+
 initializeConverter :: IO (GInfo,HTk.HTk)
 initializeConverter = do
@@ -54 +56 @@
     graphInfo it is contained in and the conversion maps. -}
 convertGraph :: ConvFunc
-convertGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                          , gi_GraphInfo = actGraphInfo
-                          , gi_LIB_NAME = libname
+convertGraph gInfo@(GInfo { gi_GraphInfo = actGraphInfo
                           , windowCount = wc
                           }) title showLib = do
-  libEnv <- readIORef ioRefProofStatus
-  case Map.lookup libname libEnv of
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> error "Something went wrong, no library loaded"
+  Just ist -> do
+   let libEnv = i_libEnv ist
+       libname = i_ln ist
+   case Map.lookup libname libEnv of
     Just dgraph -> do
       case openlock dgraph of
@@ -87 +92 @@
         Nothing -> do
           lock <- newEmptyMVar
-          writeIORef ioRefProofStatus
-            $ Map.insert libname dgraph{openlock = Just lock} libEnv
+          let nwle = Map.insert libname dgraph{openlock = Just lock} libEnv
+              nwst = ost { i_state = Just $ ist { i_libEnv = nwle}}
+          writeIORef (intState gInfo) nwst
           convertGraph gInfo title showLib
     Nothing -> error $ "development graph with libname " ++ show libname
@@ -96 +102 @@
 -- return type equals the one of convertGraph
 initializeGraph :: GInfo -> String -> LibFunc -> IO ()
-initializeGraph gInfo@(GInfo { gi_LIB_NAME = ln }) title showLib = do
-  let title' = (title ++ " for " ++ show ln)
-  createGraph gInfo title' (convertGraph) (showLib)
+initializeGraph gInfo title showLib = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let ln = i_ln ist
+       title' = (title ++ " for " ++ show ln)
+   createGraph gInfo title' (convertGraph) (showLib)

trunk/GUI/GraphLogic.hs

@@ -107 +107 @@
 import Control.Concurrent.MVar
 
+import Interfaces.History
+import Interfaces.DataTypes
+
 -- | Locks the global lock and runs function
 runAndLock :: GInfo -> IO () -> IO ()
@@ -127 +130 @@
 -- | Undo one step of the History
 undo :: GInfo -> Bool -> IO ()
-undo gInfo@(GInfo { globalHist = gHist
-                  , gi_GraphInfo = actGraph
-                  }) isUndo = do
-  (guHist, grHist) <- takeMVar gHist
-  case if isUndo then guHist else grHist of
-    [] -> do
-       GA.showTemporaryMessage actGraph "History is empty..."
-       putMVar gHist (guHist, grHist)
-    lns : gHist' -> do
-      undoDGraphs gInfo isUndo lns
-      putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
-                                else (reverse lns : guHist, gHist')
-
-undoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
-undoDGraphs g u = mapM_ $ undoDGraph g u
-
-undoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
-undoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                        , gi_GraphInfo = actGraph
-                        }) isUndo ln = do
-  GA.showTemporaryMessage actGraph $
-        (if isUndo then "Un" else "Re") ++ "do last change to "
-        ++ show ln ++ "..."
-  lockGlobal gInfo
-  le <- readIORef ioRefProofStatus
-  let
-    dg = lookupDGraph ln le
-    (dg', changes) = (if isUndo then undoHistStep else redoHistStep) dg
-  writeIORef ioRefProofStatus $ Map.insert ln dg' le
-  case openlock dg' of
-    Nothing -> return ()
-    Just lock -> do
-      mvar <- tryTakeMVar lock
-      case mvar of
-        Nothing -> return ()
-        Just applyHist -> do
-          applyHist changes
-          putMVar lock applyHist
-  unlockGlobal gInfo
+undo gInfo@(GInfo { gi_GraphInfo = actGraph }) isUndo = 
+ do
+  intSt <- readIORef $ intState gInfo
+  let nwSt = if isUndo then undoOneStep intSt else redoOneStep intSt 
+  writeIORef (intState gInfo) nwSt
+  remakeGraph gInfo
 
 -- | reloads the Library of the DevGraph
 reload :: GInfo -> IO()
-reload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                    , gi_LIB_NAME = ln
-                    , gi_hetcatsOpts = opts
+reload gInfo@(GInfo { gi_hetcatsOpts = opts
                     , gi_GraphInfo = actGraphInfo
                     }) = do
   lockGlobal gInfo
-  oldle <- readIORef ioRefProofStatus
-  let
-    libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
+  oldst <- readIORef $ intState gInfo
+  case i_state oldst of 
+   Nothing -> do 
+               unlockGlobal gInfo
+               return ()
+   Just ist -> do
+    let
+     oldle = i_libEnv ist
+     ln = i_ln ist
+     libdeps =Rel.toList$ Rel.intransKernel$ Rel.transClosure$ Rel.fromList
               $ getLibDeps oldle
-  ioruplibs <- newIORef ([] :: [LIB_NAME])
-  writeIORef ioruplibs []
-  reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
-  unlockGlobal gInfo
-  libs <- readIORef ioruplibs
-  case libs of
-    [] -> GA.showTemporaryMessage actGraphInfo "Reload not needed!"
-    _ -> remakeGraph gInfo
+    ioruplibs <- newIORef ([] :: [LIB_NAME])
+    writeIORef ioruplibs []
+    reloadLibs (intState gInfo) opts libdeps ioruplibs ln
+    unlockGlobal gInfo
+    libs <- readIORef ioruplibs
+    case libs of
+      [] -> GA.showTemporaryMessage actGraphInfo "Reload not needed!"
+      _ -> remakeGraph gInfo
 
 -- | Creates a list of all LIB_NAME pairs, which have a dependency
@@ -199 +174 @@
 
 -- | Reloads a library
-reloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
+reloadLib :: IORef IntState -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
           -> IO ()
-reloadLib iorle opts ioruplibs ln = do
-  mfile <- existsAnSource opts {intype = GuessIn}
+reloadLib iorst opts ioruplibs ln = do
+ ost <- readIORef iorst 
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   mfile <- existsAnSource opts {intype = GuessIn}
            $ rmSuffix $ libNameToFile opts ln
-  case mfile of
+   case mfile of
     Nothing -> return ()
     Just file -> do
-      le <- readIORef iorle
+      let le = i_libEnv ist
       mFunc <- case openlock $ lookupDGraph ln le of
         Just lock -> tryTakeMVar lock
@@ -224 +203 @@
                                      "Reload: Can't set openlock in DevGraph"
             Nothing -> return ()
-          writeIORef iorle $ newle
+          let nwst = ost { i_state = Just ist { 
+                                       i_libEnv = newle } }
+          writeIORef iorst $ nwst
         Nothing ->
           errorDialog "Error" $ "Error when reloading file " ++ show file
 
 -- | Reloads libraries if nessesary
-reloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
+reloadLibs :: IORef IntState -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
            -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
-reloadLibs iorle opts deps ioruplibs ln = do
-  uplibs <- readIORef ioruplibs
-  case elem ln uplibs of
+reloadLibs iorst opts deps ioruplibs ln = do
+ ost <- readIORef iorst
+ case i_state ost of 
+  Nothing -> return False
+  Just ist -> do
+   uplibs <- readIORef ioruplibs
+   case elem ln uplibs of
     True -> return True
     False -> do
       let
         deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
-      res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
+      res <- mapM (reloadLibs iorst opts deps ioruplibs) deps'
       let
         libupdate = foldl (\ u r -> if r then True else u) False res
       case libupdate of
         True -> do
-          reloadLib iorle opts ioruplibs ln
+          reloadLib iorst opts ioruplibs ln
           return True
         False -> do
-          le <- readIORef iorle
-          let
-            newln:_ = filter (ln ==) $ Map.keys le
-          mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
-          case mfile of
-            Nothing -> return False
-            Just file -> do
-              newmt <- getModificationTime file
-              let
+          ost' <- readIORef iorst
+          case i_state ost' of 
+           Nothing -> return False
+           Just ist' -> do
+            let le = i_libEnv ist'
+            let
+             newln:_ = filter (ln ==) $ Map.keys le
+            mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
+            case mfile of
+              Nothing -> return False
+              Just file -> do
+               newmt <- getModificationTime file
+               let
                 libupdate' = (getModTime $ getLIB_ID newln) < newmt
-              case libupdate' of
+               case libupdate' of
                 False -> return False
                 True -> do
-                  reloadLib iorle opts ioruplibs ln
+                  reloadLib iorst opts ioruplibs ln
                   return True
 
 -- | Deletes the old edges and nodes of the Graph and makes new ones
 remakeGraph :: GInfo -> IO ()
-remakeGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                         , gi_LIB_NAME = ln
-                         , gi_GraphInfo = actGraphInfo
+remakeGraph gInfo@(GInfo { gi_GraphInfo = actGraphInfo
                          }) = do
-  le <- readIORef ioRefProofStatus
-  let
-    dgraph = lookupDGraph ln le
-  showNodes gInfo
-  GA.clear actGraphInfo
-  convert actGraphInfo dgraph
-  hideNodes gInfo
+  ost <- readIORef $ intState gInfo
+  case i_state ost of 
+   Nothing -> return ()
+   Just ist -> do
+    let le = i_libEnv ist
+        ln = i_ln ist
+        dgraph = lookupDGraph ln le
+    showNodes gInfo
+    GA.clear actGraphInfo
+    convert actGraphInfo dgraph
+    hideNodes gInfo
 
 -- | Toggles to display internal node names
@@ -301 +292 @@
 -- | hides all unnamed internal nodes that are proven
 hideNodes :: GInfo -> IO ()
-hideNodes (GInfo { libEnvIORef = ioRefProofStatus
-                 , gi_LIB_NAME = ln
-                 , gi_GraphInfo = actGraphInfo
+hideNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
                  }) = do
   hhn <- GA.hasHiddenNodes actGraphInfo
-  case hhn of
-    True ->
-      GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
-    False -> do
-      GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
-      le <- readIORef ioRefProofStatus
-      let dg = lookupDGraph ln le
-          nodes = selectNodesByType dg [DGNodeType
+  ost <- readIORef $ intState gInfo
+  case i_state ost of 
+   Nothing -> return ()
+   Just ist -> do 
+    case hhn of
+     True ->
+       GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
+     False -> do
+       GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
+       let le = i_libEnv ist
+           ln = i_ln ist
+           dg = lookupDGraph ln le
+           nodes = selectNodesByType dg [DGNodeType
                                          {nonRefType = NonRefType
                                            {isProvenCons = True
                                            , isInternalSpec = True}
                                          , isLocallyEmpty = True}]
-          edges = getCompressedEdges dg nodes
-      GA.hideNodes actGraphInfo nodes edges
+           edges = getCompressedEdges dg nodes
+       GA.hideNodes actGraphInfo nodes edges
 
 -- | selects all nodes of a type with outgoing edges
@@ -382 +376 @@
 -- | Let the user select a Node to focus
 focusNode :: GInfo -> IO ()
-focusNode GInfo { libEnvIORef = ioRefProofStatus
-                , gi_LIB_NAME = ln
-                , gi_GraphInfo = grInfo } = do
-  le <- readIORef ioRefProofStatus
-  idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
+focusNode gInfo@(GInfo { gi_GraphInfo = grInfo }) = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let le = i_libEnv ist
+       ln = i_ln ist
+   idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
                     $ labNodesDG $ lookupDGraph ln le
-  selection <- listBox "Select a node to focus"
-    $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
-  case selection of
+   selection <- listBox "Select a node to focus"
+     $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
+   case selection of
     Just idx -> GA.focusNode grInfo $ fst $ idsnodes !! idx
     Nothing -> return ()
 
 translateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
-translateGraph (GInfo {libEnvIORef = ioRefProofStatus,
-                       gi_LIB_NAME = ln,
-                       gi_hetcatsOpts = opts
+translateGraph gInfo@(GInfo { gi_hetcatsOpts = opts
                       }) convGraph showLib = do
-  le <- readIORef ioRefProofStatus
-  openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do 
+   let le = i_libEnv ist
+       ln = i_ln ist
+   openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
 
 showLibGraph :: GInfo -> LibFunc -> IO ()
@@ -431 +431 @@
 
 saveProofStatus :: GInfo -> FilePath -> IO ()
-saveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
-                       , gi_LIB_NAME = ln
-                       , gi_hetcatsOpts = opts
+saveProofStatus gInfo@(GInfo { gi_hetcatsOpts = opts
                        }) file = encapsulateWaitTermAct $ do
-    proofStatus <- readIORef ioRefProofStatus
+  ost <- readIORef $ intState gInfo
+  case i_state ost of 
+   Nothing -> return ()
+   Just ist -> do 
+    let proofStatus = i_libEnv ist
+        ln = i_ln ist
     writeShATermFile file (ln, lookupHistory ln proofStatus)
     putIfVerbose opts 2 $ "Wrote " ++ file
@@ -442 +445 @@
 openProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
                 -> IO ()
-openProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                             , gi_LIB_NAME = ln
-                             , gi_hetcatsOpts = opts
+openProofStatus gInfo@(GInfo { gi_hetcatsOpts = opts
                              }) file convGraph showLib = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+    let ln = i_ln ist
     mh <- readVerbose opts ln file
     case mh of
@@ -462 +468 @@
                 Just dg -> do
                     lockGlobal gInfo
-                    oldEnv <- readIORef ioRefProofStatus
-                    let proofStatus = Map.insert ln
+                    let oldEnv = i_libEnv ist
+                        proofStatus = Map.insert ln
                                       (applyProofHistory h dg) oldEnv
-                    writeIORef ioRefProofStatus proofStatus
+                        nwst = ost { i_state = Just ist {
+                                      i_libEnv = proofStatus } }
+                    writeIORef (intState gInfo) nwst
                     unlockGlobal gInfo
                     gInfo' <- copyGInfo gInfo ln
@@ -475 +483 @@
                     GA.activateGraphWindow actGraphInfo
 
--- | apply a rule of the development graph calculus
+-- | apply a rule of the development graph calculus 
 proofMenu :: GInfo
              -> (LibEnv -> IO (Res.Result LibEnv))
              -> IO ()
-proofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                       , gi_LIB_NAME = ln
-                       , gi_GraphInfo = actGraphInfo
+proofMenu gInfo@(GInfo { gi_GraphInfo = actGraphInfo
                        , gi_hetcatsOpts = hOpts
                        , proofGUIMVar = guiMVar
-                       , globalHist = gHist
                        }) proofFun = do
-  filled <- tryPutMVar guiMVar Nothing
-  if not filled
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let ln = i_ln ist
+   filled <- tryPutMVar guiMVar Nothing
+   if not filled
     then readMVar guiMVar >>=
                   (maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
@@ -497 +507 @@
     else do
       lockGlobal gInfo
-      proofStatus <- readIORef ioRefProofStatus
+      let proofStatus = i_libEnv ist
       putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
       Res.Result ds res <- proofFun proofStatus
@@ -508 +518 @@
           let newGr = lookupDGraph ln newProofStatus
               history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
-          (guHist, grHist) <- takeMVar gHist
           doDump hOpts "PrintHistory" $ do
             putStrLn "History"
             print $ prettyHistory history
-          putMVar gHist
-           (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
+          let lln = map (\x-> [DgCommandChange x]) $ calcGlobalHistory 
+                                                   proofStatus newProofStatus
+              nst = foldl (add2history "dg rule") ost lln 
+      --        (calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
           applyChanges actGraphInfo $ reverse
             $ flatHistory history
-          writeIORef ioRefProofStatus newProofStatus
+          let nwst = nst { i_state = Just ist { i_libEnv=newProofStatus}}
+          writeIORef (intState gInfo) nwst
           unlockGlobal gInfo
           hideShowNames gInfo False
@@ -545 +557 @@
    fetches the theory from a node inside the IO Monad
    (added by KL based on code in getTheoryOfNode) -}
-lookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
+lookupTheoryOfNode :: LibEnv -> LIB_NAME -> Int
                    -> IO (Res.Result (LibEnv, Node, G_theory))
-lookupTheoryOfNode proofStatusRef ln descr = do
-  libEnv <- readIORef proofStatusRef
+lookupTheoryOfNode libEnv ln descr = do
   return $ do
     (libEnv', gth) <- computeTheory True libEnv ln descr
@@ -562 +573 @@
 used by the node menu defined in initializeGraph-}
 getTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
-getTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
-                             , gi_GraphInfo = actGraphInfo
-                             , libEnvIORef = le
+getTheoryOfNode gInfo@(GInfo { gi_GraphInfo = actGraphInfo
                              }) descr dgraph = do
- r <- lookupTheoryOfNode le ln descr
- case r of
-  Res.Result ds res -> do
-    showDiagMess (gi_hetcatsOpts gInfo) ds
-    case res of
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let le = i_libEnv ist
+       ln = i_ln ist
+   r <- lookupTheoryOfNode le ln descr
+   case r of
+    Res.Result ds res -> do
+     showDiagMess (gi_hetcatsOpts gInfo) ds
+     case res of
       (Just (le', n, gth)) -> do
         lockGlobal gInfo
@@ -576 +591 @@
                                  (addHasInHidingWarning dgraph n) gth
         let newGr = lookupDGraph ln le'
-        libEnv <- readIORef le
-        let history = snd $ splitHistory (lookupDGraph ln libEnv) newGr
+        let history = snd $ splitHistory (lookupDGraph ln le) newGr
         applyChanges actGraphInfo $ reverse $ flatHistory history
-        writeIORef le le'
+        let nwst = ost { i_state = Just $ist { i_libEnv = le'} }
+        writeIORef (intState gInfo) nwst
         unlockGlobal gInfo
       _ -> return ()
@@ -587 +602 @@
 translateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
 translateTheoryOfNode
-  gInfo@(GInfo {gi_hetcatsOpts = opts, libEnvIORef = le}) node dgraph = do
-    libEnv <- readIORef le
-    let Res.Result ds mEnv = computeTheory False libEnv (gi_LIB_NAME gInfo) node
+  gInfo@(GInfo {gi_hetcatsOpts = opts}) node dgraph = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+    let libEnv = i_libEnv ist
+        ln = i_ln ist
+        Res.Result ds mEnv = computeTheory False libEnv ln node
     case mEnv of
       Just (_, th@(G_theory lid sign _ sens _)) -> do
@@ -645 +665 @@
 -- | start local theorem proving or consistency checking at a node
 proveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
-proveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                                   , gi_LIB_NAME = ln
-                                   , commandHist = ch }) descr dgraph = do
-  let dgn = labDG dgraph descr
-      libNode = (ln,descr)
-  (dgraph',dgn') <- case hasLock dgn of
+proveAtNode checkCons gInfo descr dgraph = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let ln = i_ln ist
+       le = i_libEnv ist
+       dgn = labDG dgraph descr
+       libNode = (ln,descr)
+   (dgraph',dgn') <- case hasLock dgn of
     True -> return (dgraph, dgn)
     False -> do
       lockGlobal gInfo
-      le <- readIORef ioRefProofStatus
       (dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
-      writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
+      let nwle = Map.insert ln dgraph' le
+          nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
+      writeIORef (intState gInfo) nwst
       unlockGlobal gInfo
       return (dgraph',dgn')
-  locked <- tryLockLocal dgn'
-  case locked of
+   locked <- tryLockLocal dgn'
+   case locked of
     False -> do
       errorDialog "Error" "Proofwindow already open"
     True -> do
       let action = do
-            le <- readIORef ioRefProofStatus
             guiMVar <- newMVar Nothing
             res <- basicInferenceNode checkCons logicGraph libNode ln
-                guiMVar le ch
+                guiMVar le
+            -- add to history ch
             runProveAtNode checkCons gInfo (descr, dgn') res
             unlockLocal dgn'
@@ -685 +710 @@
                -> Res.Result (LibEnv, Res.Result G_theory) -> IO ()
 runProveAtNode checkCons gInfo (v, dgnode) res = case maybeResult res of
-    Just (le, tres) -> do
-        let nodetext = getDGNodeName dgnode ++ " node: " ++ show v
+  Just (le, tres) -> do
+   ost <- readIORef $ intState gInfo
+   case i_state ost of 
+    Nothing -> return ()
+    Just ist -> do
+        let ln = i_ln ist
+            nodetext = getDGNodeName dgnode ++ " node: " ++ show v
         when checkCons $ case maybeResult tres of
           Just gth -> createTextSaveDisplay
@@ -695 +725 @@
               $ unlines $ "could not (re-)construct a model" : map diagString ds
         proofMenu gInfo $ mergeDGNodeLab gInfo
-          (v, labDG (lookupDGraph (gi_LIB_NAME gInfo) le) v)
-    Nothing -> return ()
+          (v, labDG (lookupDGraph ln le) v)
+  Nothing -> return ()
 
 mergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
-mergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
-  let dg = lookupDGraph ln le
-      old_dgn = labDG dg v
-  return $ do
+mergeDGNodeLab gInfo (v, new_dgn) le = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return (Result [] (Just le))
+  Just ist -> do
+   let ln = i_ln ist
+       dg = lookupDGraph ln le
+       old_dgn = labDG dg v
+   return $ do
     theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
     let new_dgn' = old_dgn { dgn_theory = theory }
@@ -723 +758 @@
 -- | check conservativity of the edge
 checkconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
-checkconservativityOfEdge _ gInfo@(GInfo{gi_LIB_NAME = ln,
-                                         gi_GraphInfo = _actGraphInfo,
-                                         libEnvIORef = le})
+checkconservativityOfEdge _ gInfo@(GInfo{ gi_GraphInfo = _actGraphInfo})
                            (Just (source,target,linklab)) = do
-  lockGlobal gInfo
-  libEnv <- readIORef $ libEnvIORef gInfo
-  let libEnv' = case convertToNf ln libEnv target of
-                  Result _ (Just lE) -> lE
-                  _ -> error "checkconservativityOfEdge: convertToNf"
-  let (_, thTar) =
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let ln = i_ln ist
+       libEnv = i_libEnv ist
+   lockGlobal gInfo
+   let libEnv' = case convertToNf ln libEnv target of
+                   Result _ (Just lE) -> lE
+                   _ -> error "checkconservativityOfEdge: convertToNf"
+   let (_, thTar) =
         case computeTheory True libEnv' ln target of
           Res.Result _ (Just th1) -> th1
           _ -> error "checkconservativityOfEdge: computeTheory"
-  G_theory lid _sign _ sensTar _ <- return thTar
-  GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
-  Just (GMorphism cid' _ _ morphism3 _) <- return $
+   G_theory lid _sign _ sensTar _ <- return thTar
+   GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
+   Just (GMorphism cid' _ _ morphism3 _) <- return $
                   dgn_sigma $ labDG (lookupDGraph ln libEnv') target
-  morphism2' <- coerceMorphism (targetLogic cid) lid
+   morphism2' <- coerceMorphism (targetLogic cid) lid
                 "checkconservativityOfEdge2" morphism2
-  morphism3' <- coerceMorphism (targetLogic cid') lid
+   morphism3' <- coerceMorphism (targetLogic cid') lid
                 "checkconservativityOfEdge3" morphism3
-  let compMor = case comp morphism2' morphism3' of
-               Res.Result _ (Just phi) -> phi
-               _ -> error "checkconservativtiyOfEdge: comp"
-  let (_le', thSrc) =
-        case computeTheory False libEnv' (gi_LIB_NAME gInfo) source of
+   let compMor = case comp morphism2' morphism3' of
+                Res.Result _ (Just phi) -> phi
+                _ -> error "checkconservativtiyOfEdge: comp"
+   let (_le', thSrc) =
+        case computeTheory False libEnv' ln source of
           Res.Result _ (Just th1) -> th1
           _ -> error "checkconservativityOfEdge: computeTheory"
-  G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
-  sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
-  sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
-  let transSensSrc = propagateErrors
+   G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
+   sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
+   sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
+   let transSensSrc = propagateErrors
         $ mapThSensValueM (map_sen lid compMor) sensSrc2
-  if length (conservativityCheck lid) < 1
-   then
+   if length (conservativityCheck lid) < 1
+    then
        do
         infoDialog "Result of conservativity check"
                    "No conservativity checkers available"
-        writeIORef le libEnv'
+        let nwst = ost {i_state = Just $ist{ i_libEnv=libEnv'}}
+        writeIORef (intState gInfo) nwst
         unlockGlobal gInfo
-   else
-    do
-     checkerR <- conservativityChoser $ conservativityCheck lid
-     if Res.hasErrors $ Res.diags checkerR
-      then
-       do
-        infoDialog "Result of conservativity check"
-                   "No conservativity checker chosen"
-        writeIORef le libEnv'
-        unlockGlobal gInfo
-      else
-       do
-        let chCons =  checkConservativity $
-                      maybe (error "checkconservativityOfEdge4") id
-                            $ Res.maybeResult $ checkerR
-        let Res.Result ds res =
-                chCons
-                   (plainSign sign2, toNamedList sensSrc2)
-                   compMor $ toNamedList
-                               (sensTar `OMap.difference` transSensSrc)
-            showObls [] = ""
-            showObls obls = ", provided that the following proof obligations "
+    else
+     do
+      checkerR <- conservativityChoser $ conservativityCheck lid
+      if Res.hasErrors $ Res.diags checkerR
+       then
+        do
+         infoDialog "Result of conservativity check"
+                    "No conservativity checker chosen"
+         let nwst = ost {i_state = Just $ ist { i_libEnv = libEnv'}}
+         writeIORef (intState gInfo) nwst
+         unlockGlobal gInfo
+       else
+        do
+         let chCons =  checkConservativity $
+                       maybe (error "checkconservativityOfEdge4") id
+                             $ Res.maybeResult $ checkerR
+         let Res.Result ds res =
+                 chCons
+                    (plainSign sign2, toNamedList sensSrc2)
+                    compMor $ toNamedList
+                                (sensTar `OMap.difference` transSensSrc)
+             showObls [] = ""
+             showObls obls= ", provided that the following proof obligations "
                             ++ "can be discharged:\n"
                             ++ concatMap (flip showDoc "\n") obls
-            showRes = case res of
+             showRes = case res of
                        Just (Just (cst, obls)) -> "The link is "
                         ++ showConsistencyStatus cst ++ showObls obls
                        _ -> "Could not determine whether link is conservative"
-            myDiags = showRelDiags 2 ds
-        createTextDisplay "Result of conservativity check"
-                        (showRes ++ "\n" ++ myDiags)
-        let
+             myDiags = showRelDiags 2 ds
+         createTextDisplay "Result of conservativity check"
+                         (showRes ++ "\n" ++ myDiags)
+         let
             consShow = case res of
                         Just (Just (cst, _)) -> cst
@@ -813 +853 @@
             changes = [ DeleteEdge (source,target,linklab)
                       , InsertEdge provenEdge ]
-        let newGr = lookupDGraph ln libEnv'
-            nextGr = changesDGH newGr changes
-            newLibEnv = Map.insert ln
+         let newGr = lookupDGraph ln libEnv'
+             nextGr = changesDGH newGr changes
+             newLibEnv = Map.insert ln
               (groupHistory newGr conservativityRule nextGr) libEnv'
-        -- applyChanges actGraphInfo history
-        writeIORef le newLibEnv
-        unlockGlobal gInfo
+         -- applyChanges actGraphInfo history
+         let nwst = ost { i_state = Just $ ist { i_libEnv = newLibEnv}}
+         writeIORef (intState gInfo) nwst
+         unlockGlobal gInfo
 
 checkconservativityOfEdge descr _ Nothing =
@@ -876 +917 @@
 -- | show library referened by a DGRef node (=node drawn as a box)
 showReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
-showReferencedLibrary descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                                         , gi_LIB_NAME = ln })
+showReferencedLibrary descr gInfo
                       convGraph showLib = do
-  le <- readIORef ioRefProofStatus
-  let refNode =  labDG (lookupDGraph ln le) descr
-      refLibname = if isDGRef refNode then dgn_libname refNode
-                   else error "showReferencedLibrary"
-  case Map.lookup refLibname le of
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let ln = i_ln ist
+       le = i_libEnv ist
+       refNode =  labDG (lookupDGraph ln le) descr
+       refLibname = if isDGRef refNode then dgn_libname refNode
+                    else error "showReferencedLibrary"
+   case Map.lookup refLibname le of
     Just _ -> do
       gInfo' <- copyGInfo gInfo refLibname
@@ -946 +991 @@
                    showDiagMess opts $ diagsSl ++ diagsTrans
                    dg_showGraphAux
-                                   (\gI@(GInfo{libEnvIORef = iorLE}) -> do
-                                     writeIORef iorLE newLibEnv
-                                     convGraph (gI{ gi_LIB_NAME = ln
-                                                  , gi_hetcatsOpts = opts})
+                                   (\gI -> do
+                                     ost <- readIORef $ intState gI
+                                     let nwst = case i_state ost of
+                                                 Nothing -> ost
+                                                 Just ist -> 
+                                                  ost{i_state = Just ist{
+                                                       i_libEnv = newLibEnv,
+                                                       i_ln = ln }}
+                                     writeIORef (intState gI) nwst
+                                     convGraph (gI{ gi_hetcatsOpts = opts})
                                                "translation Graph" showLib)
                  Nothing -> myErrMess $ diagsSl ++ diagsTrans
@@ -972 +1023 @@
             -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
 saveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
-                         , gi_LIB_NAME = ln
                          , gi_hetcatsOpts = opts
                          }) nodemap linkmap = do
-  maybeFilePath <- fileSaveDialog ((rmSuffix $ libNameToFile opts ln) ++ ".udg")
+  ost <- readIORef $ intState gInfo
+  case i_state ost of 
+   Nothing -> return ()
+   Just ist -> do
+    let ln = i_ln ist
+    maybeFilePath <- fileSaveDialog ((rmSuffix $ libNameToFile opts ln) ++ ".udg")
                                   [ ("uDrawGraph",["*.udg"])
                                   , ("All Files", ["*"])] Nothing
-  case maybeFilePath of
-    Just filepath -> do
+    case maybeFilePath of
+     Just filepath -> do
       GA.showTemporaryMessage graphInfo "Converting graph..."
       nstring <- nodes2String gInfo nodemap linkmap
       writeFile filepath nstring
       GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
-    Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
+     Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
 
 -- | Converts the nodes of the graph to String representation
@@ -990 +1045 @@
              -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
              -> IO String
-nodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo
-                          , gi_LIB_NAME = ln
-                          , libEnvIORef = ioRefProofStatus
-                          }) nodemap linkmap = do
-  le <- readIORef ioRefProofStatus
-  nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
-                                 return $ not b)
+nodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo }) nodemap linkmap = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return []
+  Just ist -> do
+   let le = i_libEnv ist
+       ln = i_ln ist
+   nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
+                                  return $ not b)
                     $ labNodesDG $ lookupDGraph ln le
-  nstring <- foldM (\s node -> do
+   nstring <- foldM (\s node -> do
                      s' <- (node2String gInfo nodemap linkmap node)
                      return $ s ++ (if s /= "" then ",\n " else "") ++ s')
                    "" nodes
-  return $ "[" ++ nstring ++ "]"
+   return $ "[" ++ nstring ++ "]"
 
 -- | Converts a node to String representation
@@ -1026 +1083 @@
 links2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
              -> Int -> IO String
-links2String (GInfo { gi_GraphInfo = graphInfo
-                    , gi_LIB_NAME = ln
-                    , libEnvIORef = ioRefProofStatus
+links2String gInfo@(GInfo { gi_GraphInfo = graphInfo
                     })  linkmap nodeid = do
-  le <- readIORef ioRefProofStatus
-  edges <- filterM (\(src,_,edge) -> do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return []
+  Just ist -> do 
+   let ln = i_ln ist
+       le = i_libEnv ist
+   edges <- filterM (\(src,_,edge) -> do
                       let eid = dgl_id edge
                       b <- GA.isHiddenEdge graphInfo eid
                       return $ (not b) && src == nodeid)
                      $ labEdgesDG $ lookupDGraph ln le
-  foldM (\s edge -> do
+   foldM (\s edge -> do
           s' <- link2String linkmap edge
           return $ s ++ (if s /= "" then ",\n   " else "") ++ s') "" edges

trunk/GUI/GraphMenu.hs

@@ -55 +55 @@
 
 import Control.Concurrent.MVar
+
+
+import Interfaces.DataTypes
+import Interfaces.History 
 
 -- | Adds to the DGNodeType list style options for each type
@@ -135 +139 @@
 -- | Creates the graph. Runs makegraph
 createGraph :: GInfo -> String -> ConvFunc -> LibFunc -> IO ()
-createGraph gInfo@(GInfo { gi_LIB_NAME = ln
-                         , gi_GraphInfo = actGraphInfo
+createGraph gInfo@(GInfo { gi_GraphInfo = actGraphInfo
                          , gi_hetcatsOpts = opts
                          }) title convGraph showLib = do
-  let file = rmSuffix (libNameToFile opts ln) ++ prfSuffix
-  deselectEdgeTypes <- newIORef []
-  GA.makegraphExt actGraphInfo
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let ln = i_ln ist 
+       file = rmSuffix (libNameToFile opts ln) ++ prfSuffix
+   deselectEdgeTypes <- newIORef []
+   globMenu <- createGlobalMenu gInfo convGraph showLib deselectEdgeTypes
+   GA.makegraphExt actGraphInfo
                   title
                   (createOpen gInfo file convGraph showLib)
@@ -148 +157 @@
                   (createClose gInfo)
                   (Just (createExit gInfo))
-                  (createGlobalMenu gInfo convGraph showLib deselectEdgeTypes)
+                  globMenu
                   (createNodeTypes gInfo convGraph showLib)
                   (createEdgeTypes gInfo)
@@ -182 +191 @@
 -- | Returns the save-function
 createClose :: GInfo -> IO Bool
-createClose (GInfo { gi_LIB_NAME = ln
-                   , libEnvIORef = ioRefProofStatus
-                   , windowCount = wc
+createClose gInfo@(GInfo { windowCount = wc
                    , exitMVar = exit
                    }) = do
-  le <- readIORef ioRefProofStatus
-  case Map.lookup ln le of
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return False
+  Just ist -> do
+   let le = i_libEnv ist
+       ln = i_ln ist
+   case Map.lookup ln le of
     Just dgraph -> do
       case openlock dgraph of
@@ -199 +211 @@
     Nothing -> error $ "development graph with libname " ++ show ln
                        ++" does not exist"
-  count <- takeMVar wc
-  case count == 1 of
+   count <- takeMVar wc
+   case count == 1 of
     True -> putMVar exit ()
     False -> putMVar wc $ count - 1
-  return True
+   return True
 
 -- | Returns the save-function
@@ -212 +224 @@
 -- | Creates the global menu
 createGlobalMenu :: GInfo -> ConvFunc -> LibFunc -> IORef [String]
-                 -> [GlobalMenu]
-createGlobalMenu gInfo@(GInfo { gi_LIB_NAME = ln
-                              , gi_hetcatsOpts = opts
-                              , commandHist = ch
+                 -> IO [GlobalMenu]
+createGlobalMenu gInfo@(GInfo { gi_hetcatsOpts = opts
 #ifdef GTKGLADE
                               , gi_GraphInfo = gi
@@ -222 +232 @@
                               }) convGraph showLib _ =
 #endif
-  let ral x = runAndLock gInfo x in
-  [GlobalMenu (Menu Nothing
-    [ Button "Undo" $ ral $ undo gInfo True
-    , Button "Redo" $ ral $ undo gInfo False
-    , Button "Reload" $ ral $ reload gInfo
-    , Menu (Just "Unnamed nodes")
+ do 
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return []
+  Just ist -> do
+   let ral x = runAndLock gInfo x 
+       ln = i_ln ist
+   return 
+    [GlobalMenu (Menu Nothing
+     [ Button "Undo" $ ral $ undo gInfo True
+     , Button "Redo" $ ral $ undo gInfo False
+     , Button "Reload" $ ral $ reload gInfo
+     , Menu (Just "Unnamed nodes")
         [ Button "Hide/show names" $ ral $ hideShowNames gInfo True
         , Button "Hide nodes" $ ral $ hideNodes gInfo
         , Button "Show nodes" $ ral $ showNodes gInfo
       ]
-    , Button "Focus node" $ ral $ focusNode gInfo
+     , Button "Focus node" $ ral $ focusNode gInfo
 #ifdef GTKGLADE
-    , Button "Select Linktypes" $ showLinkTypeChoice deselectEdgeTypes
+     , Button "Select Linktypes" $ showLinkTypeChoice deselectEdgeTypes
                                 $ (\ eList -> ral $ do
                                     GA.showAll gi
@@ -241 +258 @@
                                   )
 #endif
-    , Menu (Just "Proofs") $ map (\ (str, cmd) ->
-       Button str $ addMenuItemToHist ch str >>
-                  (ral $ performProofAction gInfo
+     , Menu (Just "Proofs") $ map (\ (str, cmd) ->
+       -- History ? or just some partial history in ch ?
+        Button str $ (ral $ performProofAction gInfo
                   $ proofMenu gInfo $ return . return . cmd ln
                   . Map.map undoRedo))
-       [ ("Automatic", automatic)
-       , ("Global Subsumption", globSubsume)
-       , ("Global Decomposition", globDecomp)
-       , ("Local Inference", localInference)
-       , ("Local Decomposition (merge of rules)", locDecomp)
-       , ("Composition (merge of rules)", composition)
-       , ("Composition - creating new links", compositionCreatingEdges)
-       ] ++
-       [Button "Hide Theorem Shift" $
-               (addMenuItemToHist ch "Hide Theorem Shift") >>
+        [ ("Automatic", automatic)
+        , ("Global Subsumption", globSubsume)
+        , ("Global Decomposition", globDecomp)
+        , ("Local Inference", localInference)
+        , ("Local Decomposition (merge of rules)", locDecomp)
+        , ("Composition (merge of rules)", composition)
+        , ("Composition - creating new links", compositionCreatingEdges)
+        ] ++
+        [Button "Hide Theorem Shift" $
+               -- (addMenuItemToHist ch "Hide Theorem Shift") >>
                (ral $ performProofAction gInfo
                $ proofMenu gInfo $ fmap return . interactiveHideTheoremShift ln)
-       ] ++
-       map (\ (str, cmd) ->
-              Button str $ (addMenuItemToHist ch str) >>
-                  (ral $ performProofAction gInfo
-                  $ proofMenu gInfo $ return . cmd ln))
-       [ ("Theorem Hide Shift", theoremHideShift)
-       , ("Compute Colimit", computeColimit)
-       , ("Compute normal forms", convertNodesToNf)
-       ] ++
-       [ Menu (Just "Flattening") $ map ( \ (str, cmd) ->
-          Button str $ ral $ performProofAction gInfo
-                     $ proofMenu gInfo $ return . cmd)
-             [ ("Importings", libEnv_flattening_imports)
-             , ("Disjoint unions", libEnv_flattening_dunions)
-             , ("Importings and renamings", libEnv_flattening_renamings)
-             , ("Hiding", libEnv_flattening_hiding)
-             , ("Heterogeneity", libEnv_flattening_heterogen)
-             , ("Qualify all names", qualifyLibEnv)]]
-    , Button "Dump LibEnv" $ do
-         le <- readIORef $ libEnvIORef gInfo
-         print $ prettyLibEnv le
-    , Button "Translate Graph" $ ral $ translateGraph gInfo convGraph showLib
-    , Button "Show Logic Graph" $ ral $ showLogicGraph daVinciSort
-    , Button "Show Library Graph" $ ral $ showLibGraph gInfo showLib
-    , Button "Save Graph for uDrawGraph" $ ral
-             $ saveUDGraph gInfo (mapNodeTypes opts) $ mapEdgeTypes opts
-    , Button "Save proof-script" $ ral
-             $ askSaveProofScript (gi_GraphInfo gInfo) ch
-    ])
-  ]
+        ] ++
+        map (\ (str, cmd) ->
+               Button str $ -- (addMenuItemToHist ch str) >>
+                   (ral $ performProofAction gInfo
+                   $ proofMenu gInfo $ return . cmd ln))
+        [ ("Theorem Hide Shift", theoremHideShift)
+        , ("Compute Colimit", computeColimit)
+        , ("Compute normal forms", convertNodesToNf)
+        ] ++
+        [ Menu (Just "Flattening") $ map ( \ (str, cmd) ->
+           Button str $ ral $ performProofAction gInfo
+                      $ proofMenu gInfo $ return . cmd)
+              [ ("Importings", libEnv_flattening_imports)
+              , ("Disjoint unions", libEnv_flattening_dunions)
+              , ("Importings and renamings", libEnv_flattening_renamings)
+              , ("Hiding", libEnv_flattening_hiding)
+              , ("Heterogeneity", libEnv_flattening_heterogen)
+              , ("Qualify all names", qualifyLibEnv)]]
+     , Button "Dump LibEnv" $ do
+          let le = i_libEnv ist
+          print $ prettyLibEnv le
+     , Button "Translate Graph" $ ral $ translateGraph gInfo convGraph showLib
+     , Button "Show Logic Graph" $ ral $ showLogicGraph daVinciSort
+     , Button "Show Library Graph" $ ral $ showLibGraph gInfo showLib
+     , Button "Save Graph for uDrawGraph" $ ral
+              $ saveUDGraph gInfo (mapNodeTypes opts) $ mapEdgeTypes opts
+--     , Button "Save proof-script" $ ral
+--              $ askSaveProofScript (gi_GraphInfo gInfo) ch
+     ])
+    ]
 
 -- | A list of all Node Types
@@ -383 +400 @@
                     (Button title
                       (\ (_, descr) ->
-                        do le <- readIORef $ libEnvIORef gInfo
-                           let dGraph = lookupDGraph (gi_LIB_NAME gInfo) le
+                        do 
+                         ost <- readIORef $ intState gInfo
+                         case i_state ost of 
+                          Nothing -> return ()
+                          Just ist -> do 
+                           let le = i_libEnv ist
+                               ln = i_ln ist
+                               dGraph = lookupDGraph ln le
                            runAndLock gInfo $  menuFun descr dGraph
                            return ()
@@ -403 +426 @@
 -}
 createLocalMenuTaxonomy :: GInfo -> ButtonMenu GA.NodeValue
-createLocalMenuTaxonomy ginfo@(GInfo { gi_LIB_NAME = ln
-                                     , libEnvIORef = le }) =
+createLocalMenuTaxonomy ginfo =
   (Menu (Just "Taxonomy graphs")
         [ createMenuButton "Subsort graph" (passTh displaySubsortGraph) ginfo
@@ -410 +432 @@
         ])
   where passTh displayFun descr _ =
-          do r <- lookupTheoryOfNode le ln descr
+         do 
+          ost <- readIORef $ intState ginfo
+          case i_state ost of 
+           Nothing -> return ()
+           Just ist -> do 
+             let ln = i_ln ist
+                 le = i_libEnv ist
+             r <- lookupTheoryOfNode le ln descr
              case r of
                Res.Result [] (Just (_le',n, gth)) ->

trunk/GUI/GraphTypes.hs

@@ -28 +28 @@
 import GUI.GraphAbstraction(GraphInfo, initgraphs)
 import GUI.ProofManagement (GUIMVar)
-import GUI.History(CommandHistory, emptyCommandHistory)
+-- import GUI.History(CommandHistory, emptyCommandHistory)
 import GUI.UDGUtils
 
@@ -42 +42 @@
 
 import Control.Concurrent.MVar
+
+import Interfaces.DataTypes
+import Interfaces.Utils
+
 
 data InternalNames = InternalNames
@@ -51 +55 @@
 data GInfo = GInfo
              { -- Global
-               libEnvIORef :: IORef LibEnv
+               intState :: IORef IntState
+--               libEnvIORef :: IORef LibEnv
              , gi_hetcatsOpts :: HetcatsOpts
              , windowCount :: MVar Integer
              , exitMVar :: MVar ()
              , globalLock :: MVar ()
-             , globalHist :: MVar ([[LIB_NAME]],[[LIB_NAME]])
-             , commandHist :: CommandHistory
+--             , globalHist :: MVar ([[LIB_NAME]],[[LIB_NAME]])
+--             , commandHist :: CommandHistory
              , functionLock :: MVar ()
                -- Local
-             , gi_LIB_NAME :: LIB_NAME
+--             , gi_LIB_NAME :: LIB_NAME
              , gi_GraphInfo :: GraphInfo
              , internalNamesIORef :: IORef InternalNames
@@ -94 +99 @@
 emptyGInfo :: IO GInfo
 emptyGInfo = do
-  iorLE <- newIORef emptyLibEnv
+  let ihist = IntHistory { 
+                 undoList = [], 
+                 redoList = [] }
+      istate = emptyIntIState emptyLibEnv $ Lib_id $ Indirect_link 
+                                        "" nullRange "" noTime
+      st = IntState { 
+            i_state = Just istate,
+            i_hist  = ihist }
+  
+  intSt <- newIORef st
+--  iorLE <- newIORef emptyLibEnv
   graphInfo <- initgraphs
   iorIN <- newIORef $ InternalNames False []
@@ -102 +117 @@
   exit <- newEmptyMVar
   wc <- newMVar 0
-  gh <- newMVar ([],[])
-  ch <- emptyCommandHistory
-  return $ GInfo { libEnvIORef = iorLE
-                  , gi_LIB_NAME = Lib_id $ Indirect_link "" nullRange "" noTime
+--  gh <- newMVar ([],[])
+--  ch <- emptyCommandHistory
+  return $ GInfo {
+  --              libEnvIORef = iorLE
+  --             , gi_LIB_NAME = Lib_id $ Indirect_link "" nullRange "" noTime
+                   intState = intSt
                  , gi_GraphInfo = graphInfo
                  , internalNamesIORef = iorIN
@@ -113 +130 @@
                  , exitMVar = exit
                  , globalLock = gl
-                 , globalHist = gh
-                 , commandHist = ch
+  --             , globalHist = gh
+  --             , commandHist = ch
                  , functionLock = fl
                  }
@@ -124 +141 @@
   iorIN <- newIORef $ InternalNames False []
   guiMVar <- newEmptyMVar
-  return $ gInfo { gi_LIB_NAME = newLN
-                 , gi_GraphInfo = graphInfo
+  intSt <- readIORef $ intState gInfo
+  let intSt' = intSt { 
+                i_state = case i_state intSt of 
+                           Nothing -> Nothing
+                           Just st -> Just $ st {
+                                                 i_ln = newLN}
+                    }
+  writeIORef (intState gInfo) $ intSt'
+  return $ gInfo { -- gi_LIB_NAME = newLN
+                   gi_GraphInfo = graphInfo
                  , internalNamesIORef = iorIN
                  , proofGUIMVar = guiMVar

trunk/GUI/History.hs

@@ -149 +149 @@
 -- If at least one goal was proved and the prove is not the same as last time
 -- the prove gets added, otherwise not.
-addProveToHist :: CommandHistory
+addProveToHist :: CommandHistory 
         -> ProofState lid sentence         -- current proofstate
         -> Maybe (G_prover, AnyComorphism) -- possible used translation

trunk/GUI/ShowGraph.hs

@@ -40 +40 @@
 import Control.Concurrent.MVar
 
+import Interfaces.DataTypes
+
 showGraph :: FilePath -> HetcatsOpts ->
              Maybe (LIB_NAME, -- filename
@@ -55 +57 @@
     useHTk -- All messages are displayed in TK dialog windows
     -- from this point on
-    writeIORef (libEnvIORef gInfo) le
-    ch <- (initCommandHistory file)
-    let gInfo' = gInfo { gi_LIB_NAME = ln
-                       , gi_hetcatsOpts = opts
-                       , commandHist = ch
-                       }
+    ost <- readIORef $ intState gInfo
+    let nwst = case i_state ost of 
+                Nothing -> ost
+                Just ist -> ost{ i_state = Just $ ist { i_libEnv = le
+                                                      , i_ln = ln} }
+    writeIORef (intState gInfo) nwst
+--    ch <- (initCommandHistory file)
+    let gInfo' = gInfo { gi_hetcatsOpts = opts     }
     showLibGraph gInfo'
     mShowGraph gInfo' ln

trunk/GUI/ShowLibGraph.hs

@@ -36 +36 @@
 import Control.Concurrent(threadDelay)
 
+import Interfaces.DataTypes
+
 type NodeArcList = ([DaVinciNode LIB_NAME],[DaVinciArc (IO String)])
 
@@ -65 +67 @@
 -- | Reloads all Libraries and the Library Dependency Graph
 reload :: GInfo -> IORef DaVinciGraphTypeSyn -> IORef NodeArcList -> IO()
-reload gInfo@(GInfo {gi_LIB_NAME = ln,
-                     gi_hetcatsOpts = opts
+reload gInfo@(GInfo {gi_hetcatsOpts = opts
                     }) depGRef nodeArcRef = do
-  depG <- readIORef depGRef
-  (nodes', arcs) <- readIORef nodeArcRef
-  let
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do  
+   let ln = i_ln ist
+   depG <- readIORef depGRef
+   (nodes', arcs) <- readIORef nodeArcRef
+   let
     libfile = libNameToFile opts ln
-  m <- anaLib opts { outtypes = [] } libfile
-  case m of
+   m <- anaLib opts { outtypes = [] } libfile
+   case m of
     Nothing -> fail $
       "Error when reloading file '" ++ libfile ++  "'"
@@ -85 +91 @@
 -- | Adds the Librarys and the Dependencies to the Graph
 addNodesAndArcs :: GInfo -> DaVinciGraphTypeSyn -> IORef NodeArcList -> IO ()
-addNodesAndArcs gInfo@(GInfo { libEnvIORef = ioRefProofStatus
-                             , gi_hetcatsOpts = opts}) depG nodeArcRef = do
-  le <- readIORef ioRefProofStatus
-  let
+addNodesAndArcs gInfo@(GInfo { gi_hetcatsOpts = opts}) depG nodeArcRef = do
+ ost <- readIORef $ intState gInfo
+ case i_state ost of 
+  Nothing -> return ()
+  Just ist -> do
+   let 
+    le = i_libEnv ist
     lookup' x y = Map.findWithDefault (error "lookup': node not found") y x
     keys = Map.keys le
@@ -99 +108 @@
                        Color (getColor opts Green True True) $$$
                        emptyNodeTypeParms
-  subNodeType <- newNodeType depG subNodeTypeParms
-  subNodeList <- mapM (newNode depG subNodeType) keys
-  let
+   subNodeType <- newNodeType depG subNodeTypeParms
+   subNodeList <- mapM (newNode depG subNodeType) keys
+   let
     nodes' = Map.fromList $ zip keys subNodeList
     subArcMenu = LocalMenu(UDG.Menu Nothing [])
@@ -108 +117 @@
                       Color (getColor opts Black False False) $$$
                       emptyArcTypeParms
-  subArcType <- newArcType depG subArcTypeParms
-  let
+   subArcType <- newArcType depG subArcTypeParms
+   let
     insertSubArc = \ (node1, node2) -> newArc depG subArcType (return "")
                        (lookup' nodes' node1) (lookup' nodes' node2)
-  subArcList <- mapM insertSubArc $  Rel.toList $ Rel.intransKernel $
+   subArcList <- mapM insertSubArc $  Rel.toList $ Rel.intransKernel $
     Rel.transClosure $ Rel.fromList $ getLibDeps le
-  writeIORef nodeArcRef (subNodeList, subArcList)
+   writeIORef nodeArcRef (subNodeList, subArcList)
 
 mShowGraph :: GInfo -> LIB_NAME -> IO()

trunk/Interfaces/History.hs

@@ -37 +37 @@
 
 
-add2history :: IntState -> String -> [UndoRedoElem] -> IntState
-add2history st name descr
+-- write2Hist :: IORef IntState -> String -> [UndoRedoElem] -> IO()
+-- write2Hist iost name descr
+--  = do 
+--    ost <- readIORef iost 
+--    let nwst = add2history name ost descr
+--    writeIORef iost nwst
+
+add2history :: String -> IntState -> [UndoRedoElem] -> IntState
+add2history name st descr
  = case undoList $ i_hist st of
     [] ->  let nwEl = Int_CmdHistoryDescription {

trunk/PGIP/DataTypesUtils.hs

@@ -61 +61 @@
 add2hist :: [UndoRedoElem] -> CMDL_State ->  CMDL_State
 add2hist descr st
- = let intst = add2history (intState st) [] descr
+ = let intst = add2history [] (intState st)  descr
    in st {
          intState = intst }

trunk/PGIP/DgCommands.hs

@@ -294 +294 @@
                                (n,_) -> selectANode n dgState
                                ) listNodes
-          --      oldH = history state
                 nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
              return $ add2hist [IStateChange $ Just dgState] $
@@ -307 +306 @@
                                           cComorphism = getIdComorphism elems
                                           } }
-               --    history = oldH {
-               --         undoInstances = ([],[]):(undoInstances oldH),
-               --         redoInstances = []},
                    }
 
@@ -332 +328 @@
                            (n,_) -> selectANode n dgState
                            ) lsNodes
-         -- oldH = history state
           nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
                -- ADD TO HISTORY
@@ -343 +338 @@
                                           cComorphism = getIdComorphism elems
                                             } }
-        --      history = oldH {
-        --                 undoInstances= ([],[]):(undoInstances oldH),
-        --                 redoInstances= []
-        --                 },
               }

trunk/Proofs/InferBasic.hs

@@ -51 +51 @@
 import GUI.Utils
 import GUI.ProofManagement
-import GUI.History(CommandHistory, addProveToHist)
+-- import GUI.History(CommandHistory, addProveToHist)
 
 import qualified Common.Lib.Graph as Tree
@@ -153 +153 @@
 basicInferenceNode :: Bool -- ^ True = CheckConsistency; False = Prove
                    -> LogicGraph -> (LIB_NAME,Node) -> LIB_NAME
-                   -> GUIMVar -> LibEnv -> CommandHistory
+                   -> GUIMVar -> LibEnv 
+                   -- -> CommandHistory
                    -> IO (Result (LibEnv, Result G_theory))
-basicInferenceNode checkCons lg (ln, node) libname guiMVar libEnv ch = do
+basicInferenceNode checkCons lg (ln, node) libname guiMVar libEnv 
+ -- ch 
+ = do
       let dGraph = lookupDGraph libname libEnv
       runResultT $ do
@@ -211 +214 @@
             newTh <- ResultT $
                    proofManagementGUI lid1 ProofActions {
-                       proveF = (proveKnownPMap lg ch freedefs),
-                       fineGrainedSelectionF = (proveFineGrainedSelect lg ch freedefs),
+                       proveF = (proveKnownPMap lg freedefs),
+                       fineGrainedSelectionF = (proveFineGrainedSelect lg  freedefs),
                        recalculateSublogicF  =
                                      recalculateSublogicAndSelectedTheory }
@@ -238 +241 @@
                    -> (LIB_NAME,Node)
                    -> GUIMVar
-                   -> CommandHistory
+                   -- -> CommandHistory
                    -> LibEnv
                    -> IO (Result (LibEnv, Result G_theory))
-basicInferenceSubTree checkCons lg (ln, node) guiMVar ch libEnv = do
+basicInferenceSubTree checkCons lg (ln, node) guiMVar libEnv = do
       let dGraph = lookupDGraph ln libEnv
       runResultT $ do
@@ -308 +311 @@
             newTh <- ResultT $
                    proofManagementGUI lid1 ProofActions {
-                       proveF = (proveKnownPMap lg ch freedefs),
-                       fineGrainedSelectionF = (proveFineGrainedSelect lg ch freedefs),
+                       proveF = (proveKnownPMap lg freedefs),
+                       fineGrainedSelectionF = (proveFineGrainedSelect lg freedefs),
                        recalculateSublogicF  =
                                      recalculateSublogicAndSelectedTheory }
@@ -340 +343 @@
                raw_symbol1
                proof_tree1) =>
-       LogicGraph -> CommandHistory
+       LogicGraph 
+       -- -> CommandHistory
     -> [FreeDefMorphism sentence morphism1]
     -> ProofState lid sentence -> IO (Result (ProofState lid sentence))
-proveKnownPMap lg ch freedefs st =
-    maybe (proveFineGrainedSelect lg ch freedefs st)
-          (callProver st ch False freedefs) $
+proveKnownPMap lg  freedefs st =
+    maybe (proveFineGrainedSelect lg freedefs st)
+          (callProver st False freedefs) $
           lookupKnownProver st ProveGUI
 
@@ -359 +363 @@
                proof_tree1) =>
        ProofState lid sentence
-    -> CommandHistory -> Bool -- indicates if a translation was chosen
+    -- -> CommandHistory 
+    -> Bool -- indicates if a translation was chosen
     -> [FreeDefMorphism sentence morphism1]
     -> (G_prover,AnyComorphism) -> IO (Result (ProofState lid sentence))
-callProver st ch trans_chosen freedefs p_cm@(_,acm) =
+callProver st trans_chosen freedefs p_cm@(_,acm) =
        runResultT $ do
         G_theory_with_prover lid th p <- liftR $ prepareForProving st p_cm
@@ -372 +377 @@
         -- lift $ putStrLn $ show ps
         let st' = markProved acm lid ps st
-        lift $ addProveToHist ch st'
-            (if trans_chosen then Just p_cm else Nothing) ps
+--        lift $ addProveToHist ch st'
+--            (if trans_chosen then Just p_cm else Nothing) ps
         return st'
 
@@ -387 +392 @@
                raw_symbol1
                proof_tree1) =>
-       LogicGraph -> CommandHistory
+       LogicGraph -- -> CommandHistory
     -> [FreeDefMorphism sentence morphism1]
     -> ProofState lid sentence -> IO (Result (ProofState lid sentence))
-proveFineGrainedSelect lg ch freedefs st =
+proveFineGrainedSelect lg freedefs st =
     runResultT $ do
        let sl = sublogicOfTheory st
@@ -400 +405 @@
        pr <- selectProver cmsToProvers
        ResultT $ callProver st{lastSublogic = sublogicOfTheory st,
-                               comorphismsToProvers = cmsToProvers} ch True freedefs pr
+                               comorphismsToProvers = cmsToProvers} True freedefs pr