ProverGUI.hs

{-# LANGUAGE CPP #-}
{- |
Module      :  ./GUI/ProverGUI.hs
Description :  cpp choice between "GUI.ProofManagement" and "GUI.GtkProverGUI"
Copyright   :  (c) C. Maeder, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (cpp)

cpp choice between "GUI.ProofManagement" and "GUI.GtkProverGUI"
-}

module GUI.ProverGUI
  ( proverGUI ) where

import Logic.Comorphism
import Static.GTheory
import Common.Result as Result
import Proofs.AbstractState
import qualified Comorphisms.KnownProvers as KnownProvers

#ifdef GTKGLADE
import GUI.GtkProverGUI
#elif defined UNI_PACKAGE
import Control.Concurrent
import GUI.HTkProverGUI
#endif

proverGUI :: ProofActions -- ^ record of possible GUI actions
  -> String -- ^ theory name
  -> String -- ^ warning information
  -> G_theory -- ^ theory
  -> KnownProvers.KnownProversMap -- ^ map of known provers
  -> [(G_prover, AnyComorphism)]  -- ^ list of suitable provers and comorphisms
  -> IO (Result.Result G_theory)
#ifdef GTKGLADE
proverGUI = showProverGUI
#elif defined UNI_PACKAGE
proverGUI prGuiAcs thName warningTxt th knownProvers comorphList = do
  guiMVar <- newMVar Nothing
  proofManagementGUI prGuiAcs thName warningTxt th knownProvers comorphList
                     guiMVar
#else
proverGUI = error "not implemented"
#endif