{- |
Module :./Interfaces/History.hs
Description : history management functions
Copyright : uni-bremen and DFKI
License : GPLv2 or higher, see LICENSE.txt
Maintainer : r.pascanu@jacobs-university.de
Stability : provisional
Portability : portable
Interfaces.History contains different functions that deal
with history
-}
module Interfaces.History
( undoOneStep
, redoOneStep
, undoOneStepWithUpdate
, redoOneStepWithUpdate
, add2history
) where
import Interfaces.DataTypes
import Interfaces.Command
import Common.LibName
import Proofs.AbstractState
import Static.DevGraph
import Static.History
import qualified Data.Map as Map
{- | Datatype used to differentiate between the two actions (so that code does
not get duplicated -}
data UndoOrRedo =
DoUndo
| DoRedo
add2history :: Command -> IntState -> [UndoRedoElem] -> IntState
add2history nm st descr = let
hst = i_hist st
ul = undoList hst
nwEl = CmdHistory
{ command = nm
, cmdHistory = descr }
in st { i_hist = hst { undoList = nwEl : ul } }
-- | Undo or redo a command that modified the development graph
undoRedoDgCmd :: UndoOrRedo -> IntState -> LibName
-> ([DGChange] -> DGraph -> IO ()) -> IO IntState
undoRedoDgCmd actionType state ln update =
case i_state state of
-- should I return an error message??
Nothing -> return state
Just dgS -> do
let
{- take ln from the history storage ??
in contrast to GUI here you operate with only one ln at a time -}
dg = lookupDGraph ln (i_libEnv dgS)
(dg', changes) = ( case actionType of
DoUndo -> undoHistStep
DoRedo -> redoHistStep) dg
newEnv = Map.insert ln dg' (i_libEnv dgS)
newst = state { i_state = Just $ dgS { i_libEnv = newEnv } }
update changes dg'
return newst
{- | Analyze changes to the selected nodes, return new nodes plus a list
of changes that would undo last changes -}
processList :: [ListChange] -> [Int_NodeInfo]
-> [ListChange] -> ([Int_NodeInfo], [ListChange])
processList ls elems acc
= case ls of
-- if nothing to process return elements and changes
[] -> (elems, acc)
x : l ->
-- else check what type of change we are dealing with
case x of
-- if it is a change in axioms
AxiomsChange nwaxms nb ->
-- apply change and store the undo action
let nwls = map (\ y ->
case y of
Element ps nb' ->
if nb' == nb
then (Element ps {includedAxioms = nwaxms} nb
, [AxiomsChange (includedAxioms ps) nb])
else (y, []) ) elems
nwelems = map fst nwls
changesLs = concatMap snd nwls
in processList l nwelems (changesLs ++ acc)
-- if it is a change in goals
GoalsChange nwgls nb ->
-- apply change and store the undo action
let nwls = map (\ y ->
case y of
Element ps nb' ->
if nb' == nb
then (Element ps {selectedGoals = nwgls} nb
, [GoalsChange (selectedGoals ps) nb])
else (y, [])) elems
nwelems = map fst nwls
changeLs = concatMap snd nwls
in processList l nwelems (changeLs ++ acc)
-- if selected nodes change
NodesChange nwelems ->
processList l nwelems (NodesChange elems : acc)
-- | Process one step of undo or redo
processAny :: UndoOrRedo -> IntState
-> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState
processAny actype state update = do
let hst = case actype of
{- find out the list of actions according to the action
(undo/redo) -}
DoUndo -> undoList $ i_hist state
DoRedo -> redoList $ i_hist state
case hst of
[] -> return state
x : l -> do
(nwst, ch) <- processUndoRedoElems actype (cmdHistory x) state [] update
let
x' = x { cmdHistory = ch }
i_hist_state = i_hist state
nwstate = case actype of
DoUndo -> nwst {
i_hist = IntHistory {
undoList = l,
redoList = x' : redoList i_hist_state
}
}
DoRedo -> nwst {
i_hist = IntHistory {
redoList = l,
undoList = x' : undoList i_hist_state
}
}
return nwstate
-- | Process a list of undo or redo changes
processUndoRedoElems :: UndoOrRedo -> [UndoRedoElem] -> IntState
-> [UndoRedoElem]
-> (LibName -> [DGChange] -> DGraph -> IO ())
-> IO (IntState, [UndoRedoElem])
processUndoRedoElems actype ls state acc update
= case i_state state of
Nothing -> return (state, [])
Just ist ->
case ls of
[] -> return (state, acc)
ChShowOutput s : l -> do
let nwst = state {i_state = Just $ ist { showOutput = s}}
ch = ChShowOutput $ showOutput ist
processUndoRedoElems actype l nwst (ch : acc) update
UseThmChange sw : l -> do
let nwst = state { i_state = Just $ ist { useTheorems = sw } }
ch = UseThmChange $ useTheorems ist
processUndoRedoElems actype l nwst (ch : acc) update
Save2FileChange sw : l -> do
let nwst = state { i_state = Just $ ist { save2file = sw } }
ch = Save2FileChange $ save2file ist
processUndoRedoElems actype l nwst (ch : acc) update
ProverChange nwp : l -> do
let nwst = state { i_state = Just $ ist { prover = nwp } }
ch = ProverChange $ prover ist
processUndoRedoElems actype l nwst (ch : acc) update
ConsCheckerChange nwc : l -> do
let nwst = state { i_state = Just $ ist { consChecker = nwc} }
ch = ConsCheckerChange $ consChecker ist
processUndoRedoElems actype l nwst (ch : acc) update
ScriptChange nws : l -> do
let nwst = state { i_state = Just $ ist { script = nws } }
ch = ScriptChange $ script ist
processUndoRedoElems actype l nwst (ch : acc) update
LoadScriptChange sw : l -> do
let nwst = state { i_state = Just $ ist { loadScript = sw } }
ch = LoadScriptChange $ loadScript ist
processUndoRedoElems actype l nwst (ch : acc) update
CComorphismChange nwc : l -> do
let nwst = state { i_state = Just $ ist { cComorphism = nwc} }
ch = CComorphismChange $ cComorphism ist
processUndoRedoElems actype l nwst (ch : acc) update
DgCommandChange nln : l -> do
nwst <- undoRedoDgCmd actype state nln $ update nln
let ch = DgCommandChange nln
processUndoRedoElems actype l nwst (ch : acc) update
ListChange nls : l -> do
let (nwels, lc) = processList nls (elements ist) []
nwst = state { i_state = Just $ ist { elements = nwels } }
ch = ListChange lc
processUndoRedoElems actype l nwst (ch : acc) update
IStateChange nist : l -> do
let nwst = state { i_state = nist }
ch = IStateChange $ Just ist
processUndoRedoElems actype l nwst (ch : acc) update
undoOneStep :: IntState -> IO IntState
undoOneStep ist = processAny DoUndo ist (\ _ _ _ -> return ())
redoOneStep :: IntState -> IO IntState
redoOneStep ist = processAny DoRedo ist (\ _ _ _ -> return ())
undoOneStepWithUpdate :: IntState -> (LibName -> [DGChange] -> DGraph -> IO ())
-> IO IntState
undoOneStepWithUpdate = processAny DoUndo
redoOneStepWithUpdate :: IntState -> (LibName -> [DGChange] -> DGraph -> IO ())
-> IO IntState
redoOneStepWithUpdate = processAny DoRedo