package circusRefine.gui;

/*
 * Projeto : Refine - Ferramenta Educacional para Refinamentos
 *
 * Tipo : TelaObrigacao
 *
 */
//http://forum.java.sun.com/thread.jspa?forumID=57&threadID=604783
import circusRefine.core.ExternalManager;
import circusRefine.core.ObrigacaoProva;
import circusRefine.core.crules.CRulesException;
import circusRefine.core.print.Printer;
import circusRefine.core.print.ops.PrinterOps;
import circusRefine.core.storage.SetandoFormaOP;
import circusRefine.util.CRefineException;
import circusRefine.util.OPTipos;

import java.awt.BorderLayout;
import java.awt.Color;
import java.awt.Font;

import javax.swing.ImageIcon;
import javax.swing.JCheckBoxMenuItem;
import javax.swing.JFileChooser;
import javax.swing.JMenu;
import javax.swing.JMenuItem;
import javax.swing.JOptionPane;
import javax.swing.JPanel;
import javax.swing.JPopupMenu;
import javax.swing.JScrollPane;
import javax.swing.JTable;
import javax.swing.ListSelectionModel;

import java.awt.datatransfer.StringSelection;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.MouseEvent;
import java.awt.event.MouseListener;
import java.io.File;
import java.io.FileOutputStream;
import java.io.IOException;
import java.util.LinkedList;

import javax.swing.event.ListSelectionEvent;
import javax.swing.event.ListSelectionListener;
import javax.swing.table.DefaultTableModel;
import javax.swing.table.TableColumn;

import zb2smt.ZB2SMTUtils;


import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.circus.ast.ActionTransformerPred;
import net.sourceforge.czt.circus.ast.ProcessTransformerPred;
import net.sourceforge.czt.circus.ast.TransformerPred;
import net.sourceforge.czt.session.Markup;
import net.sourceforge.czt.z.ast.Pred;

/**
 * TelaObrigacao � um tipo que representa a tela de obriga��o de prova
 * da ferramenta. Apenas a janela Interna
 */
public class PanelObrigacao extends JPanel {

    /* A lista que contem os objetos*/
    /* List como componente de interface da swing*/
    /**
     *
     */
    private static final long serialVersionUID = 1L;
    /* Atributos relacionados a tabela */
    private String[] colunas;
    private JTable table;
    private DefaultTableModel List;
    private String path = "images/";
    private ExternalManager gerInterface;
    private int quantOp=0;
    public static boolean isOp = false;

    /* Valor que sera substituido por romano e que indica */
    /* Lista de Obrigacoes correntes no programa */
    private LinkedList<ObrigacaoProva> ops;

    /* GUI componentes*/
    private JScrollPane roll;
    /** Refer�ncia para a tela OP*/
    private TelaObrigacao telaOP;
    private final int colunaindex = 0;
    private final int colunastatus = 1;
    private final int colunaimpressao = 2;

    /**
     * Construtor da classe TelaObrigacao.
     *
     * @param gerInterface       Gerenciador de todas as telas do sistema.
     *
     */
    public PanelObrigacao(TelaObrigacao tela, ExternalManager gerInterface, int width, int height) {

        try {
            this.telaOP = tela;
            this.gerInterface = gerInterface;
            this.ops = new LinkedList<ObrigacaoProva>();

            jbInit(width, height);
        } catch (Exception e) {
            e.printStackTrace();
        }
    }

    public String colocarEspacos(int linha) {
        String retorno = "(" + linha + ")";
        for (int i = 0; i < 8 - retorno.length(); i++) {
            retorno = retorno + " ";
        }
        return retorno;
    }

    /**
     * M�todo que inicializa os componentes da tela de obriga��o de prova.
     *
     */
    private void jbInit(int width, int height) throws Exception {

        //Configurando Tabela
        //Inicializando Colunas
        colunas = new String[3];
        colunas[this.colunaimpressao] = this.retornarMensagem("COD0569");
        colunas[this.colunaindex] = "#";
        colunas[this.colunastatus] = "Status";
        Object[][] data = null;

        List = new DefaultTableModel(data, colunas) {

            @Override
            public boolean isCellEditable(int arg0, int arg1) {
                return false;//Torna as celulas nao editaveis
            }
        };
        table = new JTable(List) {
            //  Returning the Class of each column will allow different
            //  renderers to be used based on Class

            public Class getColumnClass(int column) {
                if (column == 0) {
                    return Integer.class;
                } else if (column == 1) {
                    return ImageIcon.class;
                } else {
                    return String.class;
                }
            }
        };

        table.setPreferredScrollableViewportSize(table.getPreferredSize());
        this.setLocation((gerInterface.getTamanhoHorizontal() * 10) / 800, ((gerInterface.getTamanhoVertical() * 318) / 600));
        this.setSize(width, height);
        this.setLayout(new BorderLayout());
        table.setBackground(Color.white);
        table.setForeground(Color.black);
        //Configurando Modo de Sele��o
        table.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
        table.setFont(new Font("CZT", Font.PLAIN, 14));
        table.setColumnSelectionAllowed(false);
        table.setRowSelectionAllowed(true);
        //table.setCellSelectionEnabled(false);
        table.setRowHeight(200);
        table.addMouseListener(new MouseListener() {

            public void mouseClicked(MouseEvent e) {
                table_mouseClicked(e);
            }

            public void mouseEntered(MouseEvent e) {
            }

            public void mouseExited(MouseEvent e) {
            }

            public void mousePressed(MouseEvent e) {
            }

            public void mouseReleased(MouseEvent e) {
            }
        });


        /* ListSelection Model*/
        //Verificando Modo de Sele��o
        ListSelectionModel list = table.getSelectionModel();
        list.addListSelectionListener(new ListSelectionListener() {

            public void valueChanged(ListSelectionEvent e) {
                selecaoDaLeiAplicada(e);
            }
        });

        //Definindo tamanho das colunas
        TableColumn coluna0 = table.getColumnModel().getColumn(0);
        /*
         * antes tinha 3 ao inves do 6
         * parte que aparece o numero de cada op
         */
        coluna0.setMaxWidth((this.getWidth() * 6) / 100);
        coluna0.setPreferredWidth((this.getWidth() * 6) / 100);
        coluna0.setMinWidth((this.getWidth() * 6) / 100);

        TableColumn coluna1 = table.getColumnModel().getColumn(1);
        TableColumn coluna2 = table.getColumnModel().getColumn(2);
        coluna1.setPreferredWidth((this.getWidth() * 10) / 100);
        coluna1.setMinWidth((this.getWidth() * 10) / 100);
        coluna1.setMaxWidth((this.getWidth() * 10) / 100);
        coluna2.setPreferredWidth((this.getWidth() * 88) / 100);
        coluna2.setCellRenderer(new TelaObrigacaoRenderer());

        roll = new JScrollPane(table);
        roll.setLocation(0, 0);
        roll.setSize(this.getWidth(), this.getHeight());

        this.add(roll);


    }

