import java.io.*;
import java.util.*;
import java.net.*;

public class TestServer extends Thread {
      public final static int DEFAULT_PORT=6789;
      protected int port;
      protected ServerSocket listen_socket;

      // Exit with an error message, when an exception occurs.
      public static void fail(Exception e, String msg) {
            System.err.println(msg + ":" + e);
            System.exit(1);
      }

     // Create a ServerSocket to listen for connections on; start the thread.
     public TestServer(int port) {
           if (port == 0) port = DEFAULT_PORT;
           this.port = port;
           try {listen_socket = new ServerSocket(port);}
           catch (IOException e) {fail(e, "Exception creating server socket");}
           System.out.println("Server: listening on port " + port);
           this.start();
     }

     // The body of the server thread.  Loop forever, listening for and
     // accepting connetions from clients.  For each connection.
     // creat a Connection object to handle communication through the
     // new socket.
     public void run() {
           try {
                 while(true) {
                       Socket client_socket = listen_socket.accept();
                       Connection c = new Connection(client_socket);
                 }
           }
           catch (IOException e) {fail(e, "Exception while listening for connetions");}
     }

     // Start the server up, listening on an optionally specified port.
     public static void main(String[] args) {
           int port = 0;
           if (args.length == 1) {
                   try {port = Integer.parseInt(args[0]);}
                   catch (NumberFormatException e) {port = 0;}
           }
           new TestServer(port);
     }
}

// This class is the thread that handles all communication with a client.
class Connection extends Thread {
      protected Socket client;
      protected DataInputStream in;
      protected PrintStream out;
      protected Process child;

      // Initialize the streams and start the thread
      public Connection(Socket client_socket) {
            client = client_socket;
            try {
                  in = new DataInputStream(client.getInputStream());
                  out = new PrintStream(client.getOutputStream());
            }
            catch (IOException e) {
                  try {client.close();} catch (IOException e2) {}
                  System.err.println("Exception while getting socket streams:" + e);
                  return;
            }
            this.start();
      }

      // Provide the service.
      public void run() {
        try {
          String line;
          String objline;
          String score;
          URL scoreURL;
          URLConnection scoreConnection;
          DataInputStream scorein;
          String scoreLine;

          String[] envArray = { "OBJ3-QUIET=" };

	  // start an OBJ process
          Process child = Runtime.getRuntime().exec("/net/cat/disk1/goguen/obj");
          DataInputStream
             objin = new DataInputStream(child.getInputStream());
          DataInputStream
             objerr = new DataInputStream(child.getErrorStream());
          PrintStream
             objout = new PrintStream(
             new BufferedOutputStream(child.getOutputStream(), 1024), true);

          // read a URL for OBJ proof score
          score = in.readLine();

          // read the OBJ proof score into the proof file
          scoreURL = new URL(score);
          scoreConnection = scoreURL.openConnection();
          scorein = new DataInputStream(scoreConnection.getInputStream());

	  // some internal parameters of OBJ3
	  objout.println("evq (setq *obj$prompt* \"\")");
	  objout.println("evq (setq *obj$input_quiet* nil)");
	  objout.println("evq (setq top-level nil)");
//	  objout.println("evq (setq in-in t)");
	  objout.flush();

          for (;;) {
            scoreLine = scorein.readLine();
            if (scoreLine.startsWith("</html>")) break;
            if (! scoreLine.startsWith("<font color=red>"))
              continue;
            if (scoreLine.endsWith("</font>")) {
              objout.println(scoreLine.substring(16,scoreLine.length()-7));
	      objout.flush();
              continue;
            }
            else {
              objout.println(scoreLine.substring(16,scoreLine.length()));
	      objout.flush();
	    }
            for (;;) {
              scoreLine = scorein.readLine();
              if (scoreLine.endsWith("</font>")) {
                objout.println(scoreLine.substring(0,scoreLine.length()-7));
	        objout.flush();
                break;
              }
              else {
	      objout.println(scoreLine);
	      objout.flush();
	      }
            }
          }
	  objout.println("quit");
	  objout.flush();
          // send back results to client
          while ((objline = objin.readLine()) != null) {
          out.println(objline);
	  out.flush(); 
          }
          out.close();
          if (child.waitFor() != 0) throw new Exception();
        } catch (Exception e) {
        } finally {
	  try {
	  client.close();
	  return;
	  } catch (IOException e2) {}
	  try {
	  child.destroy();
	  return;
	  } catch (NullPointerException e3) {}
	}
      }
}