---

ErrorTrail.java

package gov.nasa.arc.ase.jpf.tools;

import java.awt.*;
import java.io.*;
import java.util.*;
import java.awt.event.*;
import gov.nasa.arc.ase.jpf.*;

public class ErrorTrail
extends Frame
implements WindowListener, ActionListener, KeyListener
{

    // size of internal input and output buffer

    final private int BUFSIZE   = 5000;

    // allocate standard components of MiniEdit as part of initialization:

    TextArea textArea   = new TextArea();

    private String newString    = new String("New");
    private String openString   = new String("Open");
    private String saveString   = new String("Save");
    private String saveAsString = new String("Save As");
    private String quitString   = new String("Quit");

    private File file;

    private String openPrompt   = new String("Open text file");
    private String closePrompt  = new String("Save file as");

    // initialize some state flags

    private boolean neverNamed  = true;
    private boolean dirty       = false;
    private boolean menuBusy    = false;
        
        private Vector errors = new Vector();
        private Vector frames = new Vector();
        private Vector names = new Vector();

        private int index = 0;
        private int current_index = 0;
        boolean is_errorTrail = false;

    // constructor puts together UI

    public ErrorTrail(boolean b, String file_name)
    {
        this.setTitle();
        is_errorTrail = b;
        file = new File(file_name);
        MenuBar mbar = new MenuBar();
        Menu m = new Menu("File");
        m.add(new MenuItem(newString));
        m.add(new MenuItem(openString));
        m.add(new MenuItem(saveString));
        m.add(new MenuItem(saveAsString));
        m.addSeparator();
        m.add(new MenuItem(quitString));    
        m.addActionListener(this);        
        mbar.add(m);
        setMenuBar(mbar);

        textArea.addKeyListener(this);
        add("Center", textArea);

        if(is_errorTrail){
            Button prev_button = new Button("Previous");
            Button next_button = new Button("Next");
            Button quit_button = new Button("Quit");
            Panel button_panel = new Panel();
            button_panel.add(prev_button);
            button_panel.add(quit_button);
            button_panel.add(next_button);
            add("South",button_panel);
            addWindowListener(this);
        }
        
    }
    public boolean action(Event evt, Object arg){
    if(arg.equals("Quit")){
        System.exit(0);
    } else if(arg.equals("Previous")){
        if(index > 0){
        index--;
        current_index -= ((String)errors.elementAt(index)).length();
        textArea.select(current_index, current_index + ((String)errors.elementAt(index)).length());
        parse_error();
        }
    } else if(arg.equals("Next")){
        if(index < errors.size()){
        current_index += ((String)errors.elementAt(index)).length();
        index++;
        textArea.select(current_index, current_index + ((String)errors.elementAt(index)).length());            
        parse_error();
        }
    }
    return true;
    }
    // action handler, part of std java event handling

    public void actionPerformed(ActionEvent evt)
    {
        String cmd = evt.getActionCommand();

        if (cmd.equals(newString))
            {
            newFile();
            }
        else if (cmd.equals(openString))
            {
            openFile();
            }
        else if (cmd.equals(saveString))
            saveFile(false);
        else if (cmd.equals(saveAsString))
            saveFile(true);
        else if (cmd.equals(quitString))
            {
            System.exit(0);
            }
    }
    public void errorSelect(int line_num){
    int counter = 0;
    int index_num = 0;
    while(counter < line_num-1){
        index_num += ((String)errors.elementAt(counter)).length();
        counter++;
    }
    
    textArea.select(index_num, index_num + ((String)errors.elementAt(counter)).length());
    textArea.requestFocus();

    }
    // use FileDialog to get a filepath

    private boolean getFile(int mode)
    {
        String prompt;
        String filename;
        String pathname;

        if (mode == FileDialog.LOAD)
            prompt = openPrompt;
        else
            prompt = closePrompt;

        FileDialog d = new FileDialog(this, prompt, mode);

        if (mode == FileDialog.LOAD)
            d.setFile("*");
        else
            d.setFile(file.getName());

        d.setDirectory(".");
        d.setVisible(true);

        filename = d.getFile(); 

        pathname = d.getDirectory() + filename; 

        if (filename != null)
        {
            file = new File(pathname);
            return(true);
        }
        else
            return(false);
    }
    public void keyPressed(KeyEvent e)
    {
    }
    public void keyReleased(KeyEvent e)
    {
    }
    // pick up keytyped events soley to mark the document as dirty.

    public void keyTyped(KeyEvent e)
    {
    }
    // main declares the MiniEdit frame which does everything

    public static void main(String[] args)
    {

        Frame f = new ErrorTrail(true, "error.trail");
        f.setSize(500, 400);
        f.setVisible(true);  
    }
    // clear out the document

    private void newFile()
    {
    }
    public void openErrorFile(){
    String part;
    StringBuffer all = new StringBuffer("");
    
    try
        {
        FileReader fr = new FileReader(file);
        BufferedReader br=new BufferedReader(fr);
        
        while ( (part=br.readLine()) != null)
            {
            errors.addElement(part+"\n");
            all.append(part);
            all.append('\n');
            }
        
        br.close();
        fr.close();
        this.setTitle("Error Trail");
        textArea.setText(all.toString());
        textArea.select(0, ((String)errors.elementAt(0)).length()); 
        parse_error();
        textArea.requestFocus();
        }   
    catch (IOException e)
        {
        System.out.println("Error - could not read file");
        }
    }
    // call getFile to get a file path, and if you get one open it

    private void openFile()
    {
        String part;
        StringBuffer all = new StringBuffer("");
        int lineNum = 1;
        String highlight ="";

        if (getFile(FileDialog.LOAD))
        {
            try
            {
                FileReader fr = new FileReader(file);
                BufferedReader br=new BufferedReader(fr);

                while ( (part=br.readLine()) != null)
                {
                    if(lineNum == 50) {
                    highlight = part;
                    }
                    all.append(part);
                    all.append('\n');
                    lineNum++;
                }

                br.close();
                fr.close();
                neverNamed = false;
                dirty = false;
                this.setTitle();
                textArea.setText(all.toString());
                int index = textArea.getText().indexOf(highlight);
                textArea.select(index, index+ highlight.length());
            }

            catch (IOException e)
            {
            }
        }

        repaint();
    }
    public void openSrcFile(){
    String part;
    StringBuffer all = new StringBuffer("");
    try
        {
        FileReader fr = new FileReader(file);
        BufferedReader br=new BufferedReader(fr);
        
        while ( (part=br.readLine()) != null)
            {
            errors.addElement(part+"\n");
            all.append(part);
            all.append('\n');
            }

        
        br.close();
        fr.close();
        textArea.setText(all.toString());
        textArea.requestFocus();
        }   
    catch (IOException e)
        {
        System.out.println("Error - could not read file");
        }
    }
    public void parse_error(){

    StringTokenizer command = new StringTokenizer((String)errors.elementAt(index), " ");
    String thread_num = command.nextToken();
    String file_name = command.nextToken();
    String line = command.nextToken();
    line = line.substring(0, line.length()-1);
    int line_num =  Integer.valueOf(line).intValue();
    boolean found = false;
    int i;

    for(i = 0; i < names.size(); ++i){
        if(((String)names.elementAt(i)).equals(file_name)){
        found = true;
        break;
        }
    }

    if(found){
        ((ErrorTrail)frames.elementAt(i)).errorSelect(line_num);
    } else {
        frames.addElement(new ErrorTrail(false, file_name));
        names.addElement(file_name);
        ((ErrorTrail)frames.elementAt(frames.size()-1)).setSize(500, 400);
        ((ErrorTrail)frames.elementAt(frames.size()-1)).setVisible(true);  
        ((ErrorTrail)frames.elementAt(frames.size()-1)).setTitle(file_name);
        ((ErrorTrail)frames.elementAt(frames.size()-1)).openSrcFile();
        ((ErrorTrail)frames.elementAt(frames.size()-1)).errorSelect(line_num);
    }

    }
    // call getFile to get a file path, and if you get one save to it

    private void saveFile(boolean As)
    {
        boolean ok;

        if (neverNamed || As)
        {
            ok = getFile(FileDialog.SAVE);
            neverNamed = false;
        }
        else
            ok = true;

        if (ok)
        {
            String all = textArea.getText();
            try
            {
                FileWriter fw = new FileWriter(file);
                BufferedWriter bw=new BufferedWriter(fw);
                bw.write(all,0,all.length());
                bw.close();
                fw.close();
                this.setTitle();
            }

            catch (IOException e)
            {
            }
        }
        repaint();
    }
    // add current filename to window title

    private void setTitle()
    {
        super.setTitle("ErrorTrail");
    }
    public void windowActivated(WindowEvent event) {
    }
    public void windowClosed(WindowEvent event) {
    }
    public void windowClosing(WindowEvent event) {
    System.exit(0);
    }
    public void windowDeactivated(WindowEvent event) {
    }
    // add the 1.1 WindowListener stuff

    public void windowDeiconified(WindowEvent event) {
    }
    public void windowIconified(WindowEvent event) {
    }
    public void windowOpened(WindowEvent event) {
    if(is_errorTrail)
        openErrorFile();
    }
}

---