    /**
     * Trata o evento de chamada ou nao de expansao de
     * Obrigacao de Prova.
     * @param e
     */
    protected void table_mouseClicked(MouseEvent e) {
        if (e.getModifiers() == MouseEvent.BUTTON3_MASK) {
            int selection = table.getSelectedRow();
            if (selection > -1) {

                ObrigacaoProva op = getOpSelecionada();
                JPopupMenu popMenu = new JPopupMenu();

                JMenu exibir = new JMenu(this.retornarMensagem("COD0011"));

                /* Adicionar Historico da PO*/
                JMenuItem log = new JMenuItem(this.retornarMensagem("COD0724"));

                log.addActionListener(new ActionListener() {

                    public void actionPerformed(ActionEvent arg0) {
                        exibirPOLog();
                    }
                });

                exibir.add(log);

                /* Verificando possibilidade de efetuar prova Manual*/

                /* Ou seja, se o provador nao conseguir estabelecer,
                 * um resultado definitivo para o predicado*/
                if (!(op.getTipo().equals(OPTipos.OP_CHECADA_TRUE)
                        || op.getTipo().equals(OPTipos.OP_CHECADA_FALSE))) {

                    if (!(op.getTipo().equals(OPTipos.OP_MANUAL_CHECADA_TRUE)
                            || op.getTipo().equals(OPTipos.OP_MANUAL_CHECADA_FALSE))) {

                        if (op.getPredicado() instanceof TransformerPred) {
                            JMenu prova = new JMenu(this.retornarMensagem("COD0732"));

                            JMenuItem iniciarProva = new JMenuItem(this.retornarMensagem("COD0733"));
                            iniciarProva.addActionListener(new ActionListener() {

                                public void actionPerformed(ActionEvent e) {
                                    iniciarSubDesenvolvimento();
                                }
                            });
                            if (!op.getTipo().equals(OPTipos.OP_SENDO_PROVADA)
                                    && !op.getTipo().equals(OPTipos.OP_PROVADA_MULT_DEV)) {
                                prova.add(iniciarProva);
                            } else if (op.getTipo().equals(OPTipos.OP_PROVADA_MULT_DEV)) {
                                JMenuItem continuarProva = new JMenuItem(this.retornarMensagem("ViewProof"));
                                continuarProva.addActionListener(new ActionListener() {

                                    public void actionPerformed(ActionEvent e) {
                                        continarSubDesenvolvimento();
                                        exibirAbaProvada();
                                    }
                                });
                                prova.add(continuarProva);
                            } else {
                                JMenuItem continuarProva = new JMenuItem(this.retornarMensagem("COD0734"));
                                continuarProva.addActionListener(new ActionListener() {

                                    public void actionPerformed(ActionEvent e) {
                                        continarSubDesenvolvimento();
                                    }
                                });
                                prova.add(continuarProva);
                            }

                            popMenu.add(prova);
                        }
                    }


                    JMenu provaManual = new JMenu(this.retornarMensagem("COD0600"));
                    JMenuItem verdade = new JMenuItem(this.retornarMensagem("COD0601"));
                    verdade.addActionListener(new ActionListener() {

                        public void actionPerformed(ActionEvent e) {
                            setarValorVerdade(e);
                            atualizarOPTipo(OPTipos.OP_CHECADA_TRUE);
                            verificarSubDesenvolvimento();
                        }
                    });

                    JMenuItem falso = new JMenuItem(this.retornarMensagem("COD0602"));
                    falso.addActionListener(new ActionListener() {

                        public void actionPerformed(ActionEvent e) {
                            setarValorFalso(e);
                            atualizarOPTipo(OPTipos.OP_CHECADA_FALSE);
                        }
                    });
                    JMenuItem naoChecada = new JMenuItem(this.retornarMensagem("COD0603"));
                    naoChecada.addActionListener(new ActionListener() {

                        public void actionPerformed(ActionEvent e) {
                            setarValorNaoChecado(e);
                            atualizarOPTipo(OPTipos.OP_CHECADA_NRECONHECIDA);
                        }
                    });

                    provaManual.add(verdade);
                    provaManual.add(falso);
                    provaManual.add(naoChecada);

                    popMenu.add(provaManual);
                } else {
                    /* Checando possibilidade de exibicao da OP nos formatos
                     * : Resumido e Expandido*/
                    JCheckBoxMenuItem expandidoValue = null;
                    JCheckBoxMenuItem defaultValue = new JCheckBoxMenuItem();

                    defaultValue.setText(this.retornarMensagem("COD0595"));
                    exibir.add(defaultValue);

                    /* Verifica o estado atual da OP*/
                    boolean estaExpandida = op.estaExtendida();
                    if (estaExpandida) {
                        expandidoValue = new JCheckBoxMenuItem();
                        expandidoValue.setText(this.retornarMensagem("COD0596"));
                        expandidoValue.setSelected(true);
                        defaultValue.setSelected(false);

                        defaultValue.addActionListener(new ActionListener() {

                            public void actionPerformed(ActionEvent e) {
                                atualizarOPImpressao();
                                setarImpressaoDefault(true);

                            }
                        });

                        exibir.add(expandidoValue);
                    } else {
                        defaultValue.setSelected(true);
                        /* Verifica se a Op pode ser Extendida */
                        if (op.podeExtender()) {
                            expandidoValue = new JCheckBoxMenuItem();
                            expandidoValue.setText(this.retornarMensagem("COD0596"));
                            expandidoValue.setSelected(false);
                            expandidoValue.addActionListener(new ActionListener() {

                                public void actionPerformed(ActionEvent e) {
                                    atualizarOPImpressao();
                                    setarImpressaoExtendida(true);

                                }
                            });

                            exibir.add(expandidoValue);
                        }
                    }
                }

                JMenu editar = new JMenu();
                editar.setText(this.retornarMensagem("COD0272"));

                JMenuItem copiar = new JMenuItem(retornarMensagem("COD0631"));

                copiar.addActionListener(new ActionListener() {

                    public void actionPerformed(ActionEvent e) {
                        copiarOPselecionada();
                    }
                });
                editar.add(copiar);


                JMenu gerar = new JMenu(this.retornarMensagem("COD0725"));

                JMenuItem harveyFile = new JMenuItem(this.retornarMensagem("COD0726"));

                harveyFile.addActionListener(new ActionListener() {

                    public void actionPerformed(ActionEvent e) {
                        imprimirPredicado();
                    }
                });

                JMenuItem smtPureFile = new JMenuItem(this.retornarMensagem("COD0731"));

                smtPureFile.addActionListener(new ActionListener() {

                    public void actionPerformed(ActionEvent e) {
                        imprimirPredicadoSMTPuro();
                    }
                });


                gerar.add(harveyFile);
                gerar.add(smtPureFile);


                popMenu.add(exibir);
                popMenu.add(editar);
                popMenu.add(gerar);
                popMenu.show(e.getComponent(), e.getX(), e.getY());
            }
        } else if (e.getModifiers() == MouseEvent.BUTTON1_MASK) {
            this.selecaoDaLeiAplicada(null);
        }
    }

