{- |

Module :$Header$

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