src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java

just one README.md;

/***************************************************************************
  Title:      graphbrowser/GraphBrowserFrame.java
  Author:     Stefan Berghofer, TU Muenchen
  Options:    :tabSize=2:

  This class is the frame for the stand-alone application. It contains
  methods for handling menubar events.
***************************************************************************/

package isabelle.graphbrowser;

import java.awt.*;
import java.awt.event.*;
import java.io.*;
import isabelle.awt.*;

public class GraphBrowserFrame extends Frame implements ActionListener {
	GraphBrowser gb;
	MenuItem i1, i2;
	String graphDir, psDir;

	public void checkMenuItems() {
		if (gb.isEmpty()) {
			i1.setEnabled(false);
			i2.setEnabled(false);
		} else {
			i1.setEnabled(true);
			i2.setEnabled(true);
		}
	}

	public void actionPerformed(ActionEvent evt) {
		String label = evt.getActionCommand();
		if (label.equals("Quit"))
			System.exit(0);
		else if (label.equals("Export to PostScript")) {
			PS(true, label);
			return;
		} else if (label.equals("Export to EPS")) {
			PS(false, label);
			return;
		} else if (label.equals("Open ...")) {
			FileDialog fd = new FileDialog(this, "Open graph file", FileDialog.LOAD);
			if (graphDir != null)
				fd.setDirectory(graphDir);
			fd.setVisible(true);
			if (fd.getFile() == null) return;
			graphDir = fd.getDirectory();
			String fname = graphDir + fd.getFile();
			GraphBrowser gb2 = new GraphBrowser(fname);
			try {
				InputStream is = new FileInputStream(fname);
				gb2.initBrowser(is, false);
				is.close();
			} catch (IOException exn) {
				String button[] = {"OK"};
				MessageDialog md = new MessageDialog(this, "Error",
					"Can't open file " + fname + ".", button);
				md.setSize(350, 200);
				md.setVisible(true);
				return;
			}
			remove(gb);
			add("Center", gb2);
			gb = gb2;
			checkMenuItems();
			validate();
		}
	}

	public void PS(boolean printable,String label) {
		FileDialog fd=new FileDialog(this,label,FileDialog.SAVE);
		if (psDir!=null)
			fd.setDirectory(psDir);
		fd.setVisible(true);
		if (fd.getFile()==null) return;
		psDir=fd.getDirectory();
		String fname=psDir+fd.getFile();

		if ((new File(fname)).exists()) {
			String buttons[]={"Overwrite","Cancel"};
			MessageDialog md=new MessageDialog(this,"Warning",
			      "Warning: File "+fname+" already exists. Overwrite?",
			      buttons);
			md.setSize(350,200);
			md.setVisible(true);
			if (md.getText().equals("Cancel")) return;
		}

		try {
			gb.PS(fname,printable);
		} catch (IOException exn) {
			String button[]={"OK"};
			MessageDialog md=new MessageDialog(this,"Error",
			      "Unable to write file "+fname+".",button);
			md.setSize(350,200);
			md.setVisible(true);
		}
	}

	public GraphBrowserFrame(GraphBrowser br) {
		super("GraphBrowser");
		MenuItem i3, i4;
		gb = br;
		MenuBar mb = new MenuBar();
		Menu m1 = new Menu("File");
		m1.add(i3 = new MenuItem("Open ..."));
		m1.add(i1 = new MenuItem("Export to PostScript"));
		m1.add(i2 = new MenuItem("Export to EPS"));
		m1.add(i4 = new MenuItem("Quit"));
		i1.addActionListener(this);
		i2.addActionListener(this);
		i3.addActionListener(this);
		i4.addActionListener(this);
		checkMenuItems();
		mb.add(m1);
		setMenuBar(mb);
		add("Center", br);
    addWindowListener( new WindowAdapter() {
      public void windowClosing(WindowEvent e) {
        System.exit(0);
      }
    });
	}
}