Copyright	(c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (imports Logic)
Safe Haskell	None

GUI.GraphLogic

Description

This module provides functions for all the menus in the Hets GUI. These are then assembled to the GUI in GUI.GraphMenu.

Synopsis

Documentation

undo :: GInfo -> Bool -> IO ()

Undo one step of the History

updateGraph :: GInfo -> [DGChange] -> IO ()

openProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc -> IO ()

implementation of open menu, read in a proof status

saveProofStatus :: GInfo -> FilePath -> IO ()

proofMenu :: GInfo -> Command -> (LibEnv -> IO (Result LibEnv)) -> IO ()

apply a rule of the development graph calculus

showDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()

show development graph for library

showReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()

show library referened by a DGRef node (=node drawn as a box)

getTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()

outputs the theory of a node in a window; used by the node menu

translateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()

translate the theory of a node in a window; used by the node menu

displaySubsortGraph :: String -> G_theory -> IO ()

displayConceptGraph :: String -> G_theory -> IO ()

showProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()

Show proof status of a node

proveAtNode :: GInfo -> Int -> DGraph -> IO ()

start local theorem proving or consistency checking at a node

ensureLockAtNode :: GInfo -> Int -> DGraph -> IO (Maybe (DGraph, DGNodeLab, LibEnv))

showNodeInfo :: Int -> DGraph -> IO ()

showDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()

showDiagMessAux :: Int -> [Diagnosis] -> IO ()

showEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()

print the id, origin, type, proof-status and morphism of the edge

checkconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()

checkconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()

check conservativity of the edge

toggleHideNames :: GInfo -> IO ()

Toggles to display internal node names

toggleHideNodes :: GInfo -> IO ()

toggleHideEdges :: GInfo -> IO ()

translateGraph :: GInfo -> IO (Maybe LibEnv)

display a window of translated graph with maximal sublogic.

showLibGraph :: GInfo -> LibFunc -> IO ()

runAndLock :: GInfo -> IO () -> IO ()

Locks the global lock and runs function

saveUDGraph :: GInfo -> Map DGNodeType (Shape value, String) -> Map DGEdgeType (EdgePattern EdgeValue, String) -> IO ()

saves the uDrawGraph graph to a file

focusNode :: GInfo -> IO ()

Let the user select a Node to focus

calcGlobalHistory :: LibEnv -> LibEnv -> [LibName]

add2history :: Command -> IntState -> [UndoRedoElem] -> IntState