package G4ip;

import java.applet.*;
import java.awt.*;
import G4ip.Sequent.*;
import G4ip.Prover.*;
import G4ip.Parser.*;

/** The applet for the prover.
  * @author      Christian Urban
  */
public class ProverApplet extends Applet {
  Prover prover;
  Parser parser;

  Button start;           
  Button clear;           
  Button next;            
  Button stop;           
  TextField lhs_text;     // place for the program formulae
  TextField rhs_text;     // place for the goal formula
  /** A field for various messages (e.g. error messages).
    */
  public Label messages;  // to be verbose   

  public void init() {
    setLayout(new BorderLayout());
    // NORTH
    Panel textfields = new Panel();
    add("North", textfields);
       // the parameters LHS_size and RHS_size are given in the html-file
    int LHS_size = Integer.parseInt(this.getParameter("LHS_size"));
    int RHS_size = Integer.parseInt(this.getParameter("RHS_size"));
    lhs_text = new TextField(LHS_size);    // program textfield
    rhs_text = new TextField(RHS_size);    // goal textfield
    Label separation = new Label("=>");    // for separation

    if (LHS_size > 0) {     // if someone prefears only single side sequents 
    textfields.add(lhs_text);   }         
    textfields.add(separation);
    textfields.add(rhs_text);

    // CENTER
    Panel buttonfield = new Panel();
    add("Center", buttonfield);
    start = new Button("Start");         
    clear = new Button("Clear");         
    next  = new Button("Next");          
    stop  = new Button("Stop");            

    switch_into_input_mode();   // start in input mode
    buttonfield.add(start);
    buttonfield.add(clear);
    buttonfield.add(next);
    buttonfield.add(stop);

    // SOUTH
    messages = new Label("");   // for any kind of message
    messages.setAlignment(Label.CENTER);
    add("South",messages);
  }
  
  /** When start is pressed; 
    * start and clear button are disabled;
    * next and stop button are enabled. 
    */
  public void switch_into_prove_mode() { 
      start.disable();    next.enable();
      clear.disable();    stop.enable();
      repaint();
    }

  /** When start is pressed 
    * and (hopefully) when prover finishes. 
    */  
  public void switch_into_input_mode() { 
      start.enable();    next.disable(); 
      clear.enable();    stop.disable();
      repaint();
    }

  /** Initiates the parse and prove process. 
    */  
  void initiate_proving() {
      Sequent sequ;
      messages.setText(""); 
      messages.repaint();
      repaint(); 
      Parser rhs_parser = new Parser(rhs_text.getText());
      Parser lhs_parser = new Parser(lhs_text.getText());
      try {                          // try to parse the input 
	sequ = new Sequent(lhs_parser.parseFormulae(),
			   rhs_parser.parseFormula());
      }
      catch (Exception exc) {        // there was a parser exception 
	messages.setText(exc.getMessage()); 
	messages.repaint();
	repaint(); 
	return;                     // in case there was an exception
      }                             // don't run the following code
      System.out.println(sequ.G.internalString()); 
      switch_into_prove_mode();
      prover = new Prover(sequ,this);
      prover.start();
  }

  /** Forces the prover to dispose all open frames.
    */
  public void destroy() {  
    if (prover != null && prover.isAlive()) { 
      prover.stop(); 
      prover.finalize();
    }
  }


  /** The actions for the buttons:
    * this bit of code would be different in Java 1.1
    */
  public boolean action(Event e, Object arg) {
    // clear button has been pressed
    if (e.target == clear) {
      messages.setText(""); 
      lhs_text.setText("");
      rhs_text.setText(""); 
      messages.repaint();
      repaint(); 
    }
    // start button has been pressed
    if (e.target == start) {
      initiate_proving();
      return true; 
    }
    // stop button has been pressed
    if (e.target == stop) {
      switch_into_input_mode();
      if (prover != null && prover.isAlive()) { prover.stop();  }
      return true; 
    }
    // next button has been pressed
    if (e.target == next) {
      if (prover != null && prover.isAlive()) { prover.resume();} 
      return true; 
    }
    return false;
  }

}