--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/TreeBrowser.java Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,94 @@
+/***************************************************************************
+ Title: graphbrowser/TreeBrowser.java
+ Author: Stefan Berghofer, TU Muenchen
+ Options: :tabSize=4:
+
+ This class defines the browser window which is used to display directory
+ trees. It contains methods for handling events.
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.*;
+import java.awt.event.*;
+import java.util.*;
+
+
+public class TreeBrowser extends Canvas implements MouseListener
+{
+ TreeNode t;
+ TreeNode selected;
+ GraphView gv;
+ long timestamp;
+ Dimension size;
+ boolean parent_needs_layout;
+ Font font;
+
+ public TreeBrowser(TreeNode tn, GraphView gr, Font f) {
+ t = tn; gv = gr; font = f;
+ size = new Dimension(0, 0);
+ parent_needs_layout = true;
+ addMouseListener(this);
+ }
+
+ public Dimension getPreferredSize() {
+ return size;
+ }
+
+ public void mouseEntered(MouseEvent evt) {}
+
+ public void mouseExited(MouseEvent evt) {}
+
+ public void mouseReleased(MouseEvent evt) {}
+
+ public void mousePressed(MouseEvent evt) {}
+
+ public void mouseClicked(MouseEvent e)
+ {
+ TreeNode l=t.lookup(e.getY());
+
+ if (l!=null)
+ {
+ if (l.select()) {
+ Vector v=new Vector(10,10);
+ t.collapsedDirectories(v);
+ gv.collapseDir(v);
+ gv.relayout();
+ } else {
+ Vertex vx=gv.getGraph().getVertexByNum(l.getNumber());
+ gv.focusToVertex(l.getNumber());
+ vx=gv.getOriginalGraph().getVertexByNum(l.getNumber());
+ if (e.getWhen()-timestamp < 400 && !(vx.getPath().equals("")))
+ gv.getBrowser().viewFile(vx.getPath());
+ timestamp=e.getWhen();
+
+ }
+ selected=l;
+ parent_needs_layout = true;
+ repaint();
+ }
+ }
+
+ public void selectNode(TreeNode nd) {
+ Vector v=new Vector(10,10);
+ nd.select();
+ t.collapsedDirectories(v);
+ gv.collapseDir(v);
+ gv.relayout();
+ selected=nd;
+ parent_needs_layout = true;
+ repaint();
+ }
+
+ public void paint(Graphics g)
+ {
+ g.setFont(font);
+ Dimension d = t.draw(g,5,5,selected);
+ if (parent_needs_layout) {
+ size = new Dimension(5+d.width, 5+d.height);
+ parent_needs_layout = false;
+ getParent().doLayout();
+ }
+ }
+}
+