sourcepane.java

ALGAE是一个快速创建算法演示的框架。目前支持的算法实现语言包括java和c

package edu.odu.cs.zeil.AlgAE.Client.SourceViewer;

import java.awt.BorderLayout;
import java.awt.CardLayout;
import java.awt.Color;
import java.awt.Dimension;
import java.awt.Font;
import java.awt.Label;
import java.awt.MenuItem;
import java.awt.Panel;
import java.awt.TextArea;

import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.ComponentAdapter;
import java.awt.event.ComponentEvent;
import java.awt.event.ComponentListener;

import java.io.BufferedReader;
import java.io.FileReader;
import java.io.InputStreamReader;

import java.net.URL;

import java.util.Hashtable;
import java.util.Vector;


import edu.odu.cs.zeil.AlgAE.Debug;
import edu.odu.cs.zeil.AlgAE.Direction;
import edu.odu.cs.zeil.AlgAE.Client.SourceViewer.SourceFile;

import java.awt.*;

public class SourcePane extends Panel
{
  private Label status;
  private int fontSize;
  private Panel mainPanel;
  private Vector files;
  private Vector menuItems;
  
  /**
   *  Maps frame identifiers (strings) onto Locations, indicating
   *  the source code to be displayed during a given frame.
   */
  private Hashtable frameIndex;


  class Location 
  {
    public SourceFile source;
    public int lineNumber;

    Location (SourceFile sf, int lineNum)
    {
      source = sf;
      lineNumber = lineNum;
    }
  }
  

  class Reader extends Thread
  {
    private Vector sourceFiles;

    Reader (Vector sources)
    {
      sourceFiles = sources;
    }

    public void run()
    {
      for (int fileNum = 0; fileNum < sourceFiles.size(); ++fileNum)
	{
	  Debug.show (Debug.sourceCode, "processing source file ", fileNum);

	  SourceFile sf = (SourceFile) sourceFiles.elementAt (fileNum);
 	  String fileName = sf.getFullFileName();
	  boolean isURL =  (fileName.indexOf("://") >= 0)
	      || (fileName.indexOf("file:") == 0);

	  // First, read the source code
	  boolean keepTrying = true;
	  BufferedReader sourceIn = null;
	  try {
	    if (isURL)
	      {
		Debug.show (Debug.sourceCode, "opening " + fileName +
			    "as URL");
		URL url = new URL(fileName);
		sourceIn = new BufferedReader
		  (new InputStreamReader (url.openStream()));
	      }
	    else
		{
		    Debug.show (Debug.sourceCode, "opening " + fileName +
				"as a local file");
		    sourceIn = new BufferedReader (new FileReader (fileName));
		}
	  }
 	  catch (java.io.FileNotFoundException e)
	    {
	      Debug.error ("Unable to open " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }
	  catch (java.net.MalformedURLException e)
	    {
	      Debug.error ("Bad URL: " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }
 	  catch (java.io.IOException e)
	    {
	      Debug.error ("Unable to open " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }

	  String line;
	  try {
	    while (keepTrying && ((line = sourceIn.readLine()) != null))
	      {
		sf.addLine (line);
	      }
	  }
	  catch (java.io.IOException e)
	    {
	      Debug.error ("Error reading from " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }
	  
	  if (sourceIn != null)
	    try {
	      sourceIn.close();
	    }
	  catch (java.io.IOException e)
	    {
	      Debug.error ("Error when closing " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }
	  sf.doneAdding();
	  
	  
	  // Then read the accompanying index.
 	  fileName = sf.getIndexFileName();
	  isURL =  (fileName.indexOf("://") >= 0)
	      || (fileName.indexOf("file:") == 0);

	  keepTrying = true;
	  try {
	    if (isURL)
	      {
		URL url = new URL(fileName);
		sourceIn = new BufferedReader
		  (new InputStreamReader (url.openStream()));
	      }
	    else
	      sourceIn = new BufferedReader (new FileReader (fileName));
	  }
 	  catch (java.io.FileNotFoundException e)
	    {
	      Debug.error ("Unable to open " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }
	  catch (java.net.MalformedURLException e)
	    {
	      Debug.error ("Bad URL: " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }
 	  catch (java.io.IOException e)
	    {
	      Debug.error ("Unable to open " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }

	  try {
	    while (keepTrying && ((line = sourceIn.readLine()) != null))
	      {
		line.trim();
		int fieldSeparation = line.indexOf(' ');
		if (fieldSeparation >= 0)
		  {
		    try {
		      Integer lineNumber = new Integer
			(line.substring(0,fieldSeparation));
		      String frameIdentifier =
			line.substring(fieldSeparation+1);
		      synchronized (frameIndex) {
			if (frameIdentifier.length() >= 0)
			  {
			    if (frameIndex.get(frameIdentifier) == null)
			      {
				frameIndex.put
				  (frameIdentifier,
				   new Location (sf, lineNumber.intValue()));
			      }
			    else
			      Debug.error
				("Error: duplicate frame identifier\n"
				 + frameIdentifier);
			  }
			else
			  Debug.error ("Error: improper format in index file "
				       + fileName + ":\n" +
				       line);
		      }
		    }
		    catch (NumberFormatException e) {
		      Debug.error ("Error: improper format in index file "
				   + fileName + ":\n" +
				   line + "\n" + e.getMessage());
		    }
		  }
		else
		  Debug.error ("Error: improper format in index file "
			       + fileName + ":\n" +
			       line);
	      }
	  }
	  catch (java.io.IOException e)
	    {
	      Debug.error ("Error reading from " + fileName
			   + "\n" + e.getMessage());
	      keepTrying = false;
	    }

	  if (sourceIn != null) 
	    try {
	      sourceIn.close();
	    }
	    catch (java.io.IOException e)
	      {
		Debug.error ("Error when closing " + fileName
		  	     + "\n" + e.getMessage());
		keepTrying = false;
	      }	  
	}
    }
    
  }
  
  private Reader reader;
    
   
  public SourcePane(Hashtable commandArgs)
  {
    setLayout(new BorderLayout());

    mainPanel = new Panel();
    add ("Center", mainPanel);

    status = new Label("file: ");
    status.setBackground (Color.lightGray);
    add ("South", status);

    mainPanel.setLayout (new CardLayout());

    files = new Vector();
    int i = 0;
    String fullFileName;
    String indexFileName;
    menuItems = new Vector();
    frameIndex = new Hashtable();
    
    while ((fullFileName = (String)commandArgs.get("source"+i)) != null)
      {
	Debug.show (Debug.sourceCode, "saving source file name ", fullFileName);
	indexFileName = (String)commandArgs.get("index"+i);
	if (indexFileName != null)
	  {
	    SourceFile sf = new SourceFile (fullFileName, indexFileName);
	    files.addElement (sf);
	    mainPanel.add (sf.getFileName(), sf);

	    MenuItem item = new MenuItem (sf.getFileName());
	    item.addActionListener(new ActionListener() {
	      public void actionPerformed(ActionEvent e) {
		MenuItem it = (MenuItem)e.getSource();
		display (it.getLabel(), -1);
		}});
	    menuItems.addElement (item);
	  }
	else
	  Debug.error ("No index file specified to corresponding to "
		       + fullFileName);
	
	++i;
      }
    if (i > 0)
      {
	SourceFile sf = (SourceFile)files.elementAt(0);
	display (sf.getFileName(), 0);
      }


    reader = new Reader(files);
    reader.start();
  }


  
  public void setLabel (String filename, int lineNum)
  {
    if (lineNum >= 0)
      status.setText (filename + ": " + lineNum);
    else
      status.setText (filename);
    //    status.repaint();
  }

  
  public void display (String fileName, int lineNumber)
  {
    setLabel (fileName, lineNumber);
    ((CardLayout) mainPanel.getLayout()).show (mainPanel, fileName);
  }

  public void display (String frameIdentifier)
  {
    Location loc;
    synchronized (frameIndex) {
      loc = (Location)frameIndex.get (frameIdentifier);
    }
    if (loc != null)
      {
	display (loc.source.getFileName(), loc.lineNumber);
	loc.source.focusOnLine (loc.lineNumber);
      }
  }

  public Vector getMenuItems()
  {
    return menuItems;
  }
  
  public void setFontSize (int size)
  {
    Font textFont = new Font("Courier", Font.PLAIN, size);
    for (int i = 0; i < files.size(); ++i)
      {
	SourceFile sf = (SourceFile)files.elementAt(i);
	sf.setFont (textFont);
      }
    
    Font oldStatusFont = status.getFont();
    if (oldStatusFont == null)
      {
	oldStatusFont = new Font ("Dialog", Font.PLAIN, size);
      }
    
    status.setFont
      (new Font(oldStatusFont.getName(),
		oldStatusFont.getStyle(),
		size));
    // invalidate();
  }

  public int getNumberOfFiles()
  {
    return files.size();
  }
  public synchronized Dimension getMinimumSize() {
    return new Dimension (10,10);
  }


  public boolean isFocusTraversable()
  {
    return true;
  }
  
}