--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphView.java Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,276 @@
+/***************************************************************************
+ 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) {}
+}