    protected void exibirAbaProvada() {
        this.gerInterface.showProvedTitle();
    }

    /**
     * Verifica se todas as Ops foram provados
     * caso o termo target do subDesenvolvimento
     *
     */
    protected void verificarSubDesenvolvimento() {
        this.gerInterface.verificarSubDevPosSetarOP();
    }

    private class ContinueSubDevelopmentThread extends Thread {

        private ExternalManager externo;
        private ObrigacaoProva op;
        private int idt;

        public ContinueSubDevelopmentThread(ExternalManager ext, int idtx, ObrigacaoProva opx) {
            externo = ext;
            idt = idtx;
            op = opx;
        }

        public void run() {

            try {
                int id;
                id = externo.continuarSubDesenvolvimento(idt, op);
                externo.updateScreen(id);
                externo.finishLoading();
            } catch (CRefineException e) {
                e.setTitleCode("COD0262");
                ErrorDialog errorDialog = new ErrorDialog(this.externo, "",
                        e);
                errorDialog.setVisible(true);
                externo.finishLoading();
                e.printStackTrace();
            } catch (CRulesException e) {
                CRefineException exc = new CRefineException(e, e.getMessage());
                exc.setTitleCode("COD0262");
                ErrorDialog errorDialog = new ErrorDialog(this.externo, path,
                        exc);
                errorDialog.setVisible(true);
                externo.finishLoading();
                e.printStackTrace();
            }


        }
    }

