root/trunk/GUI/GraphDisplay.hs @ 11173

{- |
Module      :  $Header$
Description :  Central GUI for Hets, with display of development graph
Copyright   :  (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic)

Conversion of development graphs from Logic.DevGraph
   to abstract graphs of the graph display interface

A composition table is used when abstracting the graph and composing
multiple edges. It looks like this

@
 [(\"normal\",\"normal\",\"normal\"),
 (\"normal\",\"inclusion\",\"normal\"),
 (\"inclusion\",\"normal\",\"normal\"),
 (\"inclusion\",\"inclusion\",\"inclusion\")]
@

A ginfo can be created with initgraphs. The graph is then created with
addnode and addlink.

-}

module GUI.GraphDisplay
    (convertGraph,initializeConverter)
    where

import Static.DevGraph

import GUI.GraphMenu
import GUI.GraphTypes
import GUI.GraphLogic( convert, applyChanges, hideNodes)
import qualified GUI.GraphAbstraction as GA

import qualified GUI.HTkUtils as HTk

import Data.IORef
import qualified Data.Map as Map(lookup, insert)
import Control.Concurrent.MVar

initializeConverter :: IO (GInfo,HTk.HTk)
initializeConverter = do
  wishInst <- HTk.initHTk [HTk.withdrawMainWin]
  gInfo <- emptyGInfo
  return (gInfo,wishInst)

{- | converts the development graph given by its libname into an
    abstract graph and returns the descriptor of the latter, the
    graphInfo it is contained in and the conversion maps. -}
convertGraph :: ConvFunc
convertGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
                          , gi_GraphInfo = actGraphInfo
                          , gi_LIB_NAME = libname
                          , windowCount = wc
                          }) title showLib = do
  libEnv <- readIORef ioRefProofStatus
  case Map.lookup libname libEnv of
    Just dgraph -> do
      case openlock dgraph of
        Just lock -> do
          notopen <- tryPutMVar lock $ \ hist -> do
            hhn <- GA.hasHiddenNodes actGraphInfo
            case hhn of
              True -> do
                GA.showAll actGraphInfo
                applyChanges actGraphInfo hist
                hideNodes gInfo
              False ->
                applyChanges actGraphInfo hist
            GA.redisplay actGraphInfo
          case notopen of
            True -> do
              count <- takeMVar wc
              putMVar wc $ count + 1
              initializeGraph gInfo title showLib
              if (isEmptyDG dgraph) then return ()
                else do
                  convert actGraphInfo dgraph
                  return ()
            False -> error $ "development graph with libname " ++ show libname
                             ++" is already open"
        Nothing -> do
          lock <- newEmptyMVar
          writeIORef ioRefProofStatus
            $ Map.insert libname dgraph{openlock = Just lock} libEnv
          convertGraph gInfo title showLib
    Nothing -> error $ "development graph with libname " ++ show libname
                       ++" does not exist"

-- | initializes an empty abstract graph with the needed node and edge types,
-- 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)