content: {-# 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
  