diff -r 3b8b1da2ff29 -r 12b1f4649ab1 src/Tools/GraphBrowser/graphbrowser/TreeBrowser.java
--- /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();
+		}
+	}
+}
+