/* This is CondLean's Graphical User Interface source code, written in Java */
/* Importing packages */
import javax.swing.*;
import java.awt.*;
import java.awt.event.*;
import javax.swing.border.*;
import se.sics.jasper.*;
import java.util.HashMap;
import java.io.*;
/* ------------------------------------------------------------------------------------------------- */
/* This class represents a proof tree */
class Tree {
String sequente;
String regola;
String antecedente;
String conseguente;
Tree leftProof;
Tree rightProof;
public Tree (String seq,String reg,String antec,String conseg,Tree left,Tree right){
sequente=new String(seq);
regola=new String(reg);
antecedente=new String(antec);
conseguente=new String(conseg);
leftProof=left;
rightProof=right;
}
public int righeOccupate (){
return calcolaRighe(0);
}
private int calcolaRighe (int branches){
/* We have max 3 branches in a proof tree; in that case, the proof tree needs 3 rows */
if (branches==3) return 3;
else {
/* the sequente is an axiom: heigth=2 */
if (leftProof==null) return 2;
/* the tree has one son; its heigth is 2+son's heigth */
else if (rightProof==null)
return (2+leftProof.calcolaRighe(branches));
/* the tree has two sons 2+max heigth of its sons */
else {
/* the number of branches isincremented */
int leftRows=leftProof.calcolaRighe(branches+1);
int rightRows=rightProof.calcolaRighe(branches+1);
if (leftRows>rightRows) return 2+leftRows;
else return 2+rightRows;
}
}
}
}
/* ------------------------------------------------------------------------------------------------- */
/* This listener instances a graphical window which shows a proof tree */
class ListenerAlberoDiProva implements ActionListener {
private String alberoComeStringa;
private Tree albero;
private SICStus sp;
private String messaggio;
private int dimensione;
private int seqIndici [];
public ListenerAlberoDiProva (SICStus sp, String alberoComeStringa, String msg, int sequenzaIndici [], int dim){
this.alberoComeStringa=alberoComeStringa;
this.sp=sp;
messaggio=msg;
dimensione=dim;
seqIndici=sequenzaIndici;
}
public ListenerAlberoDiProva (Tree t, String msg, int sequenzaIndici [], int dim){
albero=t;
messaggio=msg;
dimensione=dim;
seqIndici=sequenzaIndici;
}
public void actionPerformed (ActionEvent e){
if(albero==null){
System.out.println("");
/* Feedback in the command window */
System.out.println("Building the proof tree: please, wait a while...");
int stima=(int)(alberoComeStringa.length()/400);
System.out.println("Time to elapse: "+Integer.toString(stima)+" seconds");
albero=new OggettiUtili().costruisciAlberoJava(sp,alberoComeStringa,"[]","[]");
System.out.println("Operation completed");
}
int righe=albero.righeOccupate();
Prover p=new Prover(new String(messaggio+" of the sequent: "+new OggettiUtili().eliminaTagHtml(albero.sequente)),righe+1);
p.pack();
p.setVisible(true);
p.paint(albero,1,15,righe-1,seqIndici,dimensione);
}
}
/* ------------------------------------------------------------------------------------------------- */
/* Listener that shows the whole sequent in a box of the control window */
class SeqListener implements ActionListener {
String sequente;
JLabel where;
public SeqListener (String seq, JLabel box){
where=box;
sequente=new String(seq);
}
public void actionPerformed (ActionEvent e){
/* Html tags lets JLabel to show its text with different colrs */
where.setText(""+sequente+"");
}
}
/* ------------------------------------------------------------------------------------------------- */
/* Matrix used to show a proof tree in a special window */
class Bottoniera{
private JButton bottoni [][];
public Bottoniera (int rows, int cols){
int i,j;
bottoni=new JButton [rows][cols];
for (i=0;i')))
if (seqSulBottone.charAt(k)=='>')
htmlTag=false;
else htmlTag=true;
else sulBottone=sulBottone+seqSulBottone.charAt(k);
boolean hoTagliato=false;
if (sulBottone.length()<=(taglio+3)) taglio=sulBottone.length();
else hoTagliato=true;
sulBottone=sulBottone.substring(0,taglio);
if (hoTagliato)
sulBottone=sulBottone+"...";
bottoni[i][j].setFont(new Font("serif",Font.ITALIC,14));
bottoni[i][j].setText(sulBottone);
setListener(i,j,new SeqListener(value,where));
bottoni[i][j].setToolTipText("Click here to see the whole sequent");
}
public void setValueAt (ImageIcon value, int i, int j){
bottoni[i][j].setIcon(value);
bottoni[i][j].setContentAreaFilled(false);
bottoni[i][j].setFocusPainted(false);
bottoni[i][j].setBorder(new LineBorder(Color.lightGray,1));
bottoni[i][j].setMargin(new Insets(1,1,1,1));
}
public void setValueAt (int vettoreIndici [], int dim, int i, int j){
bottoni[i][j].setIcon(new ImageIcon("p.jpg"));
String seqIndici=new String("");
for (int ind=0;ind";
bottoni[i][j].setText(seqIndici);
bottoni[i][j].setVerticalTextPosition(JLabel.BOTTOM);
bottoni[i][j].setHorizontalTextPosition(JLabel.SOUTH_EAST);
bottoni[i][j].setContentAreaFilled(false);
bottoni[i][j].setFocusPainted(false);
bottoni[i][j].setBorder(new LineBorder(Color.lightGray,1));
bottoni[i][j].setMargin(new Insets(1,1,1,1));
}
public JButton getButton (int i, int j){
return (bottoni[i][j]);
}
}
/* ------------------------------------------------------------------------------------------------- */
/* This class is a a grphical window which shows a proof tree */
class Prover extends JFrame{
private Bottoniera screen;
private int sottoprove;
public JLabel box;
public Prover (String titolo,int rows){
super(titolo);
int i,j;
Container cp=getContentPane();
cp.setLayout(new BorderLayout());
screen=new Bottoniera (rows,15);
JPanel panBot=new JPanel();
JScrollPane contScroll=new JScrollPane(panBot);
int dimensioneInRighe=rows*40;
if (dimensioneInRighe>600) dimensioneInRighe=600;
contScroll.setPreferredSize(new Dimension(900,dimensioneInRighe));
cp.add(contScroll,BorderLayout.CENTER);
JPanel pan2=new JPanel();
cp.add(pan2,BorderLayout.SOUTH);
int ind=0;
while(titolo.charAt(ind)!=':')
ind++;
ind=ind+2;
box=new JLabel(""+titolo.substring(ind,titolo.length())+"");
pan2.add(box);
sottoprove=0;
/* Inserting window's buttons */
GridBagLayout gridbag = new GridBagLayout();
GridBagConstraints c = new GridBagConstraints();
panBot.setLayout(gridbag);
c.fill = GridBagConstraints.BOTH;
c.weightx = 1.0;
JButton bott;
for (i=0;i<28;i++){
bott=new JButton();
bott.setBorderPainted(false);
attacca(bott,panBot,gridbag,c);
}
c.gridwidth = GridBagConstraints.REMAINDER;
bott=new JButton();
bott.setBorderPainted(false);
attacca(bott,panBot,gridbag,c);
for (i=0;iInsert a sequent: (ex: [x,a], [x,a=>b] |- [x,a and b])