    /**
     * Continua um subdesenvolvimento que esta oculto.
     *
     */
    protected void continarSubDesenvolvimento() {
        int selection = this.table.getSelectedRow();
        int identificador = this.getIdentificadorOP(selection);
        try {
            int estaAberto = estaAbertoSubDev(identificador, getOpSelecionada());
            if (estaAberto == -1) {

                //this.gerInterface.retornarTelaPrincipal().setProgressBar(0);
                //new ContinueSubDevelopmentThread(gerInterface,identificador
                //	, getOpSelecionada()).start();

                int id = gerInterface.continuarSubDesenvolvimento(identificador, getOpSelecionada());
                gerInterface.updateScreen(id);
                this.gerInterface.retornarTelaObrigacao().updateScreen(id);
            } else {
                this.gerInterface.mudarAbaODes(estaAberto);
            }
        } catch (Exception except) {
            CRefineException e = new CRefineException(except, except.getMessage());
            e.setTitleCode("COD0262");
            ErrorDialog errorDialog = new ErrorDialog(this.gerInterface, path,
                    e);
            errorDialog.setVisible(true);
            except.printStackTrace();
        }
    }

    /**
     *
     * @param identificador
     * @param opSelecionada
     * @return -1 indicando se o subdesenvolvimento nao est� aberto e
     * o id do subdesenvolvimento caso contrario
     */
    private int estaAbertoSubDev(int identificador, ObrigacaoProva opSelecionada) {

        return gerInterface.estaAbertoSubDev(identificador, opSelecionada);
    }

    /**
     * Inicia um subdesenvolvimento a partir da Op selecionada.
     *
     */
    protected void iniciarSubDesenvolvimento() {
        setarValorSendoProvada(null);
        atualizarOPTipo(OPTipos.OP_SENDO_PROVADA);
        int selection = this.table.getSelectedRow();
        int identificador = this.getIdentificadorOP(selection);
        String nomeDes = gerInterface.getDevelopmentName();
        int id = gerInterface.iniciarSubDesenvolvimento(getOpSelecionada(), identificador, nomeDes);
        gerInterface.updateScreen(id);
    }

    /**
     *
     * @param selection a linha de sele��o da OP no panel
     * @return O identificador de uma OP na lista de Obrigacoes de Prova
     */
    private int getIdentificadorOP(int selection) {
        int vidas = selection;
        int op = 0;
        while (op < ops.size() && vidas > 0) {
            if (podeExibir(ops.get(op))) {
                vidas--;
            } else {
                selection++;
            }
            op++;
        }
        return selection;
    }

    /**
     *@return A Op selecionada considerando os tipos de ops que
     *nao est�o sendo exibidos
     */
    private ObrigacaoProva getOpSelecionada() {
        int selection = table.getSelectedRow();
        LinkedList<ObrigacaoProva> opsCopia = new LinkedList<ObrigacaoProva>();
        for (ObrigacaoProva op : ops) {
            if (podeExibir(op)) {
                opsCopia.add(op);
            }
        }
        return opsCopia.get(selection);
    }

    /**
     * Realiza a impressao do arquivo SMT Puro correspondente a
     * OP selecionado
     */
    protected void imprimirPredicadoSMTPuro() {
        Pred pred = ops.get(table.getSelectedRow()).getPredicado();
        StringBuffer body = ZB2SMTUtils.generatePureSMTText(pred);
        /* Criacao do Arquivo*/
        criandoArquivoSMT(body);
    }

    /**
     * Atualiza a impressao da OP selecionada mudando a do valor original.
     *
     */
    protected void atualizarOPImpressao() {
        ObrigacaoProva op = ops.get(table.getSelectedRow());
        String texto = "";
        if (op.estaExtendida()) {
            // setar pro valor defautl
            String[] str = (String[]) Printer.print(op.getPredicado(), gerInterface.getMark(), false);
            for (int i = 0; i < str.length; i++) {
                texto = str[i] + "\n";
            }

        } else {
            //setar pro valor extendido
            String[] str = (String[]) Printer.print(op.getExtendido(), gerInterface.getMark(), false);
            for (int i = 0; i < str.length; i++) {
                texto = str[i] + "\n";
            }
        }
        List.setValueAt(texto, table.getSelectedRow(), this.colunaimpressao);
    }

    protected void atualizarOPTipo(OPTipos tipo) {
        int selection = table.getSelectedRow();
        if (selection != -1) {
            if (tipo.equals(OPTipos.OP_CHECADA_TRUE)) {
                List.setValueAt(new ImageIcon(path + "maotrue.gif"), selection, this.colunastatus);
            } else if (tipo.equals(OPTipos.OP_CHECADA_FALSE)) {
                List.setValueAt(new ImageIcon(path + "maofalse.gif"), selection, this.colunastatus);
            } else if (tipo.equals(OPTipos.OP_SENDO_PROVADA)) {
                List.setValueAt(new ImageIcon(path + "work2.gif"), selection, this.colunastatus);
            } else {
                List.setValueAt(new ImageIcon(path + "inter.gif"), selection, this.colunastatus);
            }
        }
    }

    protected void atualizarOPTipo(int indiceOP) {

        if (indiceOP != -1) {
            OPTipos tipo = ops.get(indiceOP).getTipo();
            if (tipo.equals(OPTipos.OP_CHECADA_TRUE) || tipo.equals(OPTipos.OP_PROVADA_MULT_DEV)) {
                List.setValueAt(new ImageIcon(path + "true.gif"), indiceOP, this.colunastatus);
            } else if (tipo.equals(OPTipos.OP_CHECADA_FALSE)) {
                List.setValueAt(new ImageIcon(path + "false.gif"), indiceOP, this.colunastatus);
            } else if (tipo.equals(OPTipos.OP_MANUAL_CHECADA_TRUE)) {
                List.setValueAt(new ImageIcon(path + "maotrue.gif"), indiceOP, this.colunastatus);
            } else if (tipo.equals(OPTipos.OP_MANUAL_CHECADA_FALSE)) {
                List.setValueAt(new ImageIcon(path + "maofalse.gif"), indiceOP, this.colunastatus);
            } else if (tipo.equals(OPTipos.OP_SENDO_PROVADA)) {
                List.setValueAt(new ImageIcon(path + "work2.gif"), indiceOP, this.colunastatus);
            } else {
                List.setValueAt(new ImageIcon(path + "inter.gif"), indiceOP, this.colunastatus);
            }
        }
    }

    /**
     * Metodo que exibi uma janela com o log da PO selecionada
     */
    protected void exibirPOLog() {
        int selection = table.getSelectedRow();
        if (selection > -1) {
            ObrigacaoProva op = ops.get(selection);
            String str = op.getLog().getLog();
            JOptionPane.showMessageDialog(null, str);

        }
    }

    /**
     * Realiza a impressao do arquivo Harvey correspondente a
     * OP selecionado
     */
    protected void imprimirPredicado() {
        Pred pred = ops.get(table.getSelectedRow()).getPredicado();
        StringBuffer body = ZB2SMTUtils.generateVeritText(pred);
        /* Criacao do Arquivo*/
        criandoArquivoSMT(body);

    }

    /**
     * Metodo utilizado para criar arquivo do SMT
     * @param body corpo do arquivo
     * @param cont identificador do arquivo
     * @return String do nome do arquivo
     */
    private void criandoArquivoSMT(StringBuffer body) {
        try {

            JFileChooser fileChooser = new JFileChooser();

            File currentDir = new File(".");
            fileChooser = new JFileChooser(currentDir);
            fileChooser.setMultiSelectionEnabled(false);
            fileChooser.setDialogType(JFileChooser.SAVE_DIALOG);
            fileChooser.setDialogTitle(this.gerInterface.getMessage("COD0727"));
            int choice = fileChooser.showSaveDialog(this);
            File file = fileChooser.getSelectedFile();
            if (file != null && choice == JFileChooser.APPROVE_OPTION) {
                String fileName = file.getPath();
                File output;
                if (fileName.endsWith(".smt")) {
                    output = new File(fileName);
                } else {
                    output = new File(fileName + ".smt");
                }
                FileOutputStream out = new FileOutputStream(output);
                byte[] data = body.toString().getBytes();
                try {
                    out.write(data);
                    out.close();

                    JOptionPane.showMessageDialog(null, this.gerInterface.getMessage("COD0622"), "SMTFileGenerator", JOptionPane.INFORMATION_MESSAGE);

                } catch (IOException except) {
                    CRefineException e = new CRefineException(except, except.getMessage());
                    e.setTitleCode("COD0609");
                    throw e;
                }
            }

        } catch (Exception exception) {
            exception.printStackTrace();
        }
    }

    protected void copiarOPselecionada() {

        int selection = table.getSelectedRow();
        String output = (String) table.getValueAt(selection, colunaimpressao);
        StringSelection data = new StringSelection(output);
        java.awt.Toolkit.getDefaultToolkit().getSystemClipboard().setContents(data, data);

    }

    /**
     * Seta o valor da Obrigacao de Prova selecionada para Nao Checado
     * @param e
     */
    protected void setarValorNaoChecado(ActionEvent e) {
        int selection = table.getSelectedRow();
        if (selection > -1) {
            ObrigacaoProva op = ops.get(selection);
            OPTipos tipoAnterior = op.getTipo();
            op.setTipo(OPTipos.OP_NCHECADA);
            /* Colocando no historico e regulando Pilhas*/
            this.gerInterface.adicionandoSetValorOPHistorico(OPTipos.OP_NCHECADA, tipoAnterior, selection);
        }
    }

    /**
     * Seta o valor da OP selecionada para falso
     * @param e
     */
    protected void setarValorFalso(ActionEvent e) {
        int selection = table.getSelectedRow();
        if (selection > -1) {
            ObrigacaoProva op = ops.get(selection);
            OPTipos tipoAnterior = op.getTipo();
            op.setTipo(OPTipos.OP_MANUAL_CHECADA_FALSE);
            /* Colocando no historico e regulando Pilhas*/
            this.gerInterface.adicionandoSetValorOPHistorico(OPTipos.OP_MANUAL_CHECADA_FALSE, tipoAnterior, selection);
        }
    }

    /**
     * Seta o valor da OP selecionada para true
     * @param e
     */
    protected void setarValorVerdade(ActionEvent e) {
        int selection = table.getSelectedRow();
        if (selection > -1) {

            ObrigacaoProva op = ops.get(selection);
            OPTipos tipoAnterior = op.getTipo();
            op.setTipo(OPTipos.OP_MANUAL_CHECADA_TRUE);

            /* Colocando no historico e regulando Pilhas*/
            this.gerInterface.adicionandoSetValorOPHistorico(OPTipos.OP_MANUAL_CHECADA_TRUE, tipoAnterior, selection);
        }
    }

    /**
     * Seta o valor da OP selecionada para true
     * quando uma obriga��o de prova  provada atrav�s do
     *
     * @param e
     */
    protected void setarValorVerdade(int indiceOp, int pai) {
        if (indiceOp > -1) {

            ObrigacaoProva op = ops.get(indiceOp);
            OPTipos tipoAnterior = op.getTipo();
            op.setTipo(OPTipos.OP_CHECADA_TRUE);

            /* Colocando no historico e regulando Pilhas*/
            this.gerInterface.adicionandoSetValorOPHistorico(pai, OPTipos.OP_CHECADA_TRUE, tipoAnterior, indiceOp);
        }
    }

    /**
     * Seta o valor da OP selecionada para true
     * @param e
     */
    protected void setarValorSendoProvada(ActionEvent e) {
        int selection = table.getSelectedRow();
        if (selection > -1) {

            ObrigacaoProva op = ops.get(selection);
            OPTipos tipoAnterior = op.getTipo();
            op.setTipo(OPTipos.OP_SENDO_PROVADA);

            /* Colocando no historico e regulando Pilhas*/
            this.gerInterface.adicionandoSetValorOPHistorico(OPTipos.OP_SENDO_PROVADA, tipoAnterior, selection);
        }
    }

    /**
     * Metodo que alterna a impressao do predicado para a forma estendida.
     *
     */
    protected void setarImpressaoExtendida(boolean inserirHistorico) {
        int selection = table.getSelectedRow();
        ObrigacaoProva op = ops.get(selection);
        op.setExtendida(true);
        if (inserirHistorico) {
            SetandoFormaOP mudancaForma = new SetandoFormaOP(selection);
            this.gerInterface.adicionandoHistorico(mudancaForma);
        }

    }

    /**
     * Metodo que alterna a impressao do predicado para a forma estendida.
     *
     */
    protected void setarImpressaoExtendida(int selection, boolean inserirHistorico) {
        ObrigacaoProva op = ops.get(selection);
        op.setExtendida(true);
        if (inserirHistorico) {
            SetandoFormaOP mudancaForma = new SetandoFormaOP(selection);
            this.gerInterface.adicionandoHistorico(mudancaForma);
        }

    }

    /**
     * Metodo que alterna a impressao do predicado para a forma padrao
     *
     */
    protected void setarImpressaoDefault(boolean inserirHistorico) {
        int selection = table.getSelectedRow();
        ObrigacaoProva op = ops.get(selection);
        op.setExtendida(false);
        if (inserirHistorico) {
            SetandoFormaOP mudancaForma = new SetandoFormaOP(selection);
            this.gerInterface.adicionandoHistorico(mudancaForma);
        }
    }

    /**
     * Metodo que alterna a impressao do predicado para a forma padrao
     *
     */
    protected void setarImpressaoDefault(int selection, boolean inserirHistorico) {
        ObrigacaoProva op = ops.get(selection);
        op.setExtendida(false);
        if (inserirHistorico) {
            SetandoFormaOP mudancaForma = new SetandoFormaOP(selection);
            this.gerInterface.adicionandoHistorico(mudancaForma);
        }
    }

    /**
     * Metodo que mostra a relacao entre obrigacao e lei aplicada.
     * @param e
     */
    private void selecaoDaLeiAplicada(ListSelectionEvent e) {
        //Verifica Tabela de linha x lei
        //e seleciona a linha de lei que gerou a dada obriga��o
        int selection = table.getSelectedRow();
        if (selection != -1) {
            if (getOpSelecionada() != null) {
                int toSelect = getOpSelecionada().getLinhaLei();
                this.gerInterface.selecionarLinha(toSelect);
                this.gerInterface.normalizarSelecao(toSelect);
            }
        }
    }

    /**
     * M�todo que retorna uma mensagem que ser� impressa na tela, tanto na forma
     * de t�tulo quanto na forma de mensagem de erro.
     *
     * @param codigo     O c�digo da mensagem que ser� retornada.
     *
     * @return           Uma String que representa a mensagem de retorno.
     *
     */
    public String retornarMensagem(String codigo) {
        String mensagem = gerInterface.getMessage(codigo);
        return mensagem;
    }

    /**
     * M�todo que seta as vari�veis da tela de obriga��o com valores de um novo
     * desenvolvimento, que foi restaurado.
     *
     * @param statusTelaObrigacao        Status das variaveis da tela de obriga��o
     *                                   de provas do desenvolvimento que est�
     *                                   sendo carregado.
     *
     */
    /**
     * Metodo utilizada para listas as obriga��es de provas, dado
     * uma sequentList que nada mais � do que uma lista contendo
     * os predicados a serem exibidos.
     */
    public void listarObrigacoes(LinkedList<ObrigacaoProva> obrigs) {
        for (ObrigacaoProva obr : obrigs) {
            this.ops.add(obr);
        }

    }

    private boolean podeExibir(ObrigacaoProva obr) {
        if (obr.getTipo().equals(OPTipos.OP_CHECADA_TRUE)
                || obr.getTipo().equals(OPTipos.OP_PROVADA_MULT_DEV)) {
            return telaOP.isCheckedTrueSelected();
        } else if (obr.getTipo().equals(OPTipos.OP_CHECADA_FALSE)) {
            return telaOP.isCheckedFalseSelected();
        } else if ((obr.getTipo().equals(OPTipos.OP_CHECADA_NRECONHECIDA)
                || (obr.getTipo().equals(OPTipos.OP_NCHECADA)))) {

            return telaOP.isUncheckedSelected();
        } else if ((obr.getTipo().equals(OPTipos.OP_MANUAL_CHECADA_TRUE))) {
            return telaOP.isManualCheckedTrueSelected();
        } else if ((obr.getTipo().equals(OPTipos.OP_MANUAL_CHECADA_FALSE))) {
            return telaOP.isManualCheckedFalseSelected();
        } else if ((obr.getTipo().equals(OPTipos.OP_SENDO_PROVADA))) {
            return telaOP.isProving();
        } else {
            return false;
        }

    }

    /**
     * M�todo que carrega as obriga��es de prova na tela de obriga��o.
     *
     * @param textoObrigacao         As obriga��es de prova da tela obriga��o.
     *
     */
    public void setarTextoTela(java.util.List<String> textoObrigacao,
            OPTipos[] tipos) {

        for (int i = 0; i < textoObrigacao.size(); i++) {
            if ((tipos[i] == OPTipos.OP_CHECADA_TRUE) || (tipos[i] == OPTipos.OP_PROVADA_MULT_DEV)) {
                List.addRow(new Object[]{new Integer(i+1), new ImageIcon(path + "true.gif"), textoObrigacao.get(i)});
            } else if (tipos[i] == OPTipos.OP_CHECADA_FALSE) {
                List.addRow(new Object[]{new Integer(i+1), new ImageIcon(path + "false.gif"), textoObrigacao.get(i)});
            } else if (tipos[i].equals(OPTipos.OP_MANUAL_CHECADA_TRUE)) {
                List.addRow(new Object[]{new Integer(i+1), new ImageIcon(path + "maotrue.gif"), textoObrigacao.get(i)});
            } else if (tipos[i].equals(OPTipos.OP_MANUAL_CHECADA_FALSE)) {
                List.addRow(new Object[]{new Integer(i+1), new ImageIcon(path + "maofalse.gif"), textoObrigacao.get(i)});
            } else if (tipos[i].equals(OPTipos.OP_SENDO_PROVADA)) {
                List.addRow(new Object[]{new Integer(i+1), new ImageIcon(path + "work2.gif"), textoObrigacao.get(i)});
            } else {
                List.addRow(new Object[]{new Integer(i+1), new ImageIcon(path + "inter.gif"), textoObrigacao.get(i)});
            }
        }
    }

    /**
     * Substitui o texto da lista de obrigacoes de prova. Utilizado
     * no metodo de abertura de arquivos.
     *
     * @param textoNovo a nova lista de <code>String</code>s da
     * 	lista.
     */
    public void substituirTextoTela(java.util.List<String> textoNovo) {
        this.table.removeAll();
        for (String obg : textoNovo) {
            this.List.addRow(new Object[]{new ImageIcon(), obg});
        }

    }

    /**
     * Retira a sele��o, se existir, da tela de obriga��o de provas.
     *
     */
    public void tirarSelecao() {
        int index;
        index = table.getSelectedRow();
        if (index >= 0) {
            table.clearSelection();
        }
    }

    public void desfazer(int quant) {
        while (quant > 0) {
            ops.remove(ops.size() - 1);
            quant--;
        }
        //remove o ultimo predicado que foi inserido
    }

    public LinkedList<ObrigacaoProva> getOps() {
        return ops;
    }

    /**
     *
     * @param tipoSetado valor a ser Setado na OP de indice indiceOP
     * @param indiceOP indice do OP
     * @param insertHistorico determina se deve ocorrer ou nao insercao de passo
     * na lista de historico
     */
    public void setarValorOP(OPTipos tipoSetado, int indiceOP, boolean insertHistorico) {
        ObrigacaoProva op = ops.get(indiceOP);
        OPTipos tipoAnterior = op.getTipo();
        op.setTipo(tipoSetado);
        /* Colocando no historico e regulando Pilhas*/
        if (insertHistorico) {
            this.gerInterface.adicionandoSetValorOPHistorico(tipoSetado, tipoAnterior, indiceOP);
        }
    }

    public void mudarFormatoImpressaoOP(int indiceOP, boolean inserirHistorico) {
        if (ops.get(indiceOP).estaExtendida()) {
            setarImpressaoDefault(indiceOP, inserirHistorico);
        } else {
            setarImpressaoExtendida(indiceOP, inserirHistorico);
        }
    }

    /**
     * Realiza a atualizacao da tela Obrigacao mediante a insercao/remocao das OPS
     * @param mudandoOPExibidas Indica se h� alguma altera��o na exibi��o de tipos de ops
     */
    public void updateScreen(boolean mudandoOPExibidas) {
        /* Insercao ou Remocao*/
        if (List.getRowCount() != ops.size() || mudandoOPExibidas) {
            while (List.getRowCount() != 0) {
                List.removeRow(List.getRowCount() - 1);
            }

            LinkedList<String> strOps = new LinkedList<String>();
           // PrinterOps printer = new PrinterOps(this.gerInterface.getMark(), false);
            Printer printer = new Printer(this.gerInterface.getMark(), false);
            OPTipos[] tipos = new OPTipos[ops.size()];
            int index = 0;
            isOp = true;
            for (int i = 0; i < ops.size(); i++) {
            	System.out.println(i);
            /*	if (i==100  || i==105 || i==121 || i==122 || i==123
            			|| i == 129)
            		System.out.println(i);
            	else*/
            	if (podeExibir(ops.get(i))) {
                    ObrigacaoProva op = ops.get(i);
                    String[] strOP = null;
                    if (op.estaExtendida()) {
                        strOP = (String[]) printer.visitTerm(op.getExtendido());
                    } else {
                        strOP = (String[]) printer.visitTerm(op.getPredicado());
                    }
                    String res = "";
                    for (int k = 0; k < strOP.length; k++) {
                        res += strOP[k] + "\n";
                    }
                    strOps.add(res);
                    tipos[index++] = op.getTipo();
                }
            }
            setarTextoTela(strOps, tipos);
            isOp = false;
        } /*
         * Mudanca Unicode\ Latex
         * Mudanca de Tipo de OP
         * Mudanca de formato
         */ else {
            isOp = true;
            LinkedList<String> strOps = new LinkedList<String>();
            Printer printer = new Printer(this.gerInterface.getMark(), false);
            //PrinterOps printer = new PrinterOps(this.gerInterface.getMark(), false);
            OPTipos tipos[] = new OPTipos[ops.size()];
            int index = 0;
            for (int i = 0; i < ops.size(); i++) {
                ObrigacaoProva op = ops.get(i);
                if (podeExibir(op)) {
                    String[] strOP = null;
                    if (op.estaExtendida()) {
                        strOP = (String[]) printer.visitTerm(op.getExtendido());
                    } else {
                        strOP = (String[]) printer.visitTerm(op.getPredicado());
                    }
                    String res = "";
                    for (int k = 0; k < strOP.length; k++) {
                        res += strOP[k] + "\n";
                    }
                    strOps.add(res);
                    tipos[index++] = op.getTipo();
                }
            }
            alterarCampos(strOps, tipos);
            isOp = false;
        }
    }

    /**
     * Altera o campo de texto das OPs
     * @param strOps
     */
    private void alterarCampos(LinkedList<String> strOps, OPTipos[] tipo) {
        for (int i = 0; i < strOps.size(); i++) {
            List.setValueAt(strOps.get(i), i, this.colunaimpressao);
            if (tipo[i].equals(OPTipos.OP_CHECADA_TRUE)) {
                List.setValueAt(new ImageIcon(path + "true.gif"), i, this.colunastatus);
            } else if (tipo[i].equals(OPTipos.OP_CHECADA_FALSE)) {
                List.setValueAt(new ImageIcon(path + "false.gif"), i, this.colunastatus);
            } else if (tipo[i].equals(OPTipos.OP_MANUAL_CHECADA_TRUE)) {
                List.setValueAt(new ImageIcon(path + "maotrue.gif"), i, this.colunastatus);
            } else if (tipo[i].equals(OPTipos.OP_MANUAL_CHECADA_FALSE)) {
                List.setValueAt(new ImageIcon(path + "maofalse.gif"), i, this.colunastatus);
            } else if (tipo[i].equals(OPTipos.OP_SENDO_PROVADA)) {
                List.setValueAt(new ImageIcon(path + "work2.gif"), i, 1);
            } else {
                List.setValueAt(new ImageIcon(path + "inter.gif"), i, 1);
            }
        }
    }

    /**
     *
     * @return o Identificador da ultima op
     */
    public Integer getIdentificador() {
        return ops.size() - 1;
    }

    /**
     *
     * @param indiceOp
     * @return O termo que representa a AST no momento em que a
     * OP indexada pelo indice indiceOP foi gerado
     */
    public Term getContexto(int indiceOp) {
        return ops.get(indiceOp).getContexto();
    }

    /**
     * M�todo acionado quando a Op indexada pelo indiceOp foi provada.
     * @param indiceOp
     */
    public void opProvada(int pai, int indiceOp) {
        setarValorVerdadeProvado(indiceOp, pai);

        if (!gerInterface.isLoading()) {
            atualizarOPTipo(indiceOp);
            JOptionPane.showMessageDialog(null, this.retornarMensagem("COD0740"), this.retornarMensagem("COD0525"), JOptionPane.INFORMATION_MESSAGE);
        }


    }

    /**
     * Metodo utilizado quando uma OP � chamada;
     * @param indiceOp
     * @param pai
     */
    private void setarValorVerdadeProvado(int indiceOp, int pai) {
        if (indiceOp > -1) {
            ObrigacaoProva op = ops.get(indiceOp);
            this.gerInterface.adicionandoSetValorOPHistorico(OPTipos.OP_MANUAL_CHECADA_TRUE, op.getTipo(), indiceOp);
            op.setTipo(OPTipos.OP_CHECADA_TRUE);
            String msg = this.retornarMensagem("DevelopmentProved");
            op.getLog().insertHistoryStep("-" + msg);

        }
    }

    /**
     *
     * @return True caso todas Ops foram consideradas verdadeiras
     */
    public boolean checkOPs() {
        boolean result = true;
        for (ObrigacaoProva op : ops) {
            if (!(op.getTipo().equals(OPTipos.OP_CHECADA_TRUE)
                    || op.getTipo().equals(OPTipos.OP_MANUAL_CHECADA_TRUE)
                    || op.getTipo().equals(OPTipos.OP_PROVADA_MULT_DEV))) {
                result = false;
                break;
            }
        }

        return result;
    }

    public Term getContextoApos(int indiceOp) {
        return ops.get(indiceOp).getContextoDepois();
    }
}