Index: /trunk/PGIP/DgCommands.hs =================================================================== --- /trunk/PGIP/DgCommands.hs (revision 11082) +++ /trunk/PGIP/DgCommands.hs (revision 11229) @@ -294,5 +294,4 @@ (n,_) -> selectANode n dgState ) listNodes - -- oldH = history state nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState) return $ add2hist [IStateChange $ Just dgState] $ @@ -307,7 +306,4 @@ cComorphism = getIdComorphism elems } } - -- history = oldH { - -- undoInstances = ([],[]):(undoInstances oldH), - -- redoInstances = []}, } @@ -332,5 +328,4 @@ (n,_) -> selectANode n dgState ) lsNodes - -- oldH = history state nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState) -- ADD TO HISTORY @@ -343,7 +338,3 @@ cComorphism = getIdComorphism elems } } - -- history = oldH { - -- undoInstances= ([],[]):(undoInstances oldH), - -- redoInstances= [] - -- }, } Index: /trunk/PGIP/DataTypesUtils.hs =================================================================== --- /trunk/PGIP/DataTypesUtils.hs (revision 11082) +++ /trunk/PGIP/DataTypesUtils.hs (revision 11229) @@ -61,5 +61,5 @@ 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 } Index: /trunk/Proofs/InferBasic.hs =================================================================== --- /trunk/Proofs/InferBasic.hs (revision 11117) +++ /trunk/Proofs/InferBasic.hs (revision 11229) @@ -51,5 +51,5 @@ import GUI.Utils import GUI.ProofManagement -import GUI.History(CommandHistory, addProveToHist) +-- import GUI.History(CommandHistory, addProveToHist) import qualified Common.Lib.Graph as Tree @@ -153,7 +153,10 @@ 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,6 +214,6 @@ 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,8 +241,8 @@ -> (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,6 +311,6 @@ 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,10 +343,11 @@ 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,8 +363,9 @@ 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,6 +377,6 @@ -- 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,8 +392,8 @@ 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,3 +405,3 @@ pr <- selectProver cmsToProvers ResultT $ callProver st{lastSublogic = sublogicOfTheory st, - comorphismsToProvers = cmsToProvers} ch True freedefs pr + comorphismsToProvers = cmsToProvers} True freedefs pr Index: /trunk/GUI/GraphLogic.hs =================================================================== --- /trunk/GUI/GraphLogic.hs (revision 11173) +++ /trunk/GUI/GraphLogic.hs (revision 11229) @@ -107,4 +107,7 @@ import Control.Concurrent.MVar +import Interfaces.History +import Interfaces.DataTypes + -- | Locks the global lock and runs function runAndLock :: GInfo -> IO () -> IO () @@ -127,64 +130,36 @@ -- | 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,13 +174,17 @@ -- | 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,55 +203,67 @@ "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,23 +292,26 @@ -- | 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,23 +376,29 @@ -- | 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,9 +431,12 @@ 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,8 +445,11 @@ 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,8 +468,10 @@ 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,17 +483,19 @@ 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,5 +507,5 @@ 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,13 +518,15 @@ 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,8 +557,7 @@ 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,13 +573,17 @@ 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,8 +591,8 @@ (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,7 +602,12 @@ 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,28 +665,33 @@ -- | 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,6 +710,11 @@ -> 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,12 +725,17 @@ $ 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,76 +758,81 @@ -- | 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,11 +853,12 @@ 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,12 +917,16 @@ -- | 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,8 +991,14 @@ 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,17 +1023,21 @@ -> 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,17 +1045,19 @@ -> 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,15 +1083,18 @@ 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 Index: /trunk/GUI/GraphMenu.hs =================================================================== --- /trunk/GUI/GraphMenu.hs (revision 11173) +++ /trunk/GUI/GraphMenu.hs (revision 11229) @@ -55,4 +55,8 @@ import Control.Concurrent.MVar + + +import Interfaces.DataTypes +import Interfaces.History -- | Adds to the DGNodeType list style options for each type @@ -135,11 +139,16 @@ -- | 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,5 +157,5 @@ (createClose gInfo) (Just (createExit gInfo)) - (createGlobalMenu gInfo convGraph showLib deselectEdgeTypes) + globMenu (createNodeTypes gInfo convGraph showLib) (createEdgeTypes gInfo) @@ -182,11 +191,14 @@ -- | 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,9 +211,9 @@ 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,8 +224,6 @@ -- | 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,17 +232,24 @@ }) 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,51 +258,51 @@ ) #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,6 +400,12 @@ (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,6 +426,5 @@ -} 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,5 +432,12 @@ ]) 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)) -> Index: /trunk/GUI/GraphTypes.hs =================================================================== --- /trunk/GUI/GraphTypes.hs (revision 11173) +++ /trunk/GUI/GraphTypes.hs (revision 11229) @@ -28,5 +28,5 @@ import GUI.GraphAbstraction(GraphInfo, initgraphs) import GUI.ProofManagement (GUIMVar) -import GUI.History(CommandHistory, emptyCommandHistory) +-- import GUI.History(CommandHistory, emptyCommandHistory) import GUI.UDGUtils @@ -42,4 +42,8 @@ import Control.Concurrent.MVar + +import Interfaces.DataTypes +import Interfaces.Utils + data InternalNames = InternalNames @@ -51,14 +55,15 @@ 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,5 +99,15 @@ 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,8 +117,10 @@ 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,6 +130,6 @@ , exitMVar = exit , globalLock = gl - , globalHist = gh - , commandHist = ch + -- , globalHist = gh + -- , commandHist = ch , functionLock = fl } @@ -124,6 +141,14 @@ 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 Index: /trunk/GUI/GraphDisplay.hs =================================================================== --- /trunk/GUI/GraphDisplay.hs (revision 11173) +++ /trunk/GUI/GraphDisplay.hs (revision 11229) @@ -44,4 +44,6 @@ import Control.Concurrent.MVar +import Interfaces.DataTypes + initializeConverter :: IO (GInfo,HTk.HTk) initializeConverter = do @@ -54,11 +56,14 @@ 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,6 +92,7 @@ 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,5 +102,10 @@ -- 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) Index: /trunk/GUI/ShowLibGraph.hs =================================================================== --- /trunk/GUI/ShowLibGraph.hs (revision 11173) +++ /trunk/GUI/ShowLibGraph.hs (revision 11229) @@ -36,4 +36,6 @@ import Control.Concurrent(threadDelay) +import Interfaces.DataTypes + type NodeArcList = ([DaVinciNode LIB_NAME],[DaVinciArc (IO String)]) @@ -65,13 +67,17 @@ -- | 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,8 +91,11 @@ -- | 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,7 +108,7 @@ 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,11 +117,11 @@ 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() Index: /trunk/GUI/History.hs =================================================================== --- /trunk/GUI/History.hs (revision 11173) +++ /trunk/GUI/History.hs (revision 11229) @@ -149,5 +149,5 @@ -- 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 Index: /trunk/GUI/ShowGraph.hs =================================================================== --- /trunk/GUI/ShowGraph.hs (revision 11173) +++ /trunk/GUI/ShowGraph.hs (revision 11229) @@ -40,4 +40,6 @@ import Control.Concurrent.MVar +import Interfaces.DataTypes + showGraph :: FilePath -> HetcatsOpts -> Maybe (LIB_NAME, -- filename @@ -55,10 +57,12 @@ 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 Index: /trunk/Interfaces/History.hs =================================================================== --- /trunk/Interfaces/History.hs (revision 11082) +++ /trunk/Interfaces/History.hs (revision 11229) @@ -37,6 +37,13 @@ -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 {