{- |

Module : ./GUI/GtkAddSentence.hs

Description : Gtk GUI for adding a sentence

Copyright : (c) C. Maeder DFKI GmbH 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable (imports existential types)

This module provides a GUI to add a sentence

-}

module GUI.GtkAddSentence where

import Graphics.UI.Gtk

import Graphics.UI.Gtk.Glade

import GUI.GtkUtils

import qualified GUI.Glade.TextField as TextField

import GUI.GraphTypes

import GUI.GraphLogic

import Interfaces.Utils

import Static.DevGraph

import Static.GTheory

import Static.FromXmlUtils (BasicExtResponse (..), extendByBasicSpec)

import Common.GlobalAnnotations

import Control.Monad

import Data.IORef

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

gtkAddSentence gi n dg = postGUIAsync $ do

xml <- getGladeXML TextField.get

-- get objects

window <- xmlGetWidget xml castToWindow "TextField"

btnAbort <- xmlGetWidget xml castToButton "abort"

btnAdd <- xmlGetWidget xml castToButton "add"

entry <- xmlGetWidget xml castToEntry "entry"

let lbl = labDG dg n

name = getDGNodeName lbl

windowSetTitle window $ "Add sentence to " ++ name

onClicked btnAbort $ widgetDestroy window

onClicked btnAdd $ do

sen <- entryGetText entry

abort <- anaSentence gi (globalAnnos dg) n lbl sen

when abort $ widgetDestroy window

widgetShow window

errorFeedback :: Bool -> String -> IO Bool

errorFeedback abort msg =

errorDialog "Error" msg >> return abort

anaSentence :: GInfo -> GlobalAnnos -> Int -> DGNodeLab -> String -> IO Bool

anaSentence gi ga n lbl sen = case extendByBasicSpec ga sen $ dgn_theory lbl of

(Success gTh num _ sameSig, str)

| not sameSig -> errorFeedback False $ "signature must not change\n" ++ str

| num < 1 -> errorFeedback False "no sentence recognized"

| num > 1 -> errorFeedback False $ "multiple sentences recognized\n" ++ str

| otherwise -> do

addSentence gi n lbl gTh

return True

(Failure b, str) -> errorFeedback b str

addSentence :: GInfo -> Int -> DGNodeLab -> G_theory -> IO ()

addSentence gi n lbl th = do

let ln = libName gi

iSt = intState gi

ost <- readIORef iSt

let (ost', hist) = updateNodeProof ln ost (n, lbl) th

writeIORef iSt ost'

runAndLock gi $ updateGraph gi hist