Quellcode-Bibliothek GraphView.java Sprache: JAVA

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

  This class defines the window in which the graph is displayed. It
  contains methods for handling events such as collapsing / uncollapsing
  nodes of the graph.
***************************************************************************/

package isabelle.graphbrowser;

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

public class GraphView extends Canvas implements MouseListener, MouseMotionListener {
Graph gra, gra2;
GraphBrowser browser;
Vertex v = null;
Vector collapsed = new Vector(10,10);
Vector collapsedDirs = new Vector(10,10);
TreeBrowser tb;
long timestamp;
Vertex highlighted = null;
Dimension size;
boolean parent_needs_layout;
Font font;

public void setTreeBrowser(TreeBrowser br) {
  tb=br;
}

public GraphBrowser getBrowser() { return browser; }

public Graph getGraph() { return gra; }

public Graph getOriginalGraph() { return gra2; }

public GraphView(Graph gr, GraphBrowser br, Font f) {
  gra2=gr;
  browser=br;
  gra=(Graph)(gra2.clone());
  parent_needs_layout = true;
  size = new Dimension(0, 0);
  font = f;
  addMouseListener(this);
  addMouseMotionListener(this);
}

public void PS(String fname,boolean printable) throws IOException {
     Graph gra3 = (Graph)gra.clone();
     gra3.layout(null);
     gra3.PS(fname,printable);
}

public void paint(Graphics g) {
  g.setFont(font);
  gra.draw(g);
  if (highlighted!=null) highlighted.drawBox(g,Color.white);
  size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y);
  if (parent_needs_layout) {
   parent_needs_layout = false;
   getParent().doLayout();
  }
}

public Dimension getPreferredSize() {
  return size;
}

public void mouseMoved(MouseEvent evt) {
  int x = evt.getX() + gra.min_x;
  int y = evt.getY() + gra.min_y;

  Vertex v2=gra.vertexAt(x,y);
  Graphics g=getGraphics();
  g.setFont(font);
  g.translate(-gra.min_x,-gra.min_y);
  if (highlighted!=null) {
   highlighted.drawBox(g,Color.lightGray);
   highlighted=null;
  }
  if (v2!=v) {
   if (v!=null) v.removeButtons(g);
   if (v2!=null) v2.drawButtons(g);
   v=v2;
  }
}

public void mouseDragged(MouseEvent evt) {}

/*****************************************************************/
/* This method is called if successor / predecessor nodes (whose */
/* numbers are stored in Vector c) of a certain node should be   */
        /* displayed again                                               */
/*****************************************************************/

void uncollapse(Vector c) {
  collapsed.removeElement(c);
  collapseNodes();
}

/*****************************************************************/
/* This method is called by class TreeBrowser when directories   */
/* are collapsed / uncollapsed by the user                       */
/*****************************************************************/

public void collapseDir(Vector v) {
  collapsedDirs=v;

  collapseNodes();
}

/*****************************************************************/
/*                      Inflate node again                       */
/*****************************************************************/

public void inflateNode(Vector c) {
  Enumeration e1;

  e1=collapsedDirs.elements();
  while (e1.hasMoreElements()) {
   Directory d=(Directory)(e1.nextElement());
   if (d.collapsed==c) {
    tb.selectNode(d.getNode());
    return;
   }
  }

  collapsed.removeElement(c);
  e1=gra2.getVertices();
  while (e1.hasMoreElements()) {
   Vertex vx=(Vertex)(e1.nextElement());
   if (vx.getUp()==c) vx.setUp(null);
   if (vx.getDown()==c) vx.setDown(null);
  }

  collapseNodes();
  relayout();
}

public void relayout() {
  Graphics g = getGraphics();
  g.setFont(font);
  browser.showWaitMessage();
  highlighted=null;
  gra.layout(g);
  v=null;
  parent_needs_layout = true;
  update(g);
  browser.showReadyMessage();
}

public void focusToVertex(int n) {
  Vertex vx=gra.getVertexByNum(n);
  if (vx!=null) {
   ScrollPane scrollp = (ScrollPane)(getParent());
   Dimension vpsize = scrollp.getViewportSize();

                        int x = vx.getX()-gra.min_x;
                        int y = vx.getY()-gra.min_y;
   int offset_x = Math.min(scrollp.getHAdjustable().getMaximum(),
    Math.max(0,x-vpsize.width/2));
   int offset_y = Math.min(scrollp.getVAdjustable().getMaximum(),
    Math.max(0,y-vpsize.height/2));

   Graphics g=getGraphics();
   g.setFont(font);
   g.translate(-gra.min_x,-gra.min_y);
   if (highlighted!=null) highlighted.drawBox(g,Color.lightGray);
   vx.drawBox(g,Color.white);
   highlighted=vx;
   scrollp.setScrollPosition(offset_x, offset_y);
  }
}

/*****************************************************************/
/*             Create new graph with collapsed nodes             */
/*****************************************************************/

public void collapseNodes() {
  Enumeration e1=collapsed.elements();
  gra=(Graph)(gra2.clone());

  while (e1.hasMoreElements()) {
   Vector v1=(Vector)(e1.nextElement());
   Vector v2=gra.decode(v1);
   if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1);
  }

  e1=collapsedDirs.elements();

  while (e1.hasMoreElements()) {
   Directory d=(Directory)(e1.nextElement());
   Vector v=gra.decode(d.getCollapsed());
   if (!v.isEmpty())
    gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
  }
}

public void mouseClicked(MouseEvent evt) {
  Vector code = null;
  Vertex v2;
  int x = evt.getX() + gra.min_x;
  int y = evt.getY() + gra.min_y;

  if (v!=null) {
   int num=v.getNumber();
   v2=gra2.getVertexByNum(num);
   if (v.leftButton(x,y)) {
    if (v.getUp()!=null) {
     code=v.getUp();
     v2.setUp(null);
     v=null;
     uncollapse(code);
     relayout();
     focusToVertex(num);
    } else {
     Vector vs=v2.getPreds();
     code=gra2.encode(vs);
     v.setUp(code);v2.setUp(code);
     v=null;
     collapsed.insertElementAt(code,0);
     collapseNodes();
     relayout();
     focusToVertex(num);
    }
   } else if (v.rightButton(x,y)) {
    if (v.getDown()!=null) {
     code=v.getDown();
     v2.setDown(null);
     v=null;
     uncollapse(code);
     relayout();
     focusToVertex(num);
    } else {
     Vector vs=v2.getSuccs();
     code=gra2.encode(vs);
     v.setDown(code);v2.setDown(code);
     v=null;
     collapsed.insertElementAt(code,0);
     collapseNodes();
     relayout();
     focusToVertex(num);
    }
   } else if (v.getInflate()!=null) {
    inflateNode(v.getInflate());
    v=null;
   } else {
    if (evt.getWhen()-timestamp < 400 && !(v.getPath().equals("")))
     browser.viewFile(v.getPath());
    timestamp=evt.getWhen();
   }
  }
}

public void mouseExited(MouseEvent evt) {
  Graphics g=getGraphics();
  g.setFont(font);
  g.translate(-gra.min_x,-gra.min_y);
  if (highlighted!=null) {
   highlighted.drawBox(g,Color.lightGray);
   highlighted=null;
  }
  if (v!=null) v.removeButtons(g);
  v=null;
}

public void mouseEntered(MouseEvent evt) {}

public void mousePressed(MouseEvent evt) {}

public void mouseReleased(MouseEvent evt) {}
}

quality93%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.16Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.