merged
authorwenzelm
Fri, 16 Jul 2021 22:32:56 +0200
changeset 74290 c4c612d92fcc
parent 74272 4cca14dc577c (current diff)
parent 74289 d609fa3e816d (diff)
child 74291 47a568d9067e
merged
--- a/.hgignore	Fri Jul 16 20:13:12 2021 +0100
+++ b/.hgignore	Fri Jul 16 22:32:56 2021 +0200
@@ -16,7 +16,6 @@
 ^heaps/
 ^browser_info/
 ^doc/.*\.pdf
-^lib/classes/
 ^src/Tools/VSCode/out/
 ^src/Tools/VSCode/extension/node_modules/
 ^Admin/jenkins/ci-extras/target/
--- a/Admin/build	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-#
-# Administrative build for Isabelle source distribution.
-
-## directory layout
-
-if [ -z "$ISABELLE_HOME" ]; then
-  unset CDPATH
-  ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-  ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-fi
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  cat <<EOF
-
-Usage: $PRG [MODULES]
-
-  Produce Isabelle distribution modules from current repository sources.
-  The MODULES list may contain any of the following:
-
-    all             all modules below
-    browser         graph browser
-    jars            Isabelle/Scala
-    jars_fresh      fresh build of jars
-
-EOF
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-[ "$#" -eq 0 ] && usage
-
-MODULES="$@"; shift "$#"
-
-
-## modules
-
-function build_all ()
-{
-  build_browser
-  build_setup build
-}
-
-
-function build_browser ()
-{
-  pushd "$ISABELLE_HOME/lib/browser" >/dev/null
-  "$ISABELLE_TOOL" env ./build || exit $?
-  popd >/dev/null
-}
-
-
-function build_setup ()
-{
-  rm -rf \
-    "$ISABELLE_HOME/lib/classes/Pure.jar" \
-    "$ISABELLE_HOME/lib/classes/Pure.shasum" \
-    "$ISABELLE_HOME/src/Tools/jEdit/dist"
-  env ISABELLE_SETUP_CLASSPATH_SKIP=true "$ISABELLE_TOOL" java isabelle.setup.Setup "$@"
-}
-
-
-## main
-
-for MODULE in $MODULES
-do
-  case $MODULE in
-    all) build_all;;
-    browser) build_browser;;
-    jars) build_setup build;;
-    jars_fresh) build_setup build_fresh;;
-    *) fail "Bad module $MODULE"
-  esac
-done
--- a/Admin/build_history	Fri Jul 16 20:13:12 2021 +0100
+++ b/Admin/build_history	Fri Jul 16 22:32:56 2021 +0200
@@ -5,5 +5,5 @@
 unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-"$THIS/build" jars > /dev/null || exit $?
+env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $?
 exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"
--- a/Admin/build_release	Fri Jul 16 20:13:12 2021 +0100
+++ b/Admin/build_release	Fri Jul 16 22:32:56 2021 +0200
@@ -5,5 +5,5 @@
 unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-"$THIS/build" jars || exit $?
+env ISABELLE_SETUP_CLASSPATH_SKIP=true "$THIS/../bin/isabelle" java isabelle.setup.Setup build > /dev/null || exit $?
 exec "$THIS/../bin/isabelle_java" isabelle.Build_Release "$@"
--- a/Admin/components/components.sha1	Fri Jul 16 20:13:12 2021 +0100
+++ b/Admin/components/components.sha1	Fri Jul 16 22:32:56 2021 +0200
@@ -126,6 +126,8 @@
 a0e7527448ef0f7ce164a38a50dc26e98de3cad6  isabelle_setup-20210709.tar.gz
 e413706694b0968245ee15183af2d464814ce0a4  isabelle_setup-20210711.tar.gz
 d2c9fd7b73457a460111edd6eb93a133272935fb  isabelle_setup-20210715.tar.gz
+a5f478ba1088f67c2c86dc2fa7764b6d884e5ae5  isabelle_setup-20210716-1.tar.gz
+79fad009cb22aa5e7cb4aed3c810ad5f61790293  isabelle_setup-20210716.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56  jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39  jdk-11.0.2+9.tar.gz
--- a/Admin/components/main	Fri Jul 16 20:13:12 2021 +0100
+++ b/Admin/components/main	Fri Jul 16 22:32:56 2021 +0200
@@ -8,7 +8,7 @@
 flatlaf-1.2
 idea-icons-20210508
 isabelle_fonts-20210322
-isabelle_setup-20210715
+isabelle_setup-20210716-1
 jdk-15.0.2+7
 jedit-20210715
 jfreechart-1.5.1
--- a/bin/isabelle	Fri Jul 16 20:13:12 2021 +0100
+++ b/bin/isabelle	Fri Jul 16 22:32:56 2021 +0200
@@ -45,7 +45,7 @@
 
 ## internal tool or usage (Scala)
 
-isabelle_admin_build jars || exit $?
+isabelle_scala_build || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
--- a/etc/components	Fri Jul 16 20:13:12 2021 +0100
+++ b/etc/components	Fri Jul 16 22:32:56 2021 +0200
@@ -1,5 +1,6 @@
 #built-in components
 src/Tools/jEdit
+src/Tools/GraphBrowser
 src/Tools/Graphview
 src/Tools/VSCode
 src/HOL/Mutabelle
--- a/lib/Tools/browser	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: Isabelle graph browser
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
-  echo
-  echo "  Options are:"
-  echo "    -b           Admin/build only"
-  echo "    -c           cleanup -- remove GRAPHFILE after use"
-  echo "    -o FILE      output to FILE (ps, eps, pdf)"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-ADMIN_BUILD=""
-CLEAN=""
-OUTFILE=""
-
-while getopts "bco:" OPT
-do
-  case "$OPT" in
-    b)
-      ADMIN_BUILD=true
-      ;;
-    c)
-      CLEAN=true
-      ;;
-    o)
-      OUTFILE="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-GRAPHFILE=""
-[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-isabelle_admin_build browser || exit $?
-
-classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
-
-if [ -n "$GRAPHFILE" ]; then
-  PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
-  if [ -n "$CLEAN" ]; then
-    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
-  else
-    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
-  fi
-
-  PDF=""
-  case "$OUTFILE" in
-    *.pdf)
-      OUTFILE="${OUTFILE%%.pdf}.eps"
-      PDF=true
-      ;;
-  esac
-
-  if [ -z "$OUTFILE" ]; then
-    isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
-  else
-    isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
-  fi
-  RC="$?"
-
-  if [ -n "$PDF" ]; then
-    (
-      cd "$(dirname "$OUTFILE")"
-      "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
-    )
-  fi
-
-  rm -f "$PRIVATE_FILE"
-elif [ -z "$ADMIN_BUILD" ]; then
-  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
-  exec isabelle java GraphBrowser.GraphBrowser
-else
-  RC=0
-fi
-
-exit "$RC"
--- a/lib/Tools/components	Fri Jul 16 20:13:12 2021 +0100
+++ b/lib/Tools/components	Fri Jul 16 22:32:56 2021 +0200
@@ -127,7 +127,7 @@
   echo "Missing components:"
   for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
 elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then
-  isabelle_admin_build jars || exit $?
+  isabelle_scala_build || exit $?
   exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
 else
   for NAME in "${SELECTED_COMPONENTS[@]}"
--- a/lib/Tools/console	Fri Jul 16 20:13:12 2021 +0100
+++ b/lib/Tools/console	Fri Jul 16 22:32:56 2021 +0200
@@ -4,7 +4,7 @@
 #
 # DESCRIPTION: raw ML process (interactive mode)
 
-isabelle_admin_build jars || exit $?
+isabelle_scala_build || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 
--- a/lib/Tools/scala	Fri Jul 16 20:13:12 2021 +0100
+++ b/lib/Tools/scala	Fri Jul 16 22:32:56 2021 +0200
@@ -4,7 +4,7 @@
 #
 # DESCRIPTION: invoke Scala within the Isabelle environment
 
-isabelle_admin_build jars || exit $?
+isabelle_scala_build || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
 declare -a SCALA_ARGS=()
--- a/lib/Tools/scalac	Fri Jul 16 20:13:12 2021 +0100
+++ b/lib/Tools/scalac	Fri Jul 16 22:32:56 2021 +0200
@@ -4,7 +4,7 @@
 #
 # DESCRIPTION: invoke Scala compiler within the Isabelle environment
 
-isabelle_admin_build jars || exit $?
+isabelle_scala_build || exit $?
 
 classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
 classpath "$CLASSPATH"; unset CLASSPATH
--- a/lib/browser/GraphBrowser/AWTFontMetrics.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/AWTFontMetrics.java
-  Author:     Gerwin Klein, TU Muenchen
-
-  AbstractFontMetrics from the AWT for graphics mode.
-  
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.awt.FontMetrics;
-
-public class AWTFontMetrics implements AbstractFontMetrics {
-  private FontMetrics fontMetrics;
-
-  public AWTFontMetrics(FontMetrics m) {
-    fontMetrics = m;
-  }
-
-  public int stringWidth(String str) {
-    return fontMetrics.stringWidth(str);
-  }
-
-  public int getAscent() {
-    return fontMetrics.getAscent();
-  }
-
-  public int getDescent() {
-    return fontMetrics.getDescent();
-  }
-}
--- a/lib/browser/GraphBrowser/AbstractFontMetrics.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/AWTFontMetrics.java
-  Author:     Gerwin Klein, TU Muenchen
-
-  AbstractFontMetrics avoids dependency on java.awt.FontMetrics in 
-  batch mode.
-  
-***************************************************************************/
-
-package GraphBrowser;
-
-public interface AbstractFontMetrics {
-  public int stringWidth(String str);
-  public int getAscent();
-  public int getDescent();
-}
--- a/lib/browser/GraphBrowser/Box.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/Box.java
-  Author:     Gerwin Klein, TU Muenchen
-
-  A box with width and height. Used instead of java.awt.Dimension for 
-  batch mode.
-
-***************************************************************************/
-
-package GraphBrowser;
-
-public class Box {
-  public int width;
-  public int height;
-
-  public Box(int w, int h) {
-    this.width = w;
-    this.height = h;
-  }
-}
--- a/lib/browser/GraphBrowser/Console.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/Console.java
-  Author:     Gerwin Klein, TU Muenchen
-  Options:    :tabSize=2:
-
-  This is the graph browser's main class when run as a console application.
-  It duplicates some logic from GraphBrowser and GraphView.
-  It does so to remove dependency on AWT.
-
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.io.*;
-import java.util.*;
-
-public class Console {
-	Graph g;
-	String gfname;  
-
-  public Console(String name) {
-    gfname = name;
-  }
-
-	public void PS(String fname, boolean printable) throws IOException {
-    g.layout(null);
-		g.PS(fname,printable);
-	}
-
-
-	public void collapseNodes(Vector collapsedDir) { 
-		Enumeration e1=collapsedDir.elements();
-		Graph gra=(Graph)(g.clone());
-
-		while (e1.hasMoreElements()) {
-			Directory d=(Directory)(e1.nextElement());
-			Vector v=gra.decode(d.getCollapsed());
-			if (!v.isEmpty())
-				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
-		}
-    
-    g = gra;
-	}
-
-
-	public void initBrowser(InputStream is) {
-		try {
-			TreeNode tn = new TreeNode("Root", "", -1, true);
-      g = new Graph(is, tn);
-			Vector v = new Vector(10,10);
-			tn.collapsedDirectories(v);      
-      collapseNodes(v);
-		} catch (IOException exn) {
-			System.err.println("\nI/O error while reading graph file.");
-		} catch (ParseError exn) {
-			System.err.println("\nParse error in graph file:");
-			System.err.println(exn.getMessage());
-			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> "+
-                         "[ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
-		}
-	}
-
-	public static void main(String[] args) {
-		try {
-      if (args.length <= 1) {
-        System.err.println("Graph and output file expected.");
-        return;
-      }
-
-			Console console=new Console(args[0]);
-      InputStream is=new FileInputStream(args[0]);
-      console.initBrowser(is);
-      is.close();      
-    
-      try {
-        if (args[1].endsWith(".ps"))
-          console.PS(args[1], true);
-        else if (args[1].endsWith(".eps"))
-          console.PS(args[1], false);
-        else
-          System.err.println("Unknown file type: " + args[1]);
-      } catch (IOException exn) {
-        System.err.println("Unable to write file " + args[1]);
-      }
-		} catch (IOException exn) {
-			System.err.println("Can't open graph file "+args[0]);
-		}
-	}
-}
--- a/lib/browser/GraphBrowser/DefaultFontMetrics.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/DefaultFontMetrics.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=2:
-
-  Default font metrics which is used when no graphics context
-  is available (batch mode).
-***************************************************************************/
-
-package GraphBrowser;
-
-public class DefaultFontMetrics implements AbstractFontMetrics {
-
-  private static int[] chars =
-	{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
-	 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
-	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
-	 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24,
-	 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
-	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
-
-  private int size;
-
-  public DefaultFontMetrics(int size)
-  { this.size = size; }
-
-  public int getLeading()
-  { return 1; }
-
-  public int getAscent()
-  { return (int)(Math.round(size * 46.0 / 48.0)); }
-  
-  public int getDescent() 
-  { return (int)(Math.round(size * 10.0 / 48.0)); }
-  
-  public int charWidth(char c) {
-    if (c < 32 || c > 126) { return 0; }
-    else {
-	    return (int)(Math.round(chars[c - 32] * size / 48.0));
-    }
-  }
-  
-  public int stringWidth(String s) {
-    int l=0, i;
-    for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
-    return l;
-  }
-}
--- a/lib/browser/GraphBrowser/Directory.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-package GraphBrowser;
-
-import java.util.Vector;
-
-class Directory {
-	TreeNode node;
-	String name;
-	Vector collapsed;
-
-	public Directory(TreeNode nd,String n,Vector col) {
-		collapsed=col;
-		name=n;
-		node=nd;
-	}
-
-	public TreeNode getNode() { return node; }
-
-	public String getName() { return name; }
-
-	public Vector getCollapsed() { return collapsed; }
-}
--- a/lib/browser/GraphBrowser/DummyVertex.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/DummyVertex.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This class represents a dummy vertex, which is used to simplify the
-  layout algorithm.
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.awt.*;
-
-class DummyVertex extends Vertex {
-	public boolean isDummy() {return true;}
-
-	public Object clone() {
-		Vertex ve=new DummyVertex();
-		ve.setX(getX());ve.setY(getY());
-		return ve;
-	}
-
-	public int leftX() { return getX(); }
-
-	public int rightX() { return getX(); }
-
-	public void draw(Graphics g) {}
-}
-
--- a/lib/browser/GraphBrowser/Graph.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1062 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/Graph.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This class contains the core of the layout algorithm and methods for
-  drawing and PostScript output.
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.util.*;
-import java.awt.*;
-import java.io.*;
-
-public class Graph {
-	/**** parameters for layout ****/
-
-	public int box_height=0;
-	public int box_height2;
-	public Graphics gfx;
-
-	Vector vertices=new Vector(10,10);
-	Vector splines=new Vector(10,10);
-	Vector numEdges=new Vector(10,10);
-	Vertex []vertices2;
-
-	public int min_x=0,min_y=0,max_x=10,max_y=10;
-
-	/********************************************************************/
-	/*                         clone graph object                       */
-	/********************************************************************/
-
-	public Object clone() {
-		Graph gr=new Graph();
-		Enumeration e1;
-		int i;
-
-		gr.splines=(Vector)(splines.clone());
-
-		e1=vertices.elements();
-		while (e1.hasMoreElements())
-			gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone()));
-
-		for (i=0;i<vertices.size();i++) {
-			Vertex vx1=(Vertex)(gr.vertices.elementAt(i));
-			e1=((Vertex)(vertices.elementAt(i))).getChildren();
-			while (e1.hasMoreElements()) {
-				Vertex vx2=(Vertex)(gr.vertices.elementAt(vertices.indexOf(e1.nextElement())));
-				vx1.addChild(vx2);
-			}
-		}
-
-		gr.vertices2 = new Vertex[vertices.size()];
-		gr.vertices.copyInto(gr.vertices2);
-
-		gr.min_x=min_x;gr.max_x=max_x;
-		gr.min_y=min_y;gr.max_y=max_y;
-
-		return gr;
-	}
-
-	Graph() {}
-
-	/********************************************************************/
-	/*                      Read graph from stream                      */
-	/********************************************************************/
-
-	public Graph(InputStream s,TreeNode tn) throws IOException, ParseError {
-		StreamTokenizer tok=new StreamTokenizer(new InputStreamReader(s));
-		String name,dir,vertexID;
-		Vertex ve1,ve2;
-		boolean children,unfoldDir;
-		int index=0;
-
-		tok.nextToken();
-		while (tok.ttype!=StreamTokenizer.TT_EOF) {
-			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
-				throw new ParseError("expected: vertex name\nfound   : "+tok.toString());
-			name=tok.sval;
-                        tok.nextToken();
-			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
-				throw new ParseError("expected: vertex identifier\nfound   : "+tok.toString());
-			vertexID=tok.sval;
-			tok.nextToken();
-			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
-				throw new ParseError("expected: directory name\nfound   : "+tok.toString());
-			dir=tok.sval;
-			tok.nextToken();
-			if (tok.ttype=='+') {
-				unfoldDir=true;
-				tok.nextToken();
-			} else
-				unfoldDir=false;
-			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
-				throw new ParseError("expected: path name\nfound   : "+tok.toString());
-			ve1=findVertex(vertexID);
-			if (ve1==null) {
-				ve1=new NormalVertex("");
-				ve1.setID(vertexID);
-				ve1.setNumber(index++);
-				addVertex(ve1);
-			}
-			ve1.setPath(tok.sval);
-			ve1.setDir(dir);
-                        ve1.setLabel(name);
-			tn.insertNode(name,dir,tok.sval,ve1.getNumber(),unfoldDir);
-			tok.nextToken();
-			if (tok.ttype=='<') {
-				children=true;
-				tok.nextToken();
-			} else if (tok.ttype=='>') {
-					children=false;
-					tok.nextToken();
-			} else children=true;
-			while (tok.ttype!=';') {
-				if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
-					throw new ParseError("expected: child vertex identifier or ';'\nfound   : "+tok.toString());				
-				ve2=findVertex(tok.sval);
-				if (ve2==null) {
-					ve2=new NormalVertex("");
-					ve2.setID(tok.sval);
-					ve2.setNumber(index++);
-					addVertex(ve2);
-				}
-				if (children)
-					ve1.addChild(ve2);
-				else
-					ve1.addParent(ve2);
-				tok.nextToken();
-			}
-			tok.nextToken();
-		}
-		vertices2 = new Vertex[vertices.size()];
-		vertices.copyInto(vertices2);
-	}
-	
-	/*** Find vertex with identifier vertexID ***/
-
-	public Vertex findVertex(String vertexID) {
-		Enumeration e1=vertices.elements();
-		Vertex v1;
-
-		while (e1.hasMoreElements()) {
-			v1=(Vertex)(e1.nextElement());
-			if ((v1.getID()).equals(vertexID))
-				return v1;
-		}
-		return null;
-	}
-		 
-	public void addVertex(Vertex v) {
-		vertices.addElement(v);
-		v.setGraph(this);
-	}
-
-	public void removeVertex(Vertex v) {
-		vertices.removeElement(v);
-	}
-
-	public Enumeration getVertices() {
-		return vertices.elements();
-	}
-
-	/********************************************************************/
-	/*                          graph layout                            */
-	/********************************************************************/
-
-	public void layout(Graphics g) {
-		splines.removeAllElements();
-		hasseDiagram();
-		Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0))));
-		setParameters(g);
-		init_coordinates(layers);
-		pendulum(layers);
-		rubberband(layers);
-		calcSplines(layers);
-		calcBoundingBox();
-	}
-
-	/********************************************************************/
-	/*                      set layout parameters                       */
-	/********************************************************************/
-
-	public void setParameters(Graphics g) {
-		Enumeration e1=vertices.elements();
-		int h;
-		h=Integer.MIN_VALUE;
-
-		while (e1.hasMoreElements()) {
-		  Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
-			h=Math.max(h,dim.height);
-		}
-		box_height=h+4;
-		box_height2=box_height/2;
-		gfx=g;
-	}
-
-	/********************************************************************/
-	/*                       topological sorting                        */
-	/********************************************************************/
-
-	public Vector sort() {
-		Vector todo=(Vector)(vertices.clone());
-		Vector layers=new Vector(10,10);
-		Vector todo2;
-		Enumeration e1,e2;
-		Vertex v,v2;
-
-		e1=vertices.elements();
-		while (e1.hasMoreElements())
-			((Vertex)(e1.nextElement())).setDegree(0);
-
-		e1=vertices.elements();
-		while (e1.hasMoreElements()) {
-			v=(Vertex)(e1.nextElement());
-			e2=v.getChildren();
-			while (e2.hasMoreElements()) {
-				v2=(Vertex)(e2.nextElement());
-				todo.removeElement(v2);
-				v2.setDegree(1+v2.getDegree());
-			}
-		}
-		while (!todo.isEmpty()) {
-			layers.addElement(todo);
-			todo2=new Vector(10,10);
-			e1=todo.elements();
-			while (e1.hasMoreElements()) {
-				e2=((Vertex)(e1.nextElement())).getChildren();
-				while (e2.hasMoreElements()) {
-					v=(Vertex)(e2.nextElement());
-					v.setDegree(v.getDegree()-1);
-					if (v.getDegree()==0) {
-						todo2.addElement(v);
-						v.setDegree(layers.size());
-					}
-				}
-			}
-			todo=todo2;
-		}
-		return layers;
-	}
-
-	/********************************************************************/
-	/*                      compute hasse diagram                       */
-	/********************************************************************/
-
-	public void hasseDiagram() {
-		Enumeration e1,e2;
-		Vertex vx1,vx2;
-
-		/** construct adjacence matrix **/
-
-		int vs=vertices.size();
-		boolean adj[][]=new boolean[vs][vs];
-		boolean adj2[][]=new boolean[vs][vs];
-		int i,j,k;
-
-		e1=getVertices();
-		for (i=0;i<vs;i++) {
-			vx1=(Vertex)(e1.nextElement());
-			e2=vx1.getChildren();
-			while (e2.hasMoreElements()) {
-				vx2=(Vertex)(e2.nextElement());
-				j=vertices.indexOf(vx2);
-				adj[i][j]=true;
-				adj2[i][j]=true;
-			}
-		}
-
-		/** compute transitive closure R+ **/
-
-		for (k=0;k<vs;k++)
-			for (i=0;i<vs;i++)
-				if (adj[i][k])
-					for (j=0;j<vs;j++)
-						adj[i][j] = adj[i][j] || adj[k][j];
-
-		/** compute R \ (R+)^2 **/
-
-		for (i=0;i<vs;i++)
-			for (j=0;j<vs;j++)
-				if (adj2[i][j]) {
-					vx1=(Vertex)(vertices.elementAt(i));
-					vx2=(Vertex)(vertices.elementAt(j));
-					for (k=0;k<vs;k++)
-						if (adj[i][k] && adj[k][j]) {
-							vx1.removeChild(vx2);
-							break;
-						}
-				}
-	}
-				
-	/********************************************************************/
-	/*                      insert dummy vertices                       */
-	/********************************************************************/
-
-	public Vector insert_dummies(Vector v) {
-		Vector layers2=new Vector(10,10);
-		int n_edges;
-
-		do {
-			Enumeration e1=v.elements(),e2;
-			Vector next=new Vector(10,10);
-
-			layers2.addElement(v);
-			n_edges=0;
-			while (e1.hasMoreElements()) {
-				Vertex v1=(Vertex)(e1.nextElement());
-				e2=v1.getChildren();
-				while (e2.hasMoreElements()) {
-					n_edges++;
-					Vertex v2=(Vertex)(e2.nextElement());
-					if (v2.getDegree()!=v1.getDegree()+1) {
-						Vertex v3=new DummyVertex();
-						v3.addChild(v2);
-						v3.setDegree(v1.getDegree()+1);
-						v1.removeChild(v2);
-						v1.addChild(v3);
-						next.addElement(v3);
-						addVertex(v3);
-					} else if (next.indexOf(v2)<0) next.addElement(v2);
-				}
-			}
-			v=next;
-			numEdges.addElement(new Integer(n_edges));
-		} while (!v.isEmpty());
-		return layers2;
-	}
-
-	/********************************************************************/
-	/*                     calculation of crossings                     */
-	/********************************************************************/
-
-	public int count_crossings(Vector layers,int oldcr) {
-		int i,j,y1,y2,cr=0,l;
-		for (l=0;l<layers.size()-1;l++) {
-			Vector v1=(Vector)(layers.elementAt(l));
-			for (i=0;i<v1.size();i++) {
-				Enumeration e2=((Vertex)(v1.elementAt(i))).getChildren();
-				while (e2.hasMoreElements()) {
-					y1=((Vector)(layers.elementAt(l+1))).indexOf(e2.nextElement());
-					for (j=0;j<i;j++) {
-						Enumeration e3=((Vertex)(v1.elementAt(j))).getChildren();
-						while (e3.hasMoreElements()) {
-							y2=((Vector)(layers.elementAt(l+1))).indexOf(e3.nextElement());
-							if (y1<y2) {
-								cr++;
-								if (cr>=oldcr) return cr;
-							}
-						}
-					}
-				}
-			}
-		}
-		return cr;
-	}
-
-	/********************************************************************/
-	/* calculation of crossings where vertices vx1 and vx2 are involved */
-	/* vx1 and vx2 must be in same layer and vx1 is left from vx2       */
-	/********************************************************************/
-
-	public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) {
-		int i,cr=0,l=vx1.getDegree();
-		Vertex va,vb;
-		Vector layer;
-		Enumeration e1,e2;
-
-		if (l>0) {
-			layer=(Vector)(layers.elementAt(l-1));
-			e1=vx1.getParents();
-			while (e1.hasMoreElements()) {
-				va=(Vertex)(e1.nextElement());
-				i=layer.indexOf(va);
-				e2=vx2.getParents();
-				while (e2.hasMoreElements()) {
-					vb=(Vertex)(e2.nextElement());
-					if (layer.indexOf(vb)<i) {
-						cr++;
-						if (cr>=oldcr) return cr;
-					}
-				}
-			}
-		}
-		if (l<layers.size()-1) {
-			layer=(Vector)(layers.elementAt(l+1));
-			e1=vx1.getChildren();
-			while (e1.hasMoreElements()) {
-				va=(Vertex)(e1.nextElement());
-				i=layer.indexOf(va);
-				e2=vx2.getChildren();
-				while (e2.hasMoreElements()) {
-					vb=(Vertex)(e2.nextElement());
-					if (layer.indexOf(vb)<i) {
-						cr++;
-						if (cr>=oldcr) return cr;
-					}
-				}
-			}
-		}
-		return cr;
-	}
-
-	/********************************************************************/
-	/*       reduction of crossings by exchanging adjacent vertices     */
-	/********************************************************************/
-
-	public void exchangeVertices(Vector layers,int oldcr) {
-		int i,l,c1,c2;
-		Vertex vx1,vx2;
-		Vector v1;
-
-		for (l=0;l<layers.size();l++) {
-			v1=(Vector)(layers.elementAt(l));
-			for (i=0;i<v1.size()-1;i++) {
-				vx1=(Vertex)(v1.elementAt(i));
-				vx2=(Vertex)(v1.elementAt(i+1));
-				c1=count_crossings_2(layers,vx1,vx2,oldcr);
-				c2=count_crossings_2(layers,vx2,vx1,c1);
-				if (c2<c1) {
-					v1.setElementAt(vx2,i);
-					v1.setElementAt(vx1,i+1);
-				}
-			}
-		}
-	}
-
-	/********************************************************************/
-	/*                    minimization of crossings                     */
-	/********************************************************************/
-
-	public Vector min_crossings(Vector layers) {
-		int n,i,l,k,z=0,cr2,cr=count_crossings(layers,Integer.MAX_VALUE);
-		boolean topdown=true,first=true;
-		Enumeration e1,e2;
-		Vector v1,v2,layers2=null,best=layers;
-		Vertex vx1,vx2;
-		n=0;
-		while (n<3 && cr>0) {
-			if (topdown) {
-				/** top-down-traversal **/
-
-				layers2=new Vector(10,10);
-				for (l=0;l<layers.size();l++) {
-					v1=(Vector)(layers.elementAt(l));
-					if (l==0) layers2.addElement(v1.clone());
-					else {
-						v2=new Vector(10,10);
-						layers2.addElement(v2);
-						e1=v1.elements();
-						while (e1.hasMoreElements()) {
-							vx1=(Vertex)(e1.nextElement());
-							k=0;z=0;
-							e2=vx1.getParents();
-							while (e2.hasMoreElements()) {
-								k+=((Vector)(layers2.elementAt(l-1))).indexOf(e2.nextElement());
-								z++;
-							}
-							if (z>0)
-								vx1.setWeight(((double)(k))/z);
-							else if (first)
-								vx1.setWeight(Double.MAX_VALUE);
-							for (i=0;i<v2.size();i++)
-								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
-							if (i==v2.size()) v2.addElement(vx1);
-							else v2.insertElementAt(vx1,i);
-						}
-					}
-				}
-			} else {
-				/** bottom-up-traversal **/
-
-				layers2=new Vector(10,10);
-				for (l=layers.size()-1;l>=0;l--) {
-					v1=(Vector)(layers.elementAt(l));
-					if (l==layers.size()-1) layers2.addElement(v1.clone());
-					else {
-						v2=new Vector(10,10);
-						layers2.insertElementAt(v2,0);
-						e1=v1.elements();
-						while (e1.hasMoreElements()) {
-							vx1=(Vertex)(e1.nextElement());
-							k=0;z=0;
-							e2=vx1.getChildren();
-							while (e2.hasMoreElements()) {
-								k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement());
-								z++;
-							}
-							if (z>0)
-								vx1.setWeight(((double)(k))/z);
-							else if (first)
-								vx1.setWeight(Double.MAX_VALUE);
-							for (i=0;i<v2.size();i++)
-								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
-							if (i==v2.size()) v2.addElement(vx1);
-							else v2.insertElementAt(vx1,i);
-						}
-					}
-				}
-			}
-			//exchangeVertices(layers2,cr);
-			topdown=!topdown;
-			first=false;
-			layers=layers2;
-
-			cr2=count_crossings(layers2,cr);
-			if (cr2<cr) {
-				best=layers2;
-				cr=cr2;					
-			} else n++;
-		}
-
-		while (true) {
-			exchangeVertices(best,cr);
-			cr2=count_crossings(best,cr);
-			if (cr2<cr)
-				cr=cr2;
-			else
-				break;
-		}
-
-		return best;
-	}
-
-	/********************************************************************/
-	/*                   set initial coordinates                        */
-	/********************************************************************/
-
-	public void init_coordinates(Vector layers) {
-		int y=0;
-		Enumeration e1=layers.elements();
-		Enumeration e3=numEdges.elements();
-		while (e1.hasMoreElements()) {
-			Vector v1=(Vector)(e1.nextElement());
-			Enumeration e2=v1.elements();
-			int x=0;
-			while (e2.hasMoreElements()) {
-				Vertex ve=(Vertex)(e2.nextElement());
-				ve.setX(x+ve.box_width2());
-				ve.setY(y);
-				x+=ve.box_width()+20;
-			}
-			y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
-		}
-	}
-
-	/********************************************************************/
-	/*                       pendulum method                            */
-	/********************************************************************/
-
-	public void pendulum(Vector layers) {
-		Vector layers2=new Vector(10,10);
-		Enumeration e1=layers.elements(),e2;
-		int i,j,d1,d2,k,offset,dsum;
-		Region r1,r2;
-		boolean change;
-
-		while (e1.hasMoreElements()) {
-			e2=((Vector)(e1.nextElement())).elements();
-			Vector layer=new Vector(10,10);
-			layers2.addElement(layer);
-			while (e2.hasMoreElements()) {
-				Region r=new Region(this);
-				r.addVertex((Vertex)(e2.nextElement()));
-				layer.addElement(r);
-			}
-		}
-		for (k=0;k<10;k++) {
-			dsum=0;
-			for (j=1;j<layers2.size();j++) {
-				Vector l=(Vector)(layers2.elementAt(j));
-				if (l.size()>=2) {
-					do {
-						change=false;
-						d1=((Region)(l.firstElement())).pred_deflection();
-						for (i=0;i<l.size()-1;i++) {
-							r1=(Region)(l.elementAt(i));
-							r2=(Region)(l.elementAt(i+1));
-							d2=r2.pred_deflection();
-							if (r1.touching(r2) && (d1 <= 0 && d2 < d1 ||
-								d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) {
-								r1.combine(r2);
-								l.removeElement(r2);
-								change=true;
-								d2=r1.pred_deflection();
-							}
-							d1=d2;
-						}
-					} while (change);
-				}
-				for (i=0;i<l.size();i++) {
-					r1=(Region)(l.elementAt(i));
-					d1=r1.pred_deflection();
-					offset=d1;
-					if (d1<0 && i>0) offset=-Math.min(
-						((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1);
-					if (d1>=0 && i<l.size()-1) offset=Math.min(
-						r1.spaceBetween((Region)(l.elementAt(i+1))),d1);
-					r1.move(offset);
-					dsum+=Math.abs(d1);
-				}		
-			}
-			if (dsum==0) break;
-		}
-	}		
-
-	/********************************************************************/
-	/*                      rubberband method                           */
-	/********************************************************************/
-
-	public void rubberband(Vector layers) {
-		Enumeration e1,e2;
-		int i,n,k,d,d2;
-		Vector v;
-		Vertex vx;
-
-		for (k=0;k<10;k++) {
-			e1=layers.elements();
-			while (e1.hasMoreElements()) {
-				v=(Vector)(e1.nextElement());
-				for (i=0;i<v.size();i++) {
-					n=0;d=0;
-					vx=(Vertex)(v.elementAt(i));
-					e2=vx.getChildren();
-					while (e2.hasMoreElements()) {
-						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
-						n++;
-					}
-					e2=vx.getParents();
-					while (e2.hasMoreElements()) {
-						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
-						n++;
-					}
-					d2=(n!=0?d/n:0);
-
-					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) ||
-						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2))
-						vx.setX(vx.getX()+d2);
-				}
-			}
-		}
-	}
-
-	/**** Intersection point of two lines (auxiliary function for calcSplines)   ****/
-	/**** Calculate intersection point of line which is parallel to line (p1,p2) ****/
-	/**** and leads through p5, with line (p3,p4)                                ****/
-
-	Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) {
-		float x=0,y=0,s1=0,s2=0;
-
-		if (p1.x!=p2.x)
-			s1=((float)(p2.y-p1.y))/(p2.x-p1.x);
-		if (p3.x!=p4.x)
-			s2=((float)(p4.y-p3.y))/(p4.x-p3.x);
-		if (p1.x==p2.x) {
-			x=p5.x;
-			y=s2*(p5.x-p3.x)+p3.y;
-		} else if (p3.x==p4.x) {
-			x=p3.x;
-			y=s1*(p3.x-p5.x)+p5.y;
-		} else {
-			x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2);
-			y=s2*(x-p3.x)+p3.y;
-		}
-		return new Point(Math.round(x),Math.round(y));
-	}
-
-	/**** Calculate control points (auxiliary function for calcSplines) ****/
-
-	Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) {
-
-		/*** Points p1 , p2 , p3 define a triangle which encloses the spline.  ***/
-		/*** Check if adjacent boxes (specified by lboxx,rboxx and boxy)       ***/
-		/*** collide with the spline. In this case p1 and p3 are shifted by an ***/
-		/*** appropriate offset before they are returned                       ***/
-
-		int xh1,xh2,bx=0,by=0;
-		boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y;
-		boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y ||
-                              boxy+box_height >= p3.y && boxy+box_height <= p1.y;
-		boolean move = false;
-		Point b;
-
-		xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
-		xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
-
-		if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) {
-			move = true;
-			bx = lboxx;
-			by = boxy + (xh1 < xh2 ? 0 : box_height ) ;
-		} else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) {
-			move = true;
-			bx = rboxx;
-			by = boxy + (xh1 > xh2 ? 0 : box_height ) ;
-		} else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) {
-			move = true;
-			bx = (xh1 <= lboxx ? lboxx : rboxx ) ;
-			by = boxy;
-		} else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) {
-			move = true;
-			bx = (xh2 <= lboxx ? lboxx : rboxx ) ;
-			by = boxy+box_height;
-		}
-		b=new Point(bx,by);
-		if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b));
-		else return new Points(p1,p3);
-	}
-
-	/********************************************************************/
-	/*                        calculate splines                         */
-	/********************************************************************/
-
-	public void calcSplines(Vector layers) {
-		Enumeration e2,e1=vertices.elements();
-		Vertex vx1,vx2,vx3;
-		Vector pos,layer;
-		int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc;
-
-		while (e1.hasMoreElements()) {
-			vx1=(Vertex)(e1.nextElement());
-			if (!vx1.isDummy()) {
-				e2=vx1.getChildren();
-				while (e2.hasMoreElements()) {
-					vx2=(Vertex)(e2.nextElement());
-					if (vx2.isDummy()) {
-						vx3=vx2;
-						/**** convert edge to spline ****/
-						pos=new Vector(10,10);
-						x1=vx1.getX();
-						y1=vx1.getY()+box_height;
-
-						do {
-							/*** calculate position of control points ***/
-							x2=vx2.getX();
-							y2=vx2.getY();
-							layer=(Vector)(layers.elementAt(vx2.getDegree()));
-							k=layer.indexOf(vx2);
-							vx2=(Vertex)((vx2.getChildren()).nextElement());
-							x3=vx2.getX();
-							y3=vx2.getY();
-							spc=0;
-							leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
-								Integer.MIN_VALUE:
-								((Vertex)(layer.elementAt(k-1))).rightX()+spc;
-							rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ?
-								Integer.MAX_VALUE:
-								((Vertex)(layer.elementAt(k+1))).leftX()-spc;
-							xh=x2+box_height*(x3-x2)/(y3-y2);
-							if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) {
-								/* top control point */
-								pos.addElement(new Integer(1));
-								y1=y2;
-							} else {
-								xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1);
-								if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx))
-									/* bottom control point */
-									pos.addElement(new Integer(2));
-								else
-									/* two control points needed */
-									pos.addElement(new Integer(3));
-								y1=y2+box_height;
-							}
-							x1=x2;
-						} while (vx2.isDummy());
-						pos.addElement(new Integer(1));
-
-						/**** calculate triangles ****/
-						vx2=vx3;
-
-						int pos1,pos2,i=0;
-						Vector pts=new Vector(10,10);
-						int lboxx,rboxx,boxy;
-
-						x1=vx1.getX();
-						y1=vx1.getY()+box_height;
-						pts.addElement(new Point(x1,y1)); /** edge starting point **/
-						do {
-							x2=vx2.getX();
-							y2=vx2.getY();
-							pos1=((Integer)(pos.elementAt(i))).intValue();
-							pos2=((Integer)(pos.elementAt(i+1))).intValue();
-							i++;
-							layer=(Vector)(layers.elementAt(vx2.getDegree()));
-							k=layer.indexOf(vx2);
-							boxy=vx2.getY();
-							vx2=(Vertex)((vx2.getChildren()).nextElement());
-							x3=vx2.getX();
-							y3=vx2.getY();
-							if (pos1==2) y2+=box_height;
-							if (pos2==2) y3+=box_height;
-
-							lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ?
-								Integer.MIN_VALUE :
-								((Vertex)(layer.elementAt(k-1))).rightX();
-
-							rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ?
-								Integer.MAX_VALUE :
-								((Vertex)(layer.elementAt(k+1))).leftX();
-
-							Point p1,p2,p3;
-							Points ps;
-
-							p1 = new Point((x1+x2)/2,(y1+y2)/2);
-
-							if (pos1<=2) {
-								/** one control point **/
-								p2 = new Point(x2,y2);
-								ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy);
-								pts.addElement(ps.p);
-								pts.addElement(p2);
-								pts.addElement(ps.q);
-							} else {
-								/** two control points **/
-								p2 = new Point(x2,y2-box_height);
-								p3 = new Point(x2,y2+box_height2);
-								ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy);
-								pts.addElement(ps.p);
-								pts.addElement(p2);
-								pts.addElement(ps.q);
-								p2 = new Point(x2,y2+box_height*2);
-								ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2),
-								               lboxx,rboxx,boxy);
-								pts.addElement(ps.p);
-								pts.addElement(p2);
-								pts.addElement(ps.q);
-							}
-							x1=p2.x;
-							y1=p2.y;
-						} while (vx2.isDummy());
-
-						pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/
-						splines.addElement(new Spline(pts));
-					}
-				}
-			}
-		}
-	}
-
-	/********************************************************************/
-	/*                      calculate bounding box                      */
-	/********************************************************************/
-
-	public void calcBoundingBox() {
-		min_y=min_x=Integer.MAX_VALUE;
-		max_y=max_x=Integer.MIN_VALUE;
-
-		Enumeration e1=vertices.elements();
-		Vertex v;
-
-		while (e1.hasMoreElements()) {
-			v=(Vertex)(e1.nextElement());
-			min_x=Math.min(min_x,v.leftX());
-			max_x=Math.max(max_x,v.rightX());
-			min_y=Math.min(min_y,v.getY());
-			max_y=Math.max(max_y,v.getY()+box_height);
-		}
-		min_x-=20;
-		min_y-=20;
-		max_x+=20;
-		max_y+=20;
-	}
-
-	/********************************************************************/
-	/*                           draw graph                             */
-	/********************************************************************/
-					 
-	public void draw(Graphics g) {
-		if (box_height==0) layout(g);
-
-		g.translate(-min_x,-min_y);
-
-		Enumeration e1=vertices.elements();
-		while (e1.hasMoreElements())
-			((Vertex)(e1.nextElement())).draw(g);
-
-		e1=splines.elements();
-		while (e1.hasMoreElements())
-			((Spline)(e1.nextElement())).draw(g);
-	}
-
-	/********************************************************************/
-	/*               return vertex at position (x,y)                    */
-	/********************************************************************/
-
-	public Vertex vertexAt(int x,int y) {
-		Enumeration e1=vertices.elements();
-		while (e1.hasMoreElements()) {
-			Vertex v=(Vertex)(e1.nextElement());
-			if (v.contains(x,y)) return v;
-		}
-		return null;
-	}
-
-	/********************************************************************/
-	/*       encode list of vertices (as array of vertice numbers)      */
-	/********************************************************************/
-
-	public Vector encode(Vector v) {
-		Vector code=new Vector(10,10);
-		Enumeration e1=v.elements();
-
-		while (e1.hasMoreElements()) {
-			Vertex vx=(Vertex)(e1.nextElement());
-			if (vx.getNumber()>=0)
-				code.addElement(new Integer(vx.getNumber()));
-		}
-		return code;
-	}
-
-	/********************************************************************/
-	/*                      get vertex with number n                    */
-	/********************************************************************/
-
-	public Vertex getVertexByNum(int x) {
-		Enumeration e1=vertices.elements();
-
-		while (e1.hasMoreElements()) {
-			Vertex vx=(Vertex)(e1.nextElement());
-			if (vx.getNumber()==x) return vx;
-		}
-		return null;
-	}
-
-	/********************************************************************/
-	/*                      decode list of vertices                     */
-	/********************************************************************/
-
-	public Vector decode(Vector code) {
-		Enumeration e1=code.elements();
-		Vector vec=new Vector(10,10);
-
-		while (e1.hasMoreElements()) {
-			int i=((Integer)(e1.nextElement())).intValue();
-			//Vertex vx=getVertexByNum(i);
-			//if (vx!=null) vec.addElement(vx);
-			vec.addElement(vertices2[i]);
-		}
-		return vec;
-	}
-
-	/********************************************************************/
-	/*                       collapse vertices                          */
-	/********************************************************************/
-
-	public void collapse(Vector vs,String name,Vector inflate) {
-		Enumeration e1,e2,e3;
-		boolean nonempty=false;
-		Vertex vx3,vx2,vx1;
-		
-		e1=vertices.elements();
-
-		vx1=new NormalVertex(name);
-		vx1.setInflate(inflate);
-
-		while (e1.hasMoreElements()) {
-			vx2=(Vertex)(e1.nextElement());
-
-			if (vs.indexOf(vx2)<0) {
-				e2=vx2.getParents();
-				while (e2.hasMoreElements()) {
-					vx3=(Vertex)(e2.nextElement());
-					if (vs.indexOf(vx3)>=0) {
-						if (!vx1.isChild(vx2))
-							vx1.addChild(vx2);
-						vx3.removeChild(vx2);
-					}
-				}
-
-				e2=vx2.getChildren();
-				while (e2.hasMoreElements()) {
-					vx3=(Vertex)(e2.nextElement());
-					if (vs.indexOf(vx3)>=0) {
-						if (!vx2.isChild(vx1))
-							vx2.addChild(vx1);
-						vx2.removeChild(vx3);
-					}
-				}
-			} else { nonempty=true; }
-		}
-
-		e1=vs.elements();
-		while (e1.hasMoreElements())
-			try {
-				removeVertex((Vertex)(e1.nextElement()));
-			} catch (NoSuchElementException exn) {}
-
-		if (nonempty) addVertex(vx1);
-	}
-
-	/********************************************************************/
-	/*                      PostScript output                           */
-	/********************************************************************/
-
-	public void PS(String fname,boolean printable) throws IOException {
-		FileOutputStream f = new FileOutputStream(fname);
-		PrintWriter p = new PrintWriter(f, true);
-
-		if (printable)
-			p.println("%!PS-Adobe-2.0\n\n%%BeginProlog");
-		else {
-			p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait");
-			p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y);
-			p.println("%%EndComments\n\n%%BeginProlog");
-		}
-		p.println("/m { moveto } def /l { lineto } def /n { newpath } def");
-		p.println("/s { stroke } def /c { curveto } def");
-		p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub");
-		p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub");
-		p.println("2 div 9 index add 2 index add m pop pop pop pop");
-		p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto");
-		p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def");
-		p.println("%%EndProlog\n");
-		if (printable) {
-			int hsize=max_x-min_x;
-			int vsize=max_y-min_y;
-			if (hsize>vsize) {
-				// Landscape output
-				double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize));
-				double trans_x=50+max_y*scale+(500-scale*vsize)/2.0;
-				double trans_y=50+max_x*scale+(750-scale*hsize)/2.0;
-				p.println(trans_x+" "+trans_y+" translate");
-				p.println("-90 rotate");
-				p.println(scale+" "+(-scale)+" scale");
-			} else {
-				// Portrait output
-				double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize));
-				double trans_x=50-min_x*scale+(500-scale*hsize)/2.0;
-				double trans_y=50+max_y*scale+(750-scale*vsize)/2.0;
-				p.println(trans_x+" "+trans_y+" translate");
-				p.println(scale+" "+(-scale)+" scale");
-			}
-		} else
-			p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale");
-
-		p.println("/Helvetica findfont 12 scalefont setfont");
-		p.println("0.5 setlinewidth");
-
-		Enumeration e1=vertices.elements();
-		while (e1.hasMoreElements())
-			((Vertex)(e1.nextElement())).PS(p);
-
-		e1=splines.elements();
-		while (e1.hasMoreElements())
-			((Spline)(e1.nextElement())).PS(p);
-
-		if (printable) p.println("showpage");
-
-		f.close();
-	}
-}
-
-/**** Return value of function calcPoint ****/
-
-class Points {
-	public Point p,q;
-
-	public Points(Point p1,Point p2) {
-		p=p1;q=p2;
-	}
-}
-
--- a/lib/browser/GraphBrowser/GraphBrowser.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,215 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/GraphBrowser.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This is the graph browser's main class. It contains the "main(...)"
-  method, which is used for the stand-alone version, as well as
-  "init(...)", "start(...)" and "stop(...)" methods which are used for
-  the applet version.
-  Note: GraphBrowser is designed for the 1.1.x version of the JDK.
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.awt.*;
-import java.applet.*;
-import java.io.*;
-import java.util.*;
-import java.net.*;
-import awtUtilities.*;
-
-public class GraphBrowser extends Applet {
-	GraphView gv;
-	TreeBrowser tb=null;
-	String gfname;
-
-	static boolean isApplet;
-	static Frame f;
-
-	public GraphBrowser(String name) {
-		gfname=name;
-	}
-
-	public GraphBrowser() {}
-
-	public void showWaitMessage() {
-		if (isApplet)
-			getAppletContext().showStatus("calculating layout, please wait ...");
-		else {
-			f.setCursor(new Cursor(Cursor.WAIT_CURSOR));
-		}
-	}
-
-	public void showReadyMessage() {
-		if (isApplet)
-			getAppletContext().showStatus("ready !");
-		else {
-			f.setCursor(new Cursor(Cursor.DEFAULT_CURSOR));
-		}
-	}
-
-	public void viewFile(String fname) {
-		try {
-			if (isApplet)
-				getAppletContext().showDocument(new URL(getDocumentBase(), fname), "_blank");
-			else {
-				String path = gfname.substring(0, gfname.lastIndexOf('/') + 1);
-				Reader rd;
-				BufferedReader br;
-				String line, text = "";
-
-				try {
-					rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
-				} catch (Exception exn) {
-					rd = new FileReader(path + fname);
-				}
-				br = new BufferedReader(rd);
-
-				while ((line = br.readLine()) != null)
-					text += line + "\n";
-
-				if (fname.endsWith(".html")) {
-					/**** convert HTML to text (just a quick hack) ****/
-
-					String buf="";
-					char[] text2,text3;
-					int i,j=0;
-					boolean special=false, html=false;
-					char ctrl;
-
-					text2 = text.toCharArray();
-					text3 = new char[text.length()];
-					for (i = 0; i < text.length(); i++) {
-						char c = text2[i];
-						if (c == '&') {
-							special = true;
-							buf = "";
-						} else if (special) {
-							if (c == ';') {
-								special = false;
-								if (buf.equals("lt"))
-									text3[j++] = '<';
-								else if (buf.equals("gt"))
-									text3[j++] = '>';
-								else if (buf.equals("amp"))
-									text3[j++] = '&';
-							} else
-								buf += c;
-						} else if (c == '<') {
-							html = true;
-							ctrl = text2[i+1];
-						} else if (c == '>')
-							html = false;
-						else if (!html)
-							text3[j++] = c;
-					}
-					text = String.valueOf(text3);
-				}
-							
-				Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
-				f.setSize(500,600);
-				f.show();
-			}
-		} catch (Exception exn) {
-			System.err.println("Can't read file "+fname);
-		}
-	}
-				
-	public void PS(String fname,boolean printable) throws IOException {
-		gv.PS(fname,printable);
-	}
-
-	public boolean isEmpty() {
-		return tb==null;
-	}
-
-	public void initBrowser(InputStream is, boolean noAWT) {
-		try {
-			Font font = noAWT ? null : new Font("Helvetica", Font.PLAIN, 12);
-			TreeNode tn = new TreeNode("Root", "", -1, true);
-			gv = new GraphView(new Graph(is, tn), this, font);
-			tb = new TreeBrowser(tn, gv, font);
-			gv.setTreeBrowser(tb);
-			Vector v = new Vector(10,10);
-			tn.collapsedDirectories(v);
-			gv.collapseDir(v);
-
-			ScrollPane scrollp1 = new ScrollPane();
-			ScrollPane scrollp2 = new ScrollPane();
-			scrollp1.add(gv);
-			scrollp2.add(tb);
-			scrollp1.getHAdjustable().setUnitIncrement(20);
-			scrollp1.getVAdjustable().setUnitIncrement(20);
-			scrollp2.getHAdjustable().setUnitIncrement(20);
-			scrollp2.getVAdjustable().setUnitIncrement(20);
-			Component gv2 = new Border(scrollp1, 3);
-			Component tb2 = new Border(scrollp2, 3);
-			GridBagLayout gridbag = new GridBagLayout();
-			GridBagConstraints cnstr = new GridBagConstraints();
-			setLayout(gridbag);
-			cnstr.fill = GridBagConstraints.BOTH;
-			cnstr.insets = new Insets(5,5,5,5);
-			cnstr.weightx = 1;
-			cnstr.weighty = 1;
-			cnstr.gridwidth = 1;
-			gridbag.setConstraints(tb2,cnstr);
-			add(tb2);
-			cnstr.weightx = 2.5;
-			cnstr.gridwidth = GridBagConstraints.REMAINDER;
-			gridbag.setConstraints(gv2,cnstr);
-			add(gv2);
-		} catch (IOException exn) {
-			System.err.println("\nI/O error while reading graph file.");
-		} catch (ParseError exn) {
-			System.err.println("\nParse error in graph file:");
-			System.err.println(exn.getMessage());
-			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
-		}
-	}		
-
-	public void init() {
-		isApplet=true;
-		gfname=getParameter("graphfile");
-		try {
-			InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
-			initBrowser(is, false);
-			is.close();
-		} catch (MalformedURLException exn) {
-			System.err.println("Invalid URL: "+gfname);
-		} catch (IOException exn) {
-			System.err.println("I/O error while reading "+gfname+".");
-		}
-	}
-
-	public static void main(String[] args) {
-		isApplet=false;
-		try {
-			GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
-			if (args.length > 0) {
-				InputStream is=new FileInputStream(args[0]);
-				gb.initBrowser(is, args.length > 1);
-				is.close();
-			}
-			if (args.length > 1) {
-                            try {
-			      if (args[1].endsWith(".ps"))
-                                gb.gv.PS(args[1], true);
-                              else if (args[1].endsWith(".eps"))
-                                gb.gv.PS(args[1], false);
-                              else
-                                System.err.println("Unknown file type: " + args[1]);
-                            } catch (IOException exn) {
-                              System.err.println("Unable to write file " + args[1]);
-                            }
-                        } else {
-			    f=new GraphBrowserFrame(gb);
-			    f.setSize(700,500);
-			    f.show();
-                        }
-		} catch (IOException exn) {
-			System.err.println("Can't open graph file "+args[0]);
-		}
-	}
-}
-
--- a/lib/browser/GraphBrowser/GraphBrowserFrame.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/GraphBrowserFrame.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=2:
-
-  This class is the frame for the stand-alone application. It contains
-  methods for handling menubar events.
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.awt.*;
-import java.awt.event.*;
-import java.io.*;
-import awtUtilities.*;
-
-public class GraphBrowserFrame extends Frame implements ActionListener {
-	GraphBrowser gb;
-	MenuItem i1, i2;
-	String graphDir, psDir;
-
-	public void checkMenuItems() {
-		if (gb.isEmpty()) {
-			i1.setEnabled(false);
-			i2.setEnabled(false);
-		} else {
-			i1.setEnabled(true);
-			i2.setEnabled(true);
-		}
-	}
-
-	public void actionPerformed(ActionEvent evt) {
-		String label = evt.getActionCommand();
-		if (label.equals("Quit"))
-			System.exit(0);
-		else if (label.equals("Export to PostScript")) {
-			PS(true, label);
-			return;
-		} else if (label.equals("Export to EPS")) {
-			PS(false, label);
-			return;
-		} else if (label.equals("Open ...")) {
-			FileDialog fd = new FileDialog(this, "Open graph file", FileDialog.LOAD);
-			if (graphDir != null)
-				fd.setDirectory(graphDir);
-			fd.setVisible(true);
-			if (fd.getFile() == null) return;
-			graphDir = fd.getDirectory();
-			String fname = graphDir + fd.getFile();
-			GraphBrowser gb2 = new GraphBrowser(fname);
-			try {
-				InputStream is = new FileInputStream(fname);
-				gb2.initBrowser(is, false);
-				is.close();
-			} catch (IOException exn) {
-				String button[] = {"OK"};
-				MessageDialog md = new MessageDialog(this, "Error",
-					"Can't open file " + fname + ".", button);
-				md.setSize(350, 200);
-				md.setVisible(true);
-				return;
-			}
-			remove(gb);
-			add("Center", gb2);
-			gb = gb2;
-			checkMenuItems();
-			validate();
-		}
-	}
-
-	public void PS(boolean printable,String label) {
-		FileDialog fd=new FileDialog(this,label,FileDialog.SAVE);
-		if (psDir!=null)
-			fd.setDirectory(psDir);
-		fd.setVisible(true);
-		if (fd.getFile()==null) return;
-		psDir=fd.getDirectory();
-		String fname=psDir+fd.getFile();
-
-		if ((new File(fname)).exists()) {
-			String buttons[]={"Overwrite","Cancel"};
-			MessageDialog md=new MessageDialog(this,"Warning",
-			      "Warning: File "+fname+" already exists. Overwrite?",
-			      buttons);
-			md.setSize(350,200);
-			md.setVisible(true);
-			if (md.getText().equals("Cancel")) return;
-		}
-
-		try {
-			gb.PS(fname,printable);
-		} catch (IOException exn) {
-			String button[]={"OK"};
-			MessageDialog md=new MessageDialog(this,"Error",
-			      "Unable to write file "+fname+".",button);
-			md.setSize(350,200);
-			md.setVisible(true);
-		}
-	}
-
-	public GraphBrowserFrame(GraphBrowser br) {
-		super("GraphBrowser");
-		MenuItem i3, i4;
-		gb = br;
-		MenuBar mb = new MenuBar();
-		Menu m1 = new Menu("File");
-		m1.add(i3 = new MenuItem("Open ..."));
-		m1.add(i1 = new MenuItem("Export to PostScript"));
-		m1.add(i2 = new MenuItem("Export to EPS"));
-		m1.add(i4 = new MenuItem("Quit"));
-		i1.addActionListener(this);
-		i2.addActionListener(this);
-		i3.addActionListener(this);
-		i4.addActionListener(this);
-		checkMenuItems();
-		mb.add(m1);
-		setMenuBar(mb);
-		add("Center", br);
-    addWindowListener( new WindowAdapter() {
-      public void windowClosing(WindowEvent e) {
-        System.exit(0);
-      }
-    });
-	}
-}
--- a/lib/browser/GraphBrowser/GraphView.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-/***************************************************************************
-  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 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) {}
-}
--- a/lib/browser/GraphBrowser/NormalVertex.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/NormalVertex.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This class represents an ordinary vertex. It contains methods for
-  drawing and PostScript output.
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.util.*;
-import java.awt.*;
-import java.io.*;
-
-class NormalVertex extends Vertex {
-	String label="",path="",dir="",ID="";
-	Vector up,down,inflate=null;
-
-	public Object clone() {
-		Vertex ve=new NormalVertex(label);
-                ve.setID(ID);
-		ve.setNumber(getNumber());
-		ve.setUp(getUp());ve.setDown(getDown());
-		ve.setX(getX());ve.setY(getY());
-		ve.setPath(getPath());
-		return ve;
-	}
-
-	/*** Constructor ***/
-
-	public NormalVertex(String s) { label=s; }
-
-	public void setInflate(Vector v) { inflate=v; }
-
-	public Vector getInflate() { return inflate; }
-
-	public Vector getUp() { return up; }
-
-	public void setUp(Vector v) { up=v; }
-
-	public Vector getDown() { return down; }
-
-	public void setDown(Vector v) { down=v; }
-
-	public String getLabel() {return label;}
-
-	public void setLabel(String s) {label=s;}
-
-	public void setID(String s) { ID=s; }
-
-        public String getID() { return ID; }
-
-	public String getPath() { return path;}
-
-	public void setPath(String p) { path=p; }
-
-	public String getDir() { return dir; }
-
-	public void setDir(String d) { dir=d; }
-
-	public int leftX() { return getX()-box_width2(); }
-
-	public int rightX() { return getX()+box_width2(); }
-
-	public void drawBox(Graphics g,Color boxColor) {
-		FontMetrics fm = g.getFontMetrics(g.getFont());
-		int h=fm.getAscent()+fm.getDescent();
-
-		g.setColor(boxColor);
-		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
-		g.setColor(Color.black);
-		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
-		if (getNumber()<0)
-			g.setColor(Color.red);
-
-		g.drawString(label,
-		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
-				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
-	}
-
-	public void removeButtons(Graphics g) {
-		drawBox(g,Color.lightGray);
-	}
-
-	public void draw(Graphics g) {
-		drawBox(g,Color.lightGray);
-		g.setColor(Color.black);
-		Enumeration e1=getChildren();
-		while (e1.hasMoreElements()) {
-			Vertex v=(Vertex)(e1.nextElement());
-			if (!v.isDummy())
-				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
-		}
-	}
-
-	public boolean contains(int x,int y) {
-		return (x>=leftX() && x<=rightX() && y>=getY() &&
-                        y<=getY()+gra.box_height);
-	}
-
-	public boolean leftButton(int x,int y) {
-		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
-	}
-
-	public boolean rightButton(int x,int y) {
-		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
-	}
-
-	public void drawButtons(Graphics g) {
-		if (getNumber()<0) return;
-
-		int l=gra.box_height*2/3,d=gra.box_height/6;
-		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
-		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
-		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
-		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
-
-		if (getParents().hasMoreElements()) {
-			g.setColor(Color.gray);
-			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
-			g.setColor(getUp()!=null ? Color.red : Color.green);
-			g.fillPolygon(up_x,up_y,3);
-		}
-		if (getChildren().hasMoreElements()) {
-			g.setColor(Color.gray);
-			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
-			g.setColor(getDown()!=null ? Color.red : Color.green);
-			g.fillPolygon(down_x,down_y,3);
-		}
-		g.setColor(Color.black);
-	}
-
-	public void PS(PrintWriter p) {
-		p.print(leftX()+" "+getY()+" "+box_width()+" "+
-		        gra.box_height+" (");
-		for (int i=0;i<label.length();i++)
-		{
-			if (("()\\").indexOf(label.charAt(i))>=0)
-				p.print("\\");
-			p.print(label.charAt(i));
-		}
-		p.println(") b");
-
-		Enumeration e1=getChildren();
-		while (e1.hasMoreElements()) {
-			Vertex v=(Vertex)(e1.nextElement());
-			if (!v.isDummy())
-				p.println("n "+getX()+" "+(getY()+gra.box_height)+
-				" m "+v.getX()+" "+v.getY()+" l s");
-		}
-	}	
-}
-		
--- a/lib/browser/GraphBrowser/ParseError.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-package GraphBrowser;
-
-class ParseError extends Exception {
-	public ParseError(String s) { super(s); }
-}
--- a/lib/browser/GraphBrowser/Region.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/Region.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This is an auxiliary class which is used by the layout algorithm when
-  calculating coordinates with the "pendulum method". A "region" is a
-  group of nodes which "stick together".
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.util.*;
-
-class Region {
-	Vector vertices=new Vector(10,10);
-	Graph gra;
-
-	public Region(Graph g) { gra=g; }
-
-	public void addVertex(Vertex v) {
-		vertices.addElement(v);
-	}
-
-	public Enumeration getVertices() {
-		return vertices.elements();
-	}
-
-	public int pred_deflection() {
-		float d1=0;
-		int n=0;
-		Enumeration e1=vertices.elements();
-		while (e1.hasMoreElements()) {
-			float d2=0;
-			int p=0;
-			n++;
-			Vertex v=(Vertex)(e1.nextElement());
-			Enumeration e2=v.getParents();
-			while (e2.hasMoreElements()) {
-				p++;
-				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
-			}
-			if (p>0) d1+=d2/p;
-		}
-		return (int)(Math.round(d1/n));
-	}
-
-	public int succ_deflection() {
-		float d1=0;
-		int n=0;
-		Enumeration e1=vertices.elements();
-		while (e1.hasMoreElements()) {
-			float d2=0;
-			int p=0;
-			n++;
-			Vertex v=(Vertex)(e1.nextElement());
-			Enumeration e2=v.getChildren();
-			while (e2.hasMoreElements()) {
-				p++;
-				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
-			}
-			if (p>0) d1+=d2/p;
-		}
-		return (int)(Math.round(d1/n));
-	}
-
-	public void move(int x) {
-		Enumeration e1=vertices.elements();
-		while (e1.hasMoreElements()) {
-			Vertex v=(Vertex)(e1.nextElement());
-			v.setX(v.getX()+x);
-		}
-	}
-
-	public void combine(Region r2) {
-		Enumeration e1=r2.getVertices();
-		while (e1.hasMoreElements()) addVertex((Vertex)(e1.nextElement()));
-	}
-
-	public int spaceBetween(Region r2) {
-		return ((Vertex)(r2.getVertices().nextElement())).leftX()-
-			((Vertex)(vertices.lastElement())).rightX()-
-			20;
-	}
-
-	public boolean touching(Region r2) {
-		return spaceBetween(r2)==0;
-	}
-}
--- a/lib/browser/GraphBrowser/Spline.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/Spline.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This class is used for drawing spline curves (which are not yet
-  supported by the Java AWT).
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.awt.*;
-import java.util.*;
-import java.io.*;
-
-class SplineSection {
-
-	/*** Section of a spline function ***/
-
-	double x_b,x_c,x_d;
-	double y_b,y_c,y_d;
-	int dx,dy;
-
-	public SplineSection(double xb,double xc,double xd,
-		double yb,double yc,double yd,int dx2,int dy2) {
-		x_b=xb;x_c=xc;x_d=xd;
-		y_b=yb;y_c=yc;y_d=yd;
-		dx=dx2;dy=dy2;
-	}
-
-	public Point draw(Graphics g,Point s) {
-		double m;
-		int s_x,s_y,e_x=0,e_y=0;
-		int x,y;
-
-		s_x=s.x;s_y=s.y;
-		if (dx>=dy) {
-			if (dx==0) return s;
-			m=1/((double)dx);
-			for (x=0;x<dx;x++) {
-				e_x=(int)(Math.round((x_b*x*m+x_c)*x*m+x_d));
-				e_y=(int)(Math.round((y_b*x*m+y_c)*x*m+y_d));
-				g.drawLine(s_x,s_y,e_x,e_y);
-				s_x=e_x;s_y=e_y;
-			}
-		} else {
-			m=1/((double)dy);
-			for (y=0;y<dy;y++) {
-				e_x=(int)(Math.round((x_b*y*m+x_c)*y*m+x_d));
-				e_y=(int)(Math.round((y_b*y*m+y_c)*y*m+y_d));
-				g.drawLine(s_x,s_y,e_x,e_y);
-				s_x=e_x;s_y=e_y;
-			}
-		}
-		return new Point(e_x,e_y);
-	}
-}
-
-public class Spline {
-
-	Vector sections;
-	Vector points;
-	Point start,end;
-
-	public Spline(Vector pts) {
-		int i;
-		double d0,d1,d2,d3;
-		Point p0,p1,p2;
-		SplineSection s;
-		
-		start=(Point)(pts.firstElement());
-		end=(Point)(pts.lastElement());
-
-		sections=new Vector(10,10);
-		for (i=1;i<=pts.size()-4;i+=3) {
-			p0=(Point)(pts.elementAt(i));
-			p1=(Point)(pts.elementAt(i+1));
-			p2=(Point)(pts.elementAt(i+2));
-			s=new SplineSection(
-				(double)(p2.x-2*p1.x+p0.x),
-				2.0*(p1.x-p0.x),
-				(double)(p0.x),
-
-				(double)(p2.y-2*p1.y+p0.y),
-				2.0*(p1.y-p0.y),
-				(double)(p0.y),
-
-				Math.abs(p2.x-p0.x),
-				Math.abs(p2.y-p0.y)
-			);
-
-			sections.addElement(s);
-		}
-		points=pts;
-	}
-
-	public void draw(Graphics g) {
-		Enumeration e1=sections.elements();
-		Point p=start;
-
-		while (e1.hasMoreElements())
-			p=((SplineSection)(e1.nextElement())).draw(g,p);
-		g.drawLine(p.x,p.y,end.x,end.y);
-	}
-
-	public void PS(PrintWriter p) {
-		Point p0,p1,p2;
-		int i;
-
-		p.println("n "+start.x+" "+start.y+" m");
-		for (i=1;i<=points.size()-4;i+=3) {
-			p0=(Point)(points.elementAt(i));
-			p1=(Point)(points.elementAt(i+1));
-			p2=(Point)(points.elementAt(i+2));
-			p.println(p0.x+" "+p0.y+" l");
-			p.println(p0.x+" "+p0.y+" "+p1.x+" "+p1.y+" "+p2.x+" "+p2.y+" c");
-		}
-		p.println(end.x+" "+end.y+" l s");
-	}
-}
--- a/lib/browser/GraphBrowser/TreeBrowser.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-/***************************************************************************
-  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 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();
-		}
-	}
-}
-
--- a/lib/browser/GraphBrowser/TreeNode.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/TreeNode.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This class contains methods for storing and manipulating directory
-  trees (e.g. collapsing / uncollapsing directory branches).
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.awt.*;
-import java.util.*;
-
-
-public class TreeNode
-{
-	int starty,endy,number;
-	String name,path;
-
-	Vector leaves=new Vector(10,10);
-	boolean unfold=false;
-
-	public void insertNode(String n,String d,String p,int num,boolean u) {
-		if (d.length()==0) {
-			leaves.addElement(new TreeNode(n,p,num));
-			unfold=unfold||u;
-		} else {
-			unfold=unfold||u;
-			String str1,str2;
-			if (d.indexOf('/')<0) {
-				str1=d;str2="";
-			} else {
-				str1=d.substring(0,d.indexOf('/'));
-				str2=d.substring(d.indexOf('/')+1);
-			}
-
-			Enumeration e1=leaves.elements();
-			TreeNode nd=null;
-
-			while (e1.hasMoreElements()) {
-				TreeNode nd2=(TreeNode)(e1.nextElement());
-				if (nd2.name.equals(str1)) {
-					nd=nd2;break;
-				}
-			}
-			if (nd==null) {
-				nd=new TreeNode(str1,"",-1);
-				leaves.addElement(nd);
-			}
-			nd.insertNode(n,str2,p,num,u);
-		}
-	}
-
-	public TreeNode(String n,String p,int num) {
-		name=n;
-		path=p;
-		number=num;
-	}
-
-	public TreeNode(String n,String p,int num,boolean u) {
-		this(n,p,num);
-		unfold=u;
-	}	
-
-	public int getNumber() { return number; }
-
-	public TreeNode lookup(int y)
-	{
-		if (y>=starty && y<endy) return this;
-		else
-		if (unfold)
-			for (int i=0;i<leaves.size();i++)
-			{
-				TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
-				if (t!=null) return t;
-			}
-		return null;
-	}
-
-	public boolean select()
-	{
-		if (!leaves.isEmpty()) {
-			if (unfold) collapse();
-			else unfold=true;
-			return true;
-		}
-		return false; 
-	}
-
-	public void collapse()
-	{
-		unfold=false;
-		/*
-		for(int i=0;i<leaves.size();i++)
-			((Tree)leaves.elementAt(i)).collapse();
-		*/
-	}
-
-	void collapsedNodes(Vector v) {
-		if (number>=0) v.addElement(new Integer(number));
-		Enumeration e1=leaves.elements();
-		while (e1.hasMoreElements())
-			((TreeNode)(e1.nextElement())).collapsedNodes(v);
-	}
-
-	public void collapsedDirectories(Vector v) {
-		if (!unfold) {
-			Vector v2=new Vector(10,10);
-			v.addElement(new Directory(this,name,v2));
-			collapsedNodes(v2);
-		} else {
-			Enumeration e1=leaves.elements();
-			while (e1.hasMoreElements()) {
-				TreeNode tn=(TreeNode)(e1.nextElement());
-				if (!tn.leaves.isEmpty())
-					tn.collapsedDirectories(v);
-			}
-		}
-	}
-
-	public Dimension draw(Graphics g,int x,int y,TreeNode t)
-	{
-		FontMetrics fm=g.getFontMetrics(g.getFont());
-		int h=fm.getHeight();
-		int e=(int) (h / 10) + 1;
-		int down_x[]={x + e, x + h - e, x + (int)(h / 2)};
-		int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e};
-		int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e};
-		int right_y[]={y + e, y + (int)(h / 2), y + h - e};
-		int dx=0;
-
-		if (unfold)
-		{
-			g.setColor(Color.green);
-			g.fillPolygon(down_x,down_y,3);
-			g.setColor(Color.black);
-			g.drawString(name,x+h+4,y+fm.getAscent());
-			starty=y;endy=y+h;
-			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
-			y+=h+5;
-			for(int i=0;i<leaves.size();i++)
-			{
-				Dimension d=((TreeNode)leaves.elementAt(i)).draw(g,x+h+4,y,t);
-				y=d.height;
-				dx=Math.max(dx,d.width);
-			}
-		}
-		else
-		{
-			g.setColor(leaves.isEmpty() ? Color.blue : Color.red);
-			g.fillPolygon(right_x,right_y,3);
-			if (this==t && leaves.isEmpty())
-			{
-				g.setColor(Color.white);
-				g.fillRect(x+h+4,y,fm.stringWidth(name),h);
-			}
-			g.setColor(Color.black);
-			g.drawString(name,x+h+4,y+fm.getAscent());
-			starty=y;endy=y+h;
-			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
-			y+=h+5;
-		}
-		return new Dimension(dx,y);
-	}
-}
-
-
--- a/lib/browser/GraphBrowser/Vertex.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-/***************************************************************************
-  Title:      GraphBrowser/Vertex.java
-  Author:     Stefan Berghofer, TU Muenchen
-  Options:    :tabSize=4:
-
-  This class contains attributes and methods common to all kinds of
-  vertices (e.g. coordinates, successors, predecessors).
-***************************************************************************/
-
-package GraphBrowser;
-
-import java.util.*;
-import java.awt.*;
-import java.io.*;
-
-abstract class Vertex {
-	Vector children=new Vector(10,10);
-	Vector parents=new Vector(10,10);
-	int degree=0;
-	int number=-1;
-	double weight=0;
-	int x,y;
-	Graph gra;
-
-	public abstract Object clone();
-
-	public void setGraph(Graph g) { gra=g; }
-
-	public int countChildren() { return children.size(); }
-
-	/** getInflate returns a vector of vertices which get **/
-	/** inflated again if the user clicks on this vertex  **/
-
-	public void setInflate(Vector v) {}
-
-	public Vector getInflate() { return null; }
-
-	/** getUp returns a vector of vertices which get inflated   **/
-	/** again, if the user clicks on this vertex's upward arrow **/
-
-	public Vector getUp() { return null; }
-
-	public void setUp(Vector v) {}
-
-	/** getUp returns a vector of vertices which get inflated     **/
-	/** again, if the user clicks on this vertex's downward arrow **/
-
-	public Vector getDown() { return null; }
-
-	public void setDown(Vector v) {}
-
-	/** internal number, for decoding / encoding etc. **/
-
-	public int getNumber() { return number; }
-
-	public void setNumber(int n) { number=n; }
-
-	public String getLabel() {return "";}
-
-	public void setLabel(String s) {}
-
-	/** unique identifier **/
-
-	public String getID() {return "";}
-
-	public void setID(String s) {}
-
-	public Box getLabelSize(Graphics g) {
-		AbstractFontMetrics fm = g == null ? 
-      (AbstractFontMetrics) new DefaultFontMetrics(12) : 
-      (AbstractFontMetrics) new AWTFontMetrics(g.getFontMetrics(g.getFont()));
-		
-		return new Box(Math.max(fm.stringWidth("[. . . .]"),
-                            fm.stringWidth(getLabel())),
-                   fm.getAscent()+fm.getDescent());
-	}
-		
-	public String getPath() { return "";}
-
-	public void setPath(String p) {}
-
-	public String getDir() { return ""; }
-
-	public void setDir(String d) {}
-
-	public void setWeight(double w) {weight=w;}
-
-	public double getWeight() {return weight;}
-
-	public void setDegree(int d) { degree=d; }
-
-	public int getDegree() { return degree; }
-
-	public boolean isDummy() { return false; }
-
-	public Enumeration getChildren() {
-		return ((Vector)(children.clone())).elements();
-	}
-
-	public void addChild(Vertex v) {
-		children.addElement(v);
-		v.parents.addElement(this);
-	}
-
-	public void removeChild(Vertex v) {
-		children.removeElement(v);
-		v.parents.removeElement(this);
-	}
-
-	public boolean isChild(Vertex v) {
-		return children.indexOf(v)>=0;
-	}
-
-	public boolean isParent(Vertex v) {
-		return parents.indexOf(v)>=0;
-	}
-
-	public Enumeration getParents() {
-		return ((Vector)(parents.clone())).elements();
-	}
-
-	public void addParent(Vertex v) {
-		parents.addElement(v);
-		v.children.addElement(this);
-	}
-
-	public void removeParent(Vertex v) {
-		parents.removeElement(v);
-		v.children.removeElement(this);
-	}
-
-	/********************************************************************/
-	/*                   get all predecessor vertices                   */
-	/********************************************************************/
-
-	public Vector getPreds() {
-	    Vector preds=new Vector(10,10);
-	    Vector todo=(Vector)(parents.clone());
-	    Vertex vx1,vx2;
-	    Enumeration e;
-
-	    while (!todo.isEmpty()) {
-		vx1=(Vertex)(todo.lastElement());
-		todo.removeElementAt(todo.size()-1);
-		preds.addElement(vx1);
-		e=vx1.parents.elements();
-		while (e.hasMoreElements()) {
-		    vx2=(Vertex)(e.nextElement());
-		    if (preds.indexOf(vx2)<0 && todo.indexOf(vx2)<0)
-			todo.addElement(vx2);
-		}
-	    }
-
-	    return preds;
-	}
-
-	/********************************************************************/
-	/*                     get all successor vertices                   */
-	/********************************************************************/
-
-	public Vector getSuccs() {
-	    Vector succs=new Vector(10,10);
-	    Vector todo=(Vector)(children.clone());
-	    Vertex vx1,vx2;
-	    Enumeration e;
-
-	    while (!todo.isEmpty()) {
-		vx1=(Vertex)(todo.lastElement());
-		todo.removeElementAt(todo.size()-1);
-		succs.addElement(vx1);
-		e=vx1.children.elements();
-		while (e.hasMoreElements()) {
-		    vx2=(Vertex)(e.nextElement());
-		    if (succs.indexOf(vx2)<0 && todo.indexOf(vx2)<0)
-			todo.addElement(vx2);
-		}
-	    }
-
-	    return succs;
-	}
-
-	public int box_width() { return getLabelSize(gra.gfx).width+8; }
-
-	public int box_width2() { return box_width()/2; }
-
-	public void setX(int x) {this.x=x;}
-
-	public void setY(int y) {this.y=y;}
-
-	public int getX() {return x;}
-
-	public int getY() {return y;}
-
-	public abstract int leftX();
-
-	public abstract int rightX();
-
-	public abstract void draw(Graphics g);
-
-	public void drawButtons(Graphics g) {}
-
-	public void drawBox(Graphics g,Color boxColor) {}
-
-	public void removeButtons(Graphics g) {}
-
-	public boolean contains(int x,int y) { return false; }
-
-	public boolean leftButton(int x,int y) { return false; }
-
-	public boolean rightButton(int x,int y) { return false; }
-
-	public void PS(PrintWriter p) {}
-}
--- a/lib/browser/awtUtilities/Border.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-/***************************************************************************
-  Title:      awtUtilities/Border.java
-  Author:     Stefan Berghofer, TU Muenchen
-
-  This class defines a nice 3D border.
-***************************************************************************/
-
-package awtUtilities;
-
-import java.awt.*;
-
-public class Border extends Panel {
-	int bs;
-
-	public Insets getInsets() {
-		return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
-	}
-
-	public Border(Component comp,int s) {
-		setLayout(new GridLayout(1,1));
-		add(comp);
-		bs=s;
-	}
-
-	public void paint(Graphics g) {
-		int w = getSize().width;
-		int h = getSize().height;
-		int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,0};
-		int x2[]={w,w-bs,w-bs,w}, y2[]={0,bs,h-bs,h};
-		int y3[]={h,h-bs,h-bs,h};
-
-		g.setColor(new Color(224,224,224));
-		g.fillPolygon(y1,y2,4);
-		g.fillPolygon(x1,y1,4);
-		g.setColor(Color.gray);
-		g.fillPolygon(x2,y2,4);
-		g.fillPolygon(x1,y3,4);
-	}
-}
--- a/lib/browser/awtUtilities/MessageDialog.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-/***************************************************************************
-  Title:      awtUtilities/MessageDialog.java
-  Author:     Stefan Berghofer, TU Muenchen
-
-  This class defines a dialog window for displaying messages and buttons.
-***************************************************************************/
-
-package awtUtilities;
-
-import java.awt.*;
-import java.awt.event.*;
-
-public class MessageDialog extends Dialog implements ActionListener {
-	String txt;
-
-	public String getText() { return txt; }
-
-	public void actionPerformed(ActionEvent evt) {
-		txt = evt.getActionCommand();
-		setVisible(false);
-	}
-
-	public MessageDialog(Frame parent,String title,String text,String []buttons) {
-		super(parent,title,true);
-		int i;
-		Panel p1=new Panel(),p2=new Panel();
-		p1.setLayout(new FlowLayout(FlowLayout.CENTER,0,0));
-		p2.setLayout(new FlowLayout());
-		setFont(new Font("Helvetica", Font.PLAIN, 14));
-		setLayout(new GridLayout(2,1));
-
-		while (true) {
-			int pos=text.indexOf(' ');
-			if (pos<0) {
-				p1.add(new Label(text));
-				break;
-			} else {
-				p1.add(new Label(text.substring(0,pos)));
-				if (pos+1==text.length())
-					break;
-				else
-					text=text.substring(pos+1);
-			}
-		}
-
-		add(p1);add(p2);
-		for (i=0;i<buttons.length;i++) {
-			Button bt = new Button(buttons[i]);
-			p2.add(bt);
-			bt.addActionListener(this);
-		}
-	}
-}
--- a/lib/browser/awtUtilities/TextFrame.java	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-/***************************************************************************
-  Title:      Graph/TextFrame.java
-  Author:     Stefan Berghofer, TU Muenchen
-
-  This class defines a simple text viewer.
-***************************************************************************/
-
-package awtUtilities;
-
-import java.awt.*;
-import java.awt.event.*;
-
-public class TextFrame extends Frame implements ActionListener {
-	public void actionPerformed(ActionEvent evt) {
-		setVisible(false);
-	}
-
-	public TextFrame(String title,String text) {
-		super(title);
-		TextArea ta = new TextArea(text,200,80);
-		Button bt = new Button("Dismiss");
-		bt.addActionListener(this);
-		ta.setEditable(false);
-		add("Center", ta);
-		add("South", bt);
-	}
-}
--- a/lib/browser/build	Fri Jul 16 20:13:12 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# mk - build graph browser
-#
-# Requires proper Isabelle settings environment.
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
-
-
-## dependencies
-
-declare -a SOURCES=(
-  GraphBrowser/AWTFontMetrics.java
-  GraphBrowser/AbstractFontMetrics.java
-  GraphBrowser/Box.java
-  GraphBrowser/Console.java
-  GraphBrowser/DefaultFontMetrics.java
-  GraphBrowser/Directory.java
-  GraphBrowser/DummyVertex.java
-  GraphBrowser/Graph.java
-  GraphBrowser/GraphBrowser.java
-  GraphBrowser/GraphBrowserFrame.java
-  GraphBrowser/GraphView.java
-  GraphBrowser/NormalVertex.java
-  GraphBrowser/ParseError.java
-  GraphBrowser/Region.java
-  GraphBrowser/Spline.java
-  GraphBrowser/TreeBrowser.java
-  GraphBrowser/TreeNode.java
-  GraphBrowser/Vertex.java
-  awtUtilities/Border.java
-  awtUtilities/MessageDialog.java
-  awtUtilities/TextFrame.java
-)
-
-TARGET="$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
-
-
-## main
-
-OUTDATED=false
-
-for SOURCE in "${SOURCES[@]}"
-do
-  [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE"
-  [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
-done
-
-if [ "$OUTDATED" = true ]
-then
-  echo >&2 "### Building graph browser ..."
-
-  rm -rf classes && mkdir classes
-
-  isabelle_jdk javac -d classes -Xlint:-options -source 7 -target 7 "${SOURCES[@]}" || \
-    fail "Failed to compile sources"
-  isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . ||
-    fail "Failed to produce $TARGET"
-
-  rm -rf classes
-fi
--- a/lib/scripts/getfunctions	Fri Jul 16 20:13:12 2021 +0100
+++ b/lib/scripts/getfunctions	Fri Jul 16 22:32:56 2021 +0200
@@ -211,14 +211,21 @@
 }
 export -f isabelle_directory
 
-#administrative build
-function isabelle_admin_build ()
+#Isabelle/Scala/Java build
+function isabelle_scala_build ()
 {
-  if [ -e "$ISABELLE_HOME/Admin/build" ]; then
-    "$ISABELLE_HOME/Admin/build" "$@"
+  rm -rf \
+    "$ISABELLE_HOME/lib/classes/Pure.jar" \
+    "$ISABELLE_HOME/lib/classes/Pure.shasum" \
+    "$ISABELLE_HOME/src/Tools/jEdit/dist"
+  if [ "$1" = "fresh" ]; then
+    CMD="build_fresh"
+  else
+    CMD="build"
   fi
+  env ISABELLE_SETUP_CLASSPATH_SKIP=true isabelle java isabelle.setup.Setup "$CMD"
 }
-export -f isabelle_admin_build
+export -f isabelle_scala_build
 
 #arrays
 function splitarray ()
--- a/src/Pure/Admin/build_release.scala	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Pure/Admin/build_release.scala	Fri Jul 16 22:32:56 2021 +0200
@@ -452,10 +452,9 @@
       other_isabelle.resolve_components(echo = true)
 
       try {
-        val export_classpath =
-          "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
-        other_isabelle.bash(export_classpath + "Admin/build all", echo = true).check
-        other_isabelle.bash(export_classpath + "bin/isabelle jedit -b", echo = true).check
+        other_isabelle.bash(
+          "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" +
+          "bin/isabelle jedit -b", echo = true).check
       }
       catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/awt/Border.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,39 @@
+/***************************************************************************
+  Title:      awt/Border.java
+  Author:     Stefan Berghofer, TU Muenchen
+
+  This class defines a nice 3D border.
+***************************************************************************/
+
+package isabelle.awt;
+
+import java.awt.*;
+
+public class Border extends Panel {
+	int bs;
+
+	public Insets getInsets() {
+		return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
+	}
+
+	public Border(Component comp,int s) {
+		setLayout(new GridLayout(1,1));
+		add(comp);
+		bs=s;
+	}
+
+	public void paint(Graphics g) {
+		int w = getSize().width;
+		int h = getSize().height;
+		int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,0};
+		int x2[]={w,w-bs,w-bs,w}, y2[]={0,bs,h-bs,h};
+		int y3[]={h,h-bs,h-bs,h};
+
+		g.setColor(new Color(224,224,224));
+		g.fillPolygon(y1,y2,4);
+		g.fillPolygon(x1,y1,4);
+		g.setColor(Color.gray);
+		g.fillPolygon(x2,y2,4);
+		g.fillPolygon(x1,y3,4);
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/awt/MessageDialog.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,53 @@
+/***************************************************************************
+  Title:      awt/MessageDialog.java
+  Author:     Stefan Berghofer, TU Muenchen
+
+  This class defines a dialog window for displaying messages and buttons.
+***************************************************************************/
+
+package isabelle.awt;
+
+import java.awt.*;
+import java.awt.event.*;
+
+public class MessageDialog extends Dialog implements ActionListener {
+	String txt;
+
+	public String getText() { return txt; }
+
+	public void actionPerformed(ActionEvent evt) {
+		txt = evt.getActionCommand();
+		setVisible(false);
+	}
+
+	public MessageDialog(Frame parent,String title,String text,String []buttons) {
+		super(parent,title,true);
+		int i;
+		Panel p1=new Panel(),p2=new Panel();
+		p1.setLayout(new FlowLayout(FlowLayout.CENTER,0,0));
+		p2.setLayout(new FlowLayout());
+		setFont(new Font("Helvetica", Font.PLAIN, 14));
+		setLayout(new GridLayout(2,1));
+
+		while (true) {
+			int pos=text.indexOf(' ');
+			if (pos<0) {
+				p1.add(new Label(text));
+				break;
+			} else {
+				p1.add(new Label(text.substring(0,pos)));
+				if (pos+1==text.length())
+					break;
+				else
+					text=text.substring(pos+1);
+			}
+		}
+
+		add(p1);add(p2);
+		for (i=0;i<buttons.length;i++) {
+			Button bt = new Button(buttons[i]);
+			p2.add(bt);
+			bt.addActionListener(this);
+		}
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/awt/TextFrame.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,27 @@
+/***************************************************************************
+  Title:      awt/TextFrame.java
+  Author:     Stefan Berghofer, TU Muenchen
+
+  This class defines a simple text viewer.
+***************************************************************************/
+
+package isabelle.awt;
+
+import java.awt.*;
+import java.awt.event.*;
+
+public class TextFrame extends Frame implements ActionListener {
+	public void actionPerformed(ActionEvent evt) {
+		setVisible(false);
+	}
+
+	public TextFrame(String title,String text) {
+		super(title);
+		TextArea ta = new TextArea(text,200,80);
+		Button bt = new Button("Dismiss");
+		bt.addActionListener(this);
+		ta.setEditable(false);
+		add("Center", ta);
+		add("South", bt);
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/etc/build.props	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,26 @@
+description = graph browser
+lib = $ISABELLE_HOME/lib/classes
+name = isabelle_graphbrowser
+javac_options = -source 7 -target 7
+sources = \
+  awt/Border.java \
+  awt/MessageDialog.java \
+  awt/TextFrame.java \
+  graphbrowser/AWTFontMetrics.java \
+  graphbrowser/AbstractFontMetrics.java \
+  graphbrowser/Box.java \
+  graphbrowser/Console.java \
+  graphbrowser/DefaultFontMetrics.java \
+  graphbrowser/Directory.java \
+  graphbrowser/DummyVertex.java \
+  graphbrowser/Graph.java \
+  graphbrowser/GraphBrowser.java \
+  graphbrowser/GraphBrowserFrame.java \
+  graphbrowser/GraphView.java \
+  graphbrowser/NormalVertex.java \
+  graphbrowser/ParseError.java \
+  graphbrowser/Region.java \
+  graphbrowser/Spline.java \
+  graphbrowser/TreeBrowser.java \
+  graphbrowser/TreeNode.java \
+  graphbrowser/Vertex.java
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/etc/settings	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/AWTFontMetrics.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,31 @@
+/***************************************************************************
+  Title:      graphbrowser/AWTFontMetrics.java
+  Author:     Gerwin Klein, TU Muenchen
+
+  AbstractFontMetrics from the AWT for graphics mode.
+  
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.FontMetrics;
+
+public class AWTFontMetrics implements AbstractFontMetrics {
+  private FontMetrics fontMetrics;
+
+  public AWTFontMetrics(FontMetrics m) {
+    fontMetrics = m;
+  }
+
+  public int stringWidth(String str) {
+    return fontMetrics.stringWidth(str);
+  }
+
+  public int getAscent() {
+    return fontMetrics.getAscent();
+  }
+
+  public int getDescent() {
+    return fontMetrics.getDescent();
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/AbstractFontMetrics.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,16 @@
+/***************************************************************************
+  Title:      graphbrowser/AWTFontMetrics.java
+  Author:     Gerwin Klein, TU Muenchen
+
+  AbstractFontMetrics avoids dependency on java.awt.FontMetrics in 
+  batch mode.
+  
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+public interface AbstractFontMetrics {
+  public int stringWidth(String str);
+  public int getAscent();
+  public int getDescent();
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Box.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,20 @@
+/***************************************************************************
+  Title:      graphbrowser/Box.java
+  Author:     Gerwin Klein, TU Muenchen
+
+  A box with width and height. Used instead of java.awt.Dimension for 
+  batch mode.
+
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+public class Box {
+  public int width;
+  public int height;
+
+  public Box(int w, int h) {
+    this.width = w;
+    this.height = h;
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Console.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,89 @@
+/***************************************************************************
+  Title:      graphbrowser/Console.java
+  Author:     Gerwin Klein, TU Muenchen
+  Options:    :tabSize=2:
+
+  This is the graph browser's main class when run as a console application.
+  It duplicates some logic from GraphBrowser and GraphView.
+  It does so to remove dependency on AWT.
+
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.io.*;
+import java.util.*;
+
+public class Console {
+	Graph g;
+	String gfname;  
+
+  public Console(String name) {
+    gfname = name;
+  }
+
+	public void PS(String fname, boolean printable) throws IOException {
+    g.layout(null);
+		g.PS(fname,printable);
+	}
+
+
+	public void collapseNodes(Vector collapsedDir) { 
+		Enumeration e1=collapsedDir.elements();
+		Graph gra=(Graph)(g.clone());
+
+		while (e1.hasMoreElements()) {
+			Directory d=(Directory)(e1.nextElement());
+			Vector v=gra.decode(d.getCollapsed());
+			if (!v.isEmpty())
+				gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
+		}
+    
+    g = gra;
+	}
+
+
+	public void initBrowser(InputStream is) {
+		try {
+			TreeNode tn = new TreeNode("Root", "", -1, true);
+      g = new Graph(is, tn);
+			Vector v = new Vector(10,10);
+			tn.collapsedDirectories(v);      
+      collapseNodes(v);
+		} catch (IOException exn) {
+			System.err.println("\nI/O error while reading graph file.");
+		} catch (ParseError exn) {
+			System.err.println("\nParse error in graph file:");
+			System.err.println(exn.getMessage());
+			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> "+
+                         "[ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
+		}
+	}
+
+	public static void main(String[] args) {
+		try {
+      if (args.length <= 1) {
+        System.err.println("Graph and output file expected.");
+        return;
+      }
+
+			Console console=new Console(args[0]);
+      InputStream is=new FileInputStream(args[0]);
+      console.initBrowser(is);
+      is.close();      
+    
+      try {
+        if (args[1].endsWith(".ps"))
+          console.PS(args[1], true);
+        else if (args[1].endsWith(".eps"))
+          console.PS(args[1], false);
+        else
+          System.err.println("Unknown file type: " + args[1]);
+      } catch (IOException exn) {
+        System.err.println("Unable to write file " + args[1]);
+      }
+		} catch (IOException exn) {
+			System.err.println("Can't open graph file "+args[0]);
+		}
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,48 @@
+/***************************************************************************
+  Title:      graphbrowser/DefaultFontMetrics.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=2:
+
+  Default font metrics which is used when no graphics context
+  is available (batch mode).
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+public class DefaultFontMetrics implements AbstractFontMetrics {
+
+  private static int[] chars =
+	{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
+	 27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
+	 32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
+	 32, 29, 35, 32, 45, 32, 32, 29, 13, 13, 13, 22, 27, 11, 27, 27, 24,
+	 27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
+	 27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
+
+  private int size;
+
+  public DefaultFontMetrics(int size)
+  { this.size = size; }
+
+  public int getLeading()
+  { return 1; }
+
+  public int getAscent()
+  { return (int)(Math.round(size * 46.0 / 48.0)); }
+  
+  public int getDescent() 
+  { return (int)(Math.round(size * 10.0 / 48.0)); }
+  
+  public int charWidth(char c) {
+    if (c < 32 || c > 126) { return 0; }
+    else {
+	    return (int)(Math.round(chars[c - 32] * size / 48.0));
+    }
+  }
+  
+  public int stringWidth(String s) {
+    int l=0, i;
+    for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
+    return l;
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Directory.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,21 @@
+package isabelle.graphbrowser;
+
+import java.util.Vector;
+
+class Directory {
+	TreeNode node;
+	String name;
+	Vector collapsed;
+
+	public Directory(TreeNode nd,String n,Vector col) {
+		collapsed=col;
+		name=n;
+		node=nd;
+	}
+
+	public TreeNode getNode() { return node; }
+
+	public String getName() { return name; }
+
+	public Vector getCollapsed() { return collapsed; }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/DummyVertex.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,29 @@
+/***************************************************************************
+  Title:      graphbrowser/DummyVertex.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This class represents a dummy vertex, which is used to simplify the
+  layout algorithm.
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.*;
+
+class DummyVertex extends Vertex {
+	public boolean isDummy() {return true;}
+
+	public Object clone() {
+		Vertex ve=new DummyVertex();
+		ve.setX(getX());ve.setY(getY());
+		return ve;
+	}
+
+	public int leftX() { return getX(); }
+
+	public int rightX() { return getX(); }
+
+	public void draw(Graphics g) {}
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Graph.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,1062 @@
+/***************************************************************************
+  Title:      graphbrowser/Graph.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This class contains the core of the layout algorithm and methods for
+  drawing and PostScript output.
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.util.*;
+import java.awt.*;
+import java.io.*;
+
+public class Graph {
+	/**** parameters for layout ****/
+
+	public int box_height=0;
+	public int box_height2;
+	public Graphics gfx;
+
+	Vector vertices=new Vector(10,10);
+	Vector splines=new Vector(10,10);
+	Vector numEdges=new Vector(10,10);
+	Vertex []vertices2;
+
+	public int min_x=0,min_y=0,max_x=10,max_y=10;
+
+	/********************************************************************/
+	/*                         clone graph object                       */
+	/********************************************************************/
+
+	public Object clone() {
+		Graph gr=new Graph();
+		Enumeration e1;
+		int i;
+
+		gr.splines=(Vector)(splines.clone());
+
+		e1=vertices.elements();
+		while (e1.hasMoreElements())
+			gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone()));
+
+		for (i=0;i<vertices.size();i++) {
+			Vertex vx1=(Vertex)(gr.vertices.elementAt(i));
+			e1=((Vertex)(vertices.elementAt(i))).getChildren();
+			while (e1.hasMoreElements()) {
+				Vertex vx2=(Vertex)(gr.vertices.elementAt(vertices.indexOf(e1.nextElement())));
+				vx1.addChild(vx2);
+			}
+		}
+
+		gr.vertices2 = new Vertex[vertices.size()];
+		gr.vertices.copyInto(gr.vertices2);
+
+		gr.min_x=min_x;gr.max_x=max_x;
+		gr.min_y=min_y;gr.max_y=max_y;
+
+		return gr;
+	}
+
+	Graph() {}
+
+	/********************************************************************/
+	/*                      Read graph from stream                      */
+	/********************************************************************/
+
+	public Graph(InputStream s,TreeNode tn) throws IOException, ParseError {
+		StreamTokenizer tok=new StreamTokenizer(new InputStreamReader(s));
+		String name,dir,vertexID;
+		Vertex ve1,ve2;
+		boolean children,unfoldDir;
+		int index=0;
+
+		tok.nextToken();
+		while (tok.ttype!=StreamTokenizer.TT_EOF) {
+			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+				throw new ParseError("expected: vertex name\nfound   : "+tok.toString());
+			name=tok.sval;
+                        tok.nextToken();
+			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+				throw new ParseError("expected: vertex identifier\nfound   : "+tok.toString());
+			vertexID=tok.sval;
+			tok.nextToken();
+			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+				throw new ParseError("expected: directory name\nfound   : "+tok.toString());
+			dir=tok.sval;
+			tok.nextToken();
+			if (tok.ttype=='+') {
+				unfoldDir=true;
+				tok.nextToken();
+			} else
+				unfoldDir=false;
+			if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+				throw new ParseError("expected: path name\nfound   : "+tok.toString());
+			ve1=findVertex(vertexID);
+			if (ve1==null) {
+				ve1=new NormalVertex("");
+				ve1.setID(vertexID);
+				ve1.setNumber(index++);
+				addVertex(ve1);
+			}
+			ve1.setPath(tok.sval);
+			ve1.setDir(dir);
+                        ve1.setLabel(name);
+			tn.insertNode(name,dir,tok.sval,ve1.getNumber(),unfoldDir);
+			tok.nextToken();
+			if (tok.ttype=='<') {
+				children=true;
+				tok.nextToken();
+			} else if (tok.ttype=='>') {
+					children=false;
+					tok.nextToken();
+			} else children=true;
+			while (tok.ttype!=';') {
+				if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
+					throw new ParseError("expected: child vertex identifier or ';'\nfound   : "+tok.toString());				
+				ve2=findVertex(tok.sval);
+				if (ve2==null) {
+					ve2=new NormalVertex("");
+					ve2.setID(tok.sval);
+					ve2.setNumber(index++);
+					addVertex(ve2);
+				}
+				if (children)
+					ve1.addChild(ve2);
+				else
+					ve1.addParent(ve2);
+				tok.nextToken();
+			}
+			tok.nextToken();
+		}
+		vertices2 = new Vertex[vertices.size()];
+		vertices.copyInto(vertices2);
+	}
+	
+	/*** Find vertex with identifier vertexID ***/
+
+	public Vertex findVertex(String vertexID) {
+		Enumeration e1=vertices.elements();
+		Vertex v1;
+
+		while (e1.hasMoreElements()) {
+			v1=(Vertex)(e1.nextElement());
+			if ((v1.getID()).equals(vertexID))
+				return v1;
+		}
+		return null;
+	}
+		 
+	public void addVertex(Vertex v) {
+		vertices.addElement(v);
+		v.setGraph(this);
+	}
+
+	public void removeVertex(Vertex v) {
+		vertices.removeElement(v);
+	}
+
+	public Enumeration getVertices() {
+		return vertices.elements();
+	}
+
+	/********************************************************************/
+	/*                          graph layout                            */
+	/********************************************************************/
+
+	public void layout(Graphics g) {
+		splines.removeAllElements();
+		hasseDiagram();
+		Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0))));
+		setParameters(g);
+		init_coordinates(layers);
+		pendulum(layers);
+		rubberband(layers);
+		calcSplines(layers);
+		calcBoundingBox();
+	}
+
+	/********************************************************************/
+	/*                      set layout parameters                       */
+	/********************************************************************/
+
+	public void setParameters(Graphics g) {
+		Enumeration e1=vertices.elements();
+		int h;
+		h=Integer.MIN_VALUE;
+
+		while (e1.hasMoreElements()) {
+		  Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
+			h=Math.max(h,dim.height);
+		}
+		box_height=h+4;
+		box_height2=box_height/2;
+		gfx=g;
+	}
+
+	/********************************************************************/
+	/*                       topological sorting                        */
+	/********************************************************************/
+
+	public Vector sort() {
+		Vector todo=(Vector)(vertices.clone());
+		Vector layers=new Vector(10,10);
+		Vector todo2;
+		Enumeration e1,e2;
+		Vertex v,v2;
+
+		e1=vertices.elements();
+		while (e1.hasMoreElements())
+			((Vertex)(e1.nextElement())).setDegree(0);
+
+		e1=vertices.elements();
+		while (e1.hasMoreElements()) {
+			v=(Vertex)(e1.nextElement());
+			e2=v.getChildren();
+			while (e2.hasMoreElements()) {
+				v2=(Vertex)(e2.nextElement());
+				todo.removeElement(v2);
+				v2.setDegree(1+v2.getDegree());
+			}
+		}
+		while (!todo.isEmpty()) {
+			layers.addElement(todo);
+			todo2=new Vector(10,10);
+			e1=todo.elements();
+			while (e1.hasMoreElements()) {
+				e2=((Vertex)(e1.nextElement())).getChildren();
+				while (e2.hasMoreElements()) {
+					v=(Vertex)(e2.nextElement());
+					v.setDegree(v.getDegree()-1);
+					if (v.getDegree()==0) {
+						todo2.addElement(v);
+						v.setDegree(layers.size());
+					}
+				}
+			}
+			todo=todo2;
+		}
+		return layers;
+	}
+
+	/********************************************************************/
+	/*                      compute hasse diagram                       */
+	/********************************************************************/
+
+	public void hasseDiagram() {
+		Enumeration e1,e2;
+		Vertex vx1,vx2;
+
+		/** construct adjacence matrix **/
+
+		int vs=vertices.size();
+		boolean adj[][]=new boolean[vs][vs];
+		boolean adj2[][]=new boolean[vs][vs];
+		int i,j,k;
+
+		e1=getVertices();
+		for (i=0;i<vs;i++) {
+			vx1=(Vertex)(e1.nextElement());
+			e2=vx1.getChildren();
+			while (e2.hasMoreElements()) {
+				vx2=(Vertex)(e2.nextElement());
+				j=vertices.indexOf(vx2);
+				adj[i][j]=true;
+				adj2[i][j]=true;
+			}
+		}
+
+		/** compute transitive closure R+ **/
+
+		for (k=0;k<vs;k++)
+			for (i=0;i<vs;i++)
+				if (adj[i][k])
+					for (j=0;j<vs;j++)
+						adj[i][j] = adj[i][j] || adj[k][j];
+
+		/** compute R \ (R+)^2 **/
+
+		for (i=0;i<vs;i++)
+			for (j=0;j<vs;j++)
+				if (adj2[i][j]) {
+					vx1=(Vertex)(vertices.elementAt(i));
+					vx2=(Vertex)(vertices.elementAt(j));
+					for (k=0;k<vs;k++)
+						if (adj[i][k] && adj[k][j]) {
+							vx1.removeChild(vx2);
+							break;
+						}
+				}
+	}
+				
+	/********************************************************************/
+	/*                      insert dummy vertices                       */
+	/********************************************************************/
+
+	public Vector insert_dummies(Vector v) {
+		Vector layers2=new Vector(10,10);
+		int n_edges;
+
+		do {
+			Enumeration e1=v.elements(),e2;
+			Vector next=new Vector(10,10);
+
+			layers2.addElement(v);
+			n_edges=0;
+			while (e1.hasMoreElements()) {
+				Vertex v1=(Vertex)(e1.nextElement());
+				e2=v1.getChildren();
+				while (e2.hasMoreElements()) {
+					n_edges++;
+					Vertex v2=(Vertex)(e2.nextElement());
+					if (v2.getDegree()!=v1.getDegree()+1) {
+						Vertex v3=new DummyVertex();
+						v3.addChild(v2);
+						v3.setDegree(v1.getDegree()+1);
+						v1.removeChild(v2);
+						v1.addChild(v3);
+						next.addElement(v3);
+						addVertex(v3);
+					} else if (next.indexOf(v2)<0) next.addElement(v2);
+				}
+			}
+			v=next;
+			numEdges.addElement(Integer.valueOf(n_edges));
+		} while (!v.isEmpty());
+		return layers2;
+	}
+
+	/********************************************************************/
+	/*                     calculation of crossings                     */
+	/********************************************************************/
+
+	public int count_crossings(Vector layers,int oldcr) {
+		int i,j,y1,y2,cr=0,l;
+		for (l=0;l<layers.size()-1;l++) {
+			Vector v1=(Vector)(layers.elementAt(l));
+			for (i=0;i<v1.size();i++) {
+				Enumeration e2=((Vertex)(v1.elementAt(i))).getChildren();
+				while (e2.hasMoreElements()) {
+					y1=((Vector)(layers.elementAt(l+1))).indexOf(e2.nextElement());
+					for (j=0;j<i;j++) {
+						Enumeration e3=((Vertex)(v1.elementAt(j))).getChildren();
+						while (e3.hasMoreElements()) {
+							y2=((Vector)(layers.elementAt(l+1))).indexOf(e3.nextElement());
+							if (y1<y2) {
+								cr++;
+								if (cr>=oldcr) return cr;
+							}
+						}
+					}
+				}
+			}
+		}
+		return cr;
+	}
+
+	/********************************************************************/
+	/* calculation of crossings where vertices vx1 and vx2 are involved */
+	/* vx1 and vx2 must be in same layer and vx1 is left from vx2       */
+	/********************************************************************/
+
+	public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) {
+		int i,cr=0,l=vx1.getDegree();
+		Vertex va,vb;
+		Vector layer;
+		Enumeration e1,e2;
+
+		if (l>0) {
+			layer=(Vector)(layers.elementAt(l-1));
+			e1=vx1.getParents();
+			while (e1.hasMoreElements()) {
+				va=(Vertex)(e1.nextElement());
+				i=layer.indexOf(va);
+				e2=vx2.getParents();
+				while (e2.hasMoreElements()) {
+					vb=(Vertex)(e2.nextElement());
+					if (layer.indexOf(vb)<i) {
+						cr++;
+						if (cr>=oldcr) return cr;
+					}
+				}
+			}
+		}
+		if (l<layers.size()-1) {
+			layer=(Vector)(layers.elementAt(l+1));
+			e1=vx1.getChildren();
+			while (e1.hasMoreElements()) {
+				va=(Vertex)(e1.nextElement());
+				i=layer.indexOf(va);
+				e2=vx2.getChildren();
+				while (e2.hasMoreElements()) {
+					vb=(Vertex)(e2.nextElement());
+					if (layer.indexOf(vb)<i) {
+						cr++;
+						if (cr>=oldcr) return cr;
+					}
+				}
+			}
+		}
+		return cr;
+	}
+
+	/********************************************************************/
+	/*       reduction of crossings by exchanging adjacent vertices     */
+	/********************************************************************/
+
+	public void exchangeVertices(Vector layers,int oldcr) {
+		int i,l,c1,c2;
+		Vertex vx1,vx2;
+		Vector v1;
+
+		for (l=0;l<layers.size();l++) {
+			v1=(Vector)(layers.elementAt(l));
+			for (i=0;i<v1.size()-1;i++) {
+				vx1=(Vertex)(v1.elementAt(i));
+				vx2=(Vertex)(v1.elementAt(i+1));
+				c1=count_crossings_2(layers,vx1,vx2,oldcr);
+				c2=count_crossings_2(layers,vx2,vx1,c1);
+				if (c2<c1) {
+					v1.setElementAt(vx2,i);
+					v1.setElementAt(vx1,i+1);
+				}
+			}
+		}
+	}
+
+	/********************************************************************/
+	/*                    minimization of crossings                     */
+	/********************************************************************/
+
+	public Vector min_crossings(Vector layers) {
+		int n,i,l,k,z=0,cr2,cr=count_crossings(layers,Integer.MAX_VALUE);
+		boolean topdown=true,first=true;
+		Enumeration e1,e2;
+		Vector v1,v2,layers2=null,best=layers;
+		Vertex vx1,vx2;
+		n=0;
+		while (n<3 && cr>0) {
+			if (topdown) {
+				/** top-down-traversal **/
+
+				layers2=new Vector(10,10);
+				for (l=0;l<layers.size();l++) {
+					v1=(Vector)(layers.elementAt(l));
+					if (l==0) layers2.addElement(v1.clone());
+					else {
+						v2=new Vector(10,10);
+						layers2.addElement(v2);
+						e1=v1.elements();
+						while (e1.hasMoreElements()) {
+							vx1=(Vertex)(e1.nextElement());
+							k=0;z=0;
+							e2=vx1.getParents();
+							while (e2.hasMoreElements()) {
+								k+=((Vector)(layers2.elementAt(l-1))).indexOf(e2.nextElement());
+								z++;
+							}
+							if (z>0)
+								vx1.setWeight(((double)(k))/z);
+							else if (first)
+								vx1.setWeight(Double.MAX_VALUE);
+							for (i=0;i<v2.size();i++)
+								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
+							if (i==v2.size()) v2.addElement(vx1);
+							else v2.insertElementAt(vx1,i);
+						}
+					}
+				}
+			} else {
+				/** bottom-up-traversal **/
+
+				layers2=new Vector(10,10);
+				for (l=layers.size()-1;l>=0;l--) {
+					v1=(Vector)(layers.elementAt(l));
+					if (l==layers.size()-1) layers2.addElement(v1.clone());
+					else {
+						v2=new Vector(10,10);
+						layers2.insertElementAt(v2,0);
+						e1=v1.elements();
+						while (e1.hasMoreElements()) {
+							vx1=(Vertex)(e1.nextElement());
+							k=0;z=0;
+							e2=vx1.getChildren();
+							while (e2.hasMoreElements()) {
+								k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement());
+								z++;
+							}
+							if (z>0)
+								vx1.setWeight(((double)(k))/z);
+							else if (first)
+								vx1.setWeight(Double.MAX_VALUE);
+							for (i=0;i<v2.size();i++)
+								if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
+							if (i==v2.size()) v2.addElement(vx1);
+							else v2.insertElementAt(vx1,i);
+						}
+					}
+				}
+			}
+			//exchangeVertices(layers2,cr);
+			topdown=!topdown;
+			first=false;
+			layers=layers2;
+
+			cr2=count_crossings(layers2,cr);
+			if (cr2<cr) {
+				best=layers2;
+				cr=cr2;					
+			} else n++;
+		}
+
+		while (true) {
+			exchangeVertices(best,cr);
+			cr2=count_crossings(best,cr);
+			if (cr2<cr)
+				cr=cr2;
+			else
+				break;
+		}
+
+		return best;
+	}
+
+	/********************************************************************/
+	/*                   set initial coordinates                        */
+	/********************************************************************/
+
+	public void init_coordinates(Vector layers) {
+		int y=0;
+		Enumeration e1=layers.elements();
+		Enumeration e3=numEdges.elements();
+		while (e1.hasMoreElements()) {
+			Vector v1=(Vector)(e1.nextElement());
+			Enumeration e2=v1.elements();
+			int x=0;
+			while (e2.hasMoreElements()) {
+				Vertex ve=(Vertex)(e2.nextElement());
+				ve.setX(x+ve.box_width2());
+				ve.setY(y);
+				x+=ve.box_width()+20;
+			}
+			y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
+		}
+	}
+
+	/********************************************************************/
+	/*                       pendulum method                            */
+	/********************************************************************/
+
+	public void pendulum(Vector layers) {
+		Vector layers2=new Vector(10,10);
+		Enumeration e1=layers.elements(),e2;
+		int i,j,d1,d2,k,offset,dsum;
+		Region r1,r2;
+		boolean change;
+
+		while (e1.hasMoreElements()) {
+			e2=((Vector)(e1.nextElement())).elements();
+			Vector layer=new Vector(10,10);
+			layers2.addElement(layer);
+			while (e2.hasMoreElements()) {
+				Region r=new Region(this);
+				r.addVertex((Vertex)(e2.nextElement()));
+				layer.addElement(r);
+			}
+		}
+		for (k=0;k<10;k++) {
+			dsum=0;
+			for (j=1;j<layers2.size();j++) {
+				Vector l=(Vector)(layers2.elementAt(j));
+				if (l.size()>=2) {
+					do {
+						change=false;
+						d1=((Region)(l.firstElement())).pred_deflection();
+						for (i=0;i<l.size()-1;i++) {
+							r1=(Region)(l.elementAt(i));
+							r2=(Region)(l.elementAt(i+1));
+							d2=r2.pred_deflection();
+							if (r1.touching(r2) && (d1 <= 0 && d2 < d1 ||
+								d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) {
+								r1.combine(r2);
+								l.removeElement(r2);
+								change=true;
+								d2=r1.pred_deflection();
+							}
+							d1=d2;
+						}
+					} while (change);
+				}
+				for (i=0;i<l.size();i++) {
+					r1=(Region)(l.elementAt(i));
+					d1=r1.pred_deflection();
+					offset=d1;
+					if (d1<0 && i>0) offset=-Math.min(
+						((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1);
+					if (d1>=0 && i<l.size()-1) offset=Math.min(
+						r1.spaceBetween((Region)(l.elementAt(i+1))),d1);
+					r1.move(offset);
+					dsum+=Math.abs(d1);
+				}		
+			}
+			if (dsum==0) break;
+		}
+	}		
+
+	/********************************************************************/
+	/*                      rubberband method                           */
+	/********************************************************************/
+
+	public void rubberband(Vector layers) {
+		Enumeration e1,e2;
+		int i,n,k,d,d2;
+		Vector v;
+		Vertex vx;
+
+		for (k=0;k<10;k++) {
+			e1=layers.elements();
+			while (e1.hasMoreElements()) {
+				v=(Vector)(e1.nextElement());
+				for (i=0;i<v.size();i++) {
+					n=0;d=0;
+					vx=(Vertex)(v.elementAt(i));
+					e2=vx.getChildren();
+					while (e2.hasMoreElements()) {
+						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
+						n++;
+					}
+					e2=vx.getParents();
+					while (e2.hasMoreElements()) {
+						d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
+						n++;
+					}
+					d2=(n!=0?d/n:0);
+
+					if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) ||
+						d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2))
+						vx.setX(vx.getX()+d2);
+				}
+			}
+		}
+	}
+
+	/**** Intersection point of two lines (auxiliary function for calcSplines)   ****/
+	/**** Calculate intersection point of line which is parallel to line (p1,p2) ****/
+	/**** and leads through p5, with line (p3,p4)                                ****/
+
+	Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) {
+		float x=0,y=0,s1=0,s2=0;
+
+		if (p1.x!=p2.x)
+			s1=((float)(p2.y-p1.y))/(p2.x-p1.x);
+		if (p3.x!=p4.x)
+			s2=((float)(p4.y-p3.y))/(p4.x-p3.x);
+		if (p1.x==p2.x) {
+			x=p5.x;
+			y=s2*(p5.x-p3.x)+p3.y;
+		} else if (p3.x==p4.x) {
+			x=p3.x;
+			y=s1*(p3.x-p5.x)+p5.y;
+		} else {
+			x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2);
+			y=s2*(x-p3.x)+p3.y;
+		}
+		return new Point(Math.round(x),Math.round(y));
+	}
+
+	/**** Calculate control points (auxiliary function for calcSplines) ****/
+
+	Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) {
+
+		/*** Points p1 , p2 , p3 define a triangle which encloses the spline.  ***/
+		/*** Check if adjacent boxes (specified by lboxx,rboxx and boxy)       ***/
+		/*** collide with the spline. In this case p1 and p3 are shifted by an ***/
+		/*** appropriate offset before they are returned                       ***/
+
+		int xh1,xh2,bx=0,by=0;
+		boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y;
+		boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y ||
+                              boxy+box_height >= p3.y && boxy+box_height <= p1.y;
+		boolean move = false;
+		Point b;
+
+		xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
+		xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
+
+		if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) {
+			move = true;
+			bx = lboxx;
+			by = boxy + (xh1 < xh2 ? 0 : box_height ) ;
+		} else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) {
+			move = true;
+			bx = rboxx;
+			by = boxy + (xh1 > xh2 ? 0 : box_height ) ;
+		} else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) {
+			move = true;
+			bx = (xh1 <= lboxx ? lboxx : rboxx ) ;
+			by = boxy;
+		} else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) {
+			move = true;
+			bx = (xh2 <= lboxx ? lboxx : rboxx ) ;
+			by = boxy+box_height;
+		}
+		b=new Point(bx,by);
+		if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b));
+		else return new Points(p1,p3);
+	}
+
+	/********************************************************************/
+	/*                        calculate splines                         */
+	/********************************************************************/
+
+	public void calcSplines(Vector layers) {
+		Enumeration e2,e1=vertices.elements();
+		Vertex vx1,vx2,vx3;
+		Vector pos,layer;
+		int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc;
+
+		while (e1.hasMoreElements()) {
+			vx1=(Vertex)(e1.nextElement());
+			if (!vx1.isDummy()) {
+				e2=vx1.getChildren();
+				while (e2.hasMoreElements()) {
+					vx2=(Vertex)(e2.nextElement());
+					if (vx2.isDummy()) {
+						vx3=vx2;
+						/**** convert edge to spline ****/
+						pos=new Vector(10,10);
+						x1=vx1.getX();
+						y1=vx1.getY()+box_height;
+
+						do {
+							/*** calculate position of control points ***/
+							x2=vx2.getX();
+							y2=vx2.getY();
+							layer=(Vector)(layers.elementAt(vx2.getDegree()));
+							k=layer.indexOf(vx2);
+							vx2=(Vertex)((vx2.getChildren()).nextElement());
+							x3=vx2.getX();
+							y3=vx2.getY();
+							spc=0;
+							leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
+								Integer.MIN_VALUE:
+								((Vertex)(layer.elementAt(k-1))).rightX()+spc;
+							rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ?
+								Integer.MAX_VALUE:
+								((Vertex)(layer.elementAt(k+1))).leftX()-spc;
+							xh=x2+box_height*(x3-x2)/(y3-y2);
+							if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) {
+								/* top control point */
+								pos.addElement(Integer.valueOf(1));
+								y1=y2;
+							} else {
+								xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1);
+								if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx))
+									/* bottom control point */
+									pos.addElement(Integer.valueOf(2));
+								else
+									/* two control points needed */
+									pos.addElement(Integer.valueOf(3));
+								y1=y2+box_height;
+							}
+							x1=x2;
+						} while (vx2.isDummy());
+						pos.addElement(Integer.valueOf(1));
+
+						/**** calculate triangles ****/
+						vx2=vx3;
+
+						int pos1,pos2,i=0;
+						Vector pts=new Vector(10,10);
+						int lboxx,rboxx,boxy;
+
+						x1=vx1.getX();
+						y1=vx1.getY()+box_height;
+						pts.addElement(new Point(x1,y1)); /** edge starting point **/
+						do {
+							x2=vx2.getX();
+							y2=vx2.getY();
+							pos1=((Integer)(pos.elementAt(i))).intValue();
+							pos2=((Integer)(pos.elementAt(i+1))).intValue();
+							i++;
+							layer=(Vector)(layers.elementAt(vx2.getDegree()));
+							k=layer.indexOf(vx2);
+							boxy=vx2.getY();
+							vx2=(Vertex)((vx2.getChildren()).nextElement());
+							x3=vx2.getX();
+							y3=vx2.getY();
+							if (pos1==2) y2+=box_height;
+							if (pos2==2) y3+=box_height;
+
+							lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ?
+								Integer.MIN_VALUE :
+								((Vertex)(layer.elementAt(k-1))).rightX();
+
+							rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ?
+								Integer.MAX_VALUE :
+								((Vertex)(layer.elementAt(k+1))).leftX();
+
+							Point p1,p2,p3;
+							Points ps;
+
+							p1 = new Point((x1+x2)/2,(y1+y2)/2);
+
+							if (pos1<=2) {
+								/** one control point **/
+								p2 = new Point(x2,y2);
+								ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy);
+								pts.addElement(ps.p);
+								pts.addElement(p2);
+								pts.addElement(ps.q);
+							} else {
+								/** two control points **/
+								p2 = new Point(x2,y2-box_height);
+								p3 = new Point(x2,y2+box_height2);
+								ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy);
+								pts.addElement(ps.p);
+								pts.addElement(p2);
+								pts.addElement(ps.q);
+								p2 = new Point(x2,y2+box_height*2);
+								ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2),
+								               lboxx,rboxx,boxy);
+								pts.addElement(ps.p);
+								pts.addElement(p2);
+								pts.addElement(ps.q);
+							}
+							x1=p2.x;
+							y1=p2.y;
+						} while (vx2.isDummy());
+
+						pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/
+						splines.addElement(new Spline(pts));
+					}
+				}
+			}
+		}
+	}
+
+	/********************************************************************/
+	/*                      calculate bounding box                      */
+	/********************************************************************/
+
+	public void calcBoundingBox() {
+		min_y=min_x=Integer.MAX_VALUE;
+		max_y=max_x=Integer.MIN_VALUE;
+
+		Enumeration e1=vertices.elements();
+		Vertex v;
+
+		while (e1.hasMoreElements()) {
+			v=(Vertex)(e1.nextElement());
+			min_x=Math.min(min_x,v.leftX());
+			max_x=Math.max(max_x,v.rightX());
+			min_y=Math.min(min_y,v.getY());
+			max_y=Math.max(max_y,v.getY()+box_height);
+		}
+		min_x-=20;
+		min_y-=20;
+		max_x+=20;
+		max_y+=20;
+	}
+
+	/********************************************************************/
+	/*                           draw graph                             */
+	/********************************************************************/
+					 
+	public void draw(Graphics g) {
+		if (box_height==0) layout(g);
+
+		g.translate(-min_x,-min_y);
+
+		Enumeration e1=vertices.elements();
+		while (e1.hasMoreElements())
+			((Vertex)(e1.nextElement())).draw(g);
+
+		e1=splines.elements();
+		while (e1.hasMoreElements())
+			((Spline)(e1.nextElement())).draw(g);
+	}
+
+	/********************************************************************/
+	/*               return vertex at position (x,y)                    */
+	/********************************************************************/
+
+	public Vertex vertexAt(int x,int y) {
+		Enumeration e1=vertices.elements();
+		while (e1.hasMoreElements()) {
+			Vertex v=(Vertex)(e1.nextElement());
+			if (v.contains(x,y)) return v;
+		}
+		return null;
+	}
+
+	/********************************************************************/
+	/*       encode list of vertices (as array of vertice numbers)      */
+	/********************************************************************/
+
+	public Vector encode(Vector v) {
+		Vector code=new Vector(10,10);
+		Enumeration e1=v.elements();
+
+		while (e1.hasMoreElements()) {
+			Vertex vx=(Vertex)(e1.nextElement());
+			if (vx.getNumber()>=0)
+				code.addElement(Integer.valueOf(vx.getNumber()));
+		}
+		return code;
+	}
+
+	/********************************************************************/
+	/*                      get vertex with number n                    */
+	/********************************************************************/
+
+	public Vertex getVertexByNum(int x) {
+		Enumeration e1=vertices.elements();
+
+		while (e1.hasMoreElements()) {
+			Vertex vx=(Vertex)(e1.nextElement());
+			if (vx.getNumber()==x) return vx;
+		}
+		return null;
+	}
+
+	/********************************************************************/
+	/*                      decode list of vertices                     */
+	/********************************************************************/
+
+	public Vector decode(Vector code) {
+		Enumeration e1=code.elements();
+		Vector vec=new Vector(10,10);
+
+		while (e1.hasMoreElements()) {
+			int i=((Integer)(e1.nextElement())).intValue();
+			//Vertex vx=getVertexByNum(i);
+			//if (vx!=null) vec.addElement(vx);
+			vec.addElement(vertices2[i]);
+		}
+		return vec;
+	}
+
+	/********************************************************************/
+	/*                       collapse vertices                          */
+	/********************************************************************/
+
+	public void collapse(Vector vs,String name,Vector inflate) {
+		Enumeration e1,e2,e3;
+		boolean nonempty=false;
+		Vertex vx3,vx2,vx1;
+		
+		e1=vertices.elements();
+
+		vx1=new NormalVertex(name);
+		vx1.setInflate(inflate);
+
+		while (e1.hasMoreElements()) {
+			vx2=(Vertex)(e1.nextElement());
+
+			if (vs.indexOf(vx2)<0) {
+				e2=vx2.getParents();
+				while (e2.hasMoreElements()) {
+					vx3=(Vertex)(e2.nextElement());
+					if (vs.indexOf(vx3)>=0) {
+						if (!vx1.isChild(vx2))
+							vx1.addChild(vx2);
+						vx3.removeChild(vx2);
+					}
+				}
+
+				e2=vx2.getChildren();
+				while (e2.hasMoreElements()) {
+					vx3=(Vertex)(e2.nextElement());
+					if (vs.indexOf(vx3)>=0) {
+						if (!vx2.isChild(vx1))
+							vx2.addChild(vx1);
+						vx2.removeChild(vx3);
+					}
+				}
+			} else { nonempty=true; }
+		}
+
+		e1=vs.elements();
+		while (e1.hasMoreElements())
+			try {
+				removeVertex((Vertex)(e1.nextElement()));
+			} catch (NoSuchElementException exn) {}
+
+		if (nonempty) addVertex(vx1);
+	}
+
+	/********************************************************************/
+	/*                      PostScript output                           */
+	/********************************************************************/
+
+	public void PS(String fname,boolean printable) throws IOException {
+		FileOutputStream f = new FileOutputStream(fname);
+		PrintWriter p = new PrintWriter(f, true);
+
+		if (printable)
+			p.println("%!PS-Adobe-2.0\n\n%%BeginProlog");
+		else {
+			p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait");
+			p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y);
+			p.println("%%EndComments\n\n%%BeginProlog");
+		}
+		p.println("/m { moveto } def /l { lineto } def /n { newpath } def");
+		p.println("/s { stroke } def /c { curveto } def");
+		p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub");
+		p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub");
+		p.println("2 div 9 index add 2 index add m pop pop pop pop");
+		p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto");
+		p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def");
+		p.println("%%EndProlog\n");
+		if (printable) {
+			int hsize=max_x-min_x;
+			int vsize=max_y-min_y;
+			if (hsize>vsize) {
+				// Landscape output
+				double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize));
+				double trans_x=50+max_y*scale+(500-scale*vsize)/2.0;
+				double trans_y=50+max_x*scale+(750-scale*hsize)/2.0;
+				p.println(trans_x+" "+trans_y+" translate");
+				p.println("-90 rotate");
+				p.println(scale+" "+(-scale)+" scale");
+			} else {
+				// Portrait output
+				double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize));
+				double trans_x=50-min_x*scale+(500-scale*hsize)/2.0;
+				double trans_y=50+max_y*scale+(750-scale*vsize)/2.0;
+				p.println(trans_x+" "+trans_y+" translate");
+				p.println(scale+" "+(-scale)+" scale");
+			}
+		} else
+			p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale");
+
+		p.println("/Helvetica findfont 12 scalefont setfont");
+		p.println("0.5 setlinewidth");
+
+		Enumeration e1=vertices.elements();
+		while (e1.hasMoreElements())
+			((Vertex)(e1.nextElement())).PS(p);
+
+		e1=splines.elements();
+		while (e1.hasMoreElements())
+			((Spline)(e1.nextElement())).PS(p);
+
+		if (printable) p.println("showpage");
+
+		f.close();
+	}
+}
+
+/**** Return value of function calcPoint ****/
+
+class Points {
+	public Point p,q;
+
+	public Points(Point p1,Point p2) {
+		p=p1;q=p2;
+	}
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,215 @@
+/***************************************************************************
+  Title:      graphbrowser/GraphBrowser.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This is the graph browser's main class. It contains the "main(...)"
+  method, which is used for the stand-alone version, as well as
+  "init(...)", "start(...)" and "stop(...)" methods which are used for
+  the applet version.
+  Note: GraphBrowser is designed for the 1.1.x version of the JDK.
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.*;
+import java.applet.*;
+import java.io.*;
+import java.util.*;
+import java.net.*;
+import isabelle.awt.*;
+
+public class GraphBrowser extends Applet {
+	GraphView gv;
+	TreeBrowser tb=null;
+	String gfname;
+
+	static boolean isApplet;
+	static Frame f;
+
+	public GraphBrowser(String name) {
+		gfname=name;
+	}
+
+	public GraphBrowser() {}
+
+	public void showWaitMessage() {
+		if (isApplet)
+			getAppletContext().showStatus("calculating layout, please wait ...");
+		else {
+			f.setCursor(new Cursor(Cursor.WAIT_CURSOR));
+		}
+	}
+
+	public void showReadyMessage() {
+		if (isApplet)
+			getAppletContext().showStatus("ready !");
+		else {
+			f.setCursor(new Cursor(Cursor.DEFAULT_CURSOR));
+		}
+	}
+
+	public void viewFile(String fname) {
+		try {
+			if (isApplet)
+				getAppletContext().showDocument(new URL(getDocumentBase(), fname), "_blank");
+			else {
+				String path = gfname.substring(0, gfname.lastIndexOf('/') + 1);
+				Reader rd;
+				BufferedReader br;
+				String line, text = "";
+
+				try {
+					rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
+				} catch (Exception exn) {
+					rd = new FileReader(path + fname);
+				}
+				br = new BufferedReader(rd);
+
+				while ((line = br.readLine()) != null)
+					text += line + "\n";
+
+				if (fname.endsWith(".html")) {
+					/**** convert HTML to text (just a quick hack) ****/
+
+					String buf="";
+					char[] text2,text3;
+					int i,j=0;
+					boolean special=false, html=false;
+					char ctrl;
+
+					text2 = text.toCharArray();
+					text3 = new char[text.length()];
+					for (i = 0; i < text.length(); i++) {
+						char c = text2[i];
+						if (c == '&') {
+							special = true;
+							buf = "";
+						} else if (special) {
+							if (c == ';') {
+								special = false;
+								if (buf.equals("lt"))
+									text3[j++] = '<';
+								else if (buf.equals("gt"))
+									text3[j++] = '>';
+								else if (buf.equals("amp"))
+									text3[j++] = '&';
+							} else
+								buf += c;
+						} else if (c == '<') {
+							html = true;
+							ctrl = text2[i+1];
+						} else if (c == '>')
+							html = false;
+						else if (!html)
+							text3[j++] = c;
+					}
+					text = String.valueOf(text3);
+				}
+							
+				Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
+				f.setSize(500,600);
+				f.setVisible(true);
+			}
+		} catch (Exception exn) {
+			System.err.println("Can't read file "+fname);
+		}
+	}
+				
+	public void PS(String fname,boolean printable) throws IOException {
+		gv.PS(fname,printable);
+	}
+
+	public boolean isEmpty() {
+		return tb==null;
+	}
+
+	public void initBrowser(InputStream is, boolean noAWT) {
+		try {
+			Font font = noAWT ? null : new Font("Helvetica", Font.PLAIN, 12);
+			TreeNode tn = new TreeNode("Root", "", -1, true);
+			gv = new GraphView(new Graph(is, tn), this, font);
+			tb = new TreeBrowser(tn, gv, font);
+			gv.setTreeBrowser(tb);
+			Vector v = new Vector(10,10);
+			tn.collapsedDirectories(v);
+			gv.collapseDir(v);
+
+			ScrollPane scrollp1 = new ScrollPane();
+			ScrollPane scrollp2 = new ScrollPane();
+			scrollp1.add(gv);
+			scrollp2.add(tb);
+			scrollp1.getHAdjustable().setUnitIncrement(20);
+			scrollp1.getVAdjustable().setUnitIncrement(20);
+			scrollp2.getHAdjustable().setUnitIncrement(20);
+			scrollp2.getVAdjustable().setUnitIncrement(20);
+			Component gv2 = new Border(scrollp1, 3);
+			Component tb2 = new Border(scrollp2, 3);
+			GridBagLayout gridbag = new GridBagLayout();
+			GridBagConstraints cnstr = new GridBagConstraints();
+			setLayout(gridbag);
+			cnstr.fill = GridBagConstraints.BOTH;
+			cnstr.insets = new Insets(5,5,5,5);
+			cnstr.weightx = 1;
+			cnstr.weighty = 1;
+			cnstr.gridwidth = 1;
+			gridbag.setConstraints(tb2,cnstr);
+			add(tb2);
+			cnstr.weightx = 2.5;
+			cnstr.gridwidth = GridBagConstraints.REMAINDER;
+			gridbag.setConstraints(gv2,cnstr);
+			add(gv2);
+		} catch (IOException exn) {
+			System.err.println("\nI/O error while reading graph file.");
+		} catch (ParseError exn) {
+			System.err.println("\nParse error in graph file:");
+			System.err.println(exn.getMessage());
+			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
+		}
+	}		
+
+	public void init() {
+		isApplet=true;
+		gfname=getParameter("graphfile");
+		try {
+			InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
+			initBrowser(is, false);
+			is.close();
+		} catch (MalformedURLException exn) {
+			System.err.println("Invalid URL: "+gfname);
+		} catch (IOException exn) {
+			System.err.println("I/O error while reading "+gfname+".");
+		}
+	}
+
+	public static void main(String[] args) {
+		isApplet=false;
+		try {
+			GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
+			if (args.length > 0) {
+				InputStream is=new FileInputStream(args[0]);
+				gb.initBrowser(is, args.length > 1);
+				is.close();
+			}
+			if (args.length > 1) {
+                            try {
+			      if (args[1].endsWith(".ps"))
+                                gb.gv.PS(args[1], true);
+                              else if (args[1].endsWith(".eps"))
+                                gb.gv.PS(args[1], false);
+                              else
+                                System.err.println("Unknown file type: " + args[1]);
+                            } catch (IOException exn) {
+                              System.err.println("Unable to write file " + args[1]);
+                            }
+                        } else {
+			    f=new GraphBrowserFrame(gb);
+			    f.setSize(700,500);
+			    f.setVisible(true);
+                        }
+		} catch (IOException exn) {
+			System.err.println("Can't open graph file "+args[0]);
+		}
+	}
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,125 @@
+/***************************************************************************
+  Title:      graphbrowser/GraphBrowserFrame.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=2:
+
+  This class is the frame for the stand-alone application. It contains
+  methods for handling menubar events.
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.*;
+import java.awt.event.*;
+import java.io.*;
+import isabelle.awt.*;
+
+public class GraphBrowserFrame extends Frame implements ActionListener {
+	GraphBrowser gb;
+	MenuItem i1, i2;
+	String graphDir, psDir;
+
+	public void checkMenuItems() {
+		if (gb.isEmpty()) {
+			i1.setEnabled(false);
+			i2.setEnabled(false);
+		} else {
+			i1.setEnabled(true);
+			i2.setEnabled(true);
+		}
+	}
+
+	public void actionPerformed(ActionEvent evt) {
+		String label = evt.getActionCommand();
+		if (label.equals("Quit"))
+			System.exit(0);
+		else if (label.equals("Export to PostScript")) {
+			PS(true, label);
+			return;
+		} else if (label.equals("Export to EPS")) {
+			PS(false, label);
+			return;
+		} else if (label.equals("Open ...")) {
+			FileDialog fd = new FileDialog(this, "Open graph file", FileDialog.LOAD);
+			if (graphDir != null)
+				fd.setDirectory(graphDir);
+			fd.setVisible(true);
+			if (fd.getFile() == null) return;
+			graphDir = fd.getDirectory();
+			String fname = graphDir + fd.getFile();
+			GraphBrowser gb2 = new GraphBrowser(fname);
+			try {
+				InputStream is = new FileInputStream(fname);
+				gb2.initBrowser(is, false);
+				is.close();
+			} catch (IOException exn) {
+				String button[] = {"OK"};
+				MessageDialog md = new MessageDialog(this, "Error",
+					"Can't open file " + fname + ".", button);
+				md.setSize(350, 200);
+				md.setVisible(true);
+				return;
+			}
+			remove(gb);
+			add("Center", gb2);
+			gb = gb2;
+			checkMenuItems();
+			validate();
+		}
+	}
+
+	public void PS(boolean printable,String label) {
+		FileDialog fd=new FileDialog(this,label,FileDialog.SAVE);
+		if (psDir!=null)
+			fd.setDirectory(psDir);
+		fd.setVisible(true);
+		if (fd.getFile()==null) return;
+		psDir=fd.getDirectory();
+		String fname=psDir+fd.getFile();
+
+		if ((new File(fname)).exists()) {
+			String buttons[]={"Overwrite","Cancel"};
+			MessageDialog md=new MessageDialog(this,"Warning",
+			      "Warning: File "+fname+" already exists. Overwrite?",
+			      buttons);
+			md.setSize(350,200);
+			md.setVisible(true);
+			if (md.getText().equals("Cancel")) return;
+		}
+
+		try {
+			gb.PS(fname,printable);
+		} catch (IOException exn) {
+			String button[]={"OK"};
+			MessageDialog md=new MessageDialog(this,"Error",
+			      "Unable to write file "+fname+".",button);
+			md.setSize(350,200);
+			md.setVisible(true);
+		}
+	}
+
+	public GraphBrowserFrame(GraphBrowser br) {
+		super("GraphBrowser");
+		MenuItem i3, i4;
+		gb = br;
+		MenuBar mb = new MenuBar();
+		Menu m1 = new Menu("File");
+		m1.add(i3 = new MenuItem("Open ..."));
+		m1.add(i1 = new MenuItem("Export to PostScript"));
+		m1.add(i2 = new MenuItem("Export to EPS"));
+		m1.add(i4 = new MenuItem("Quit"));
+		i1.addActionListener(this);
+		i2.addActionListener(this);
+		i3.addActionListener(this);
+		i4.addActionListener(this);
+		checkMenuItems();
+		mb.add(m1);
+		setMenuBar(mb);
+		add("Center", br);
+    addWindowListener( new WindowAdapter() {
+      public void windowClosing(WindowEvent e) {
+        System.exit(0);
+      }
+    });
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphView.java	Fri Jul 16 22:32:56 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) {}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/NormalVertex.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,154 @@
+/***************************************************************************
+  Title:      graphbrowser/NormalVertex.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This class represents an ordinary vertex. It contains methods for
+  drawing and PostScript output.
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.util.*;
+import java.awt.*;
+import java.io.*;
+
+class NormalVertex extends Vertex {
+	String label="",path="",dir="",ID="";
+	Vector up,down,inflate=null;
+
+	public Object clone() {
+		Vertex ve=new NormalVertex(label);
+                ve.setID(ID);
+		ve.setNumber(getNumber());
+		ve.setUp(getUp());ve.setDown(getDown());
+		ve.setX(getX());ve.setY(getY());
+		ve.setPath(getPath());
+		return ve;
+	}
+
+	/*** Constructor ***/
+
+	public NormalVertex(String s) { label=s; }
+
+	public void setInflate(Vector v) { inflate=v; }
+
+	public Vector getInflate() { return inflate; }
+
+	public Vector getUp() { return up; }
+
+	public void setUp(Vector v) { up=v; }
+
+	public Vector getDown() { return down; }
+
+	public void setDown(Vector v) { down=v; }
+
+	public String getLabel() {return label;}
+
+	public void setLabel(String s) {label=s;}
+
+	public void setID(String s) { ID=s; }
+
+        public String getID() { return ID; }
+
+	public String getPath() { return path;}
+
+	public void setPath(String p) { path=p; }
+
+	public String getDir() { return dir; }
+
+	public void setDir(String d) { dir=d; }
+
+	public int leftX() { return getX()-box_width2(); }
+
+	public int rightX() { return getX()+box_width2(); }
+
+	public void drawBox(Graphics g,Color boxColor) {
+		FontMetrics fm = g.getFontMetrics(g.getFont());
+		int h=fm.getAscent()+fm.getDescent();
+
+		g.setColor(boxColor);
+		g.fillRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
+		g.setColor(Color.black);
+		g.drawRect(getX()-box_width2(),getY(),box_width(),gra.box_height);
+		if (getNumber()<0)
+			g.setColor(Color.red);
+
+		g.drawString(label,
+		             (int)Math.round((box_width()-fm.stringWidth(label))/2.0)+getX()-box_width2(),
+				fm.getAscent()+(int)Math.round((gra.box_height-h)/2.0)+getY());
+	}
+
+	public void removeButtons(Graphics g) {
+		drawBox(g,Color.lightGray);
+	}
+
+	public void draw(Graphics g) {
+		drawBox(g,Color.lightGray);
+		g.setColor(Color.black);
+		Enumeration e1=getChildren();
+		while (e1.hasMoreElements()) {
+			Vertex v=(Vertex)(e1.nextElement());
+			if (!v.isDummy())
+				g.drawLine(getX(),getY()+gra.box_height,v.getX(),v.getY());
+		}
+	}
+
+	public boolean contains(int x,int y) {
+		return (x>=leftX() && x<=rightX() && y>=getY() &&
+                        y<=getY()+gra.box_height);
+	}
+
+	public boolean leftButton(int x,int y) {
+		return contains(x,y) && x<=leftX()+gra.box_height && getParents().hasMoreElements() && getNumber()>=0;
+	}
+
+	public boolean rightButton(int x,int y) {
+		return contains(x,y) && x>=rightX()-gra.box_height && getChildren().hasMoreElements() && getNumber()>=0;
+	}
+
+	public void drawButtons(Graphics g) {
+		if (getNumber()<0) return;
+
+		int l=gra.box_height*2/3,d=gra.box_height/6;
+		int up_x[] = { leftX()+d , leftX()+d+l/2 , leftX()+d+l };
+		int up_y[] = { getY()+d+l , getY()+d , getY()+d+l };
+		int down_x[] = { rightX()-d-l , rightX()-d-l/2 , rightX()-d };
+		int down_y[] = { getY()+d , getY()+d+l , getY()+d };
+
+		if (getParents().hasMoreElements()) {
+			g.setColor(Color.gray);
+			g.fillRect(leftX()+1,getY()+1,gra.box_height-1,gra.box_height-1);
+			g.setColor(getUp()!=null ? Color.red : Color.green);
+			g.fillPolygon(up_x,up_y,3);
+		}
+		if (getChildren().hasMoreElements()) {
+			g.setColor(Color.gray);
+			g.fillRect(rightX()+1-gra.box_height,getY()+1,gra.box_height,gra.box_height-1);
+			g.setColor(getDown()!=null ? Color.red : Color.green);
+			g.fillPolygon(down_x,down_y,3);
+		}
+		g.setColor(Color.black);
+	}
+
+	public void PS(PrintWriter p) {
+		p.print(leftX()+" "+getY()+" "+box_width()+" "+
+		        gra.box_height+" (");
+		for (int i=0;i<label.length();i++)
+		{
+			if (("()\\").indexOf(label.charAt(i))>=0)
+				p.print("\\");
+			p.print(label.charAt(i));
+		}
+		p.println(") b");
+
+		Enumeration e1=getChildren();
+		while (e1.hasMoreElements()) {
+			Vertex v=(Vertex)(e1.nextElement());
+			if (!v.isDummy())
+				p.println("n "+getX()+" "+(getY()+gra.box_height)+
+				" m "+v.getX()+" "+v.getY()+" l s");
+		}
+	}	
+}
+		
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/ParseError.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,5 @@
+package isabelle.graphbrowser;
+
+class ParseError extends Exception {
+	public ParseError(String s) { super(s); }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Region.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,89 @@
+/***************************************************************************
+  Title:      graphbrowser/Region.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This is an auxiliary class which is used by the layout algorithm when
+  calculating coordinates with the "pendulum method". A "region" is a
+  group of nodes which "stick together".
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.util.*;
+
+class Region {
+	Vector vertices=new Vector(10,10);
+	Graph gra;
+
+	public Region(Graph g) { gra=g; }
+
+	public void addVertex(Vertex v) {
+		vertices.addElement(v);
+	}
+
+	public Enumeration getVertices() {
+		return vertices.elements();
+	}
+
+	public int pred_deflection() {
+		float d1=0;
+		int n=0;
+		Enumeration e1=vertices.elements();
+		while (e1.hasMoreElements()) {
+			float d2=0;
+			int p=0;
+			n++;
+			Vertex v=(Vertex)(e1.nextElement());
+			Enumeration e2=v.getParents();
+			while (e2.hasMoreElements()) {
+				p++;
+				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
+			}
+			if (p>0) d1+=d2/p;
+		}
+		return (int)(Math.round(d1/n));
+	}
+
+	public int succ_deflection() {
+		float d1=0;
+		int n=0;
+		Enumeration e1=vertices.elements();
+		while (e1.hasMoreElements()) {
+			float d2=0;
+			int p=0;
+			n++;
+			Vertex v=(Vertex)(e1.nextElement());
+			Enumeration e2=v.getChildren();
+			while (e2.hasMoreElements()) {
+				p++;
+				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
+			}
+			if (p>0) d1+=d2/p;
+		}
+		return (int)(Math.round(d1/n));
+	}
+
+	public void move(int x) {
+		Enumeration e1=vertices.elements();
+		while (e1.hasMoreElements()) {
+			Vertex v=(Vertex)(e1.nextElement());
+			v.setX(v.getX()+x);
+		}
+	}
+
+	public void combine(Region r2) {
+		Enumeration e1=r2.getVertices();
+		while (e1.hasMoreElements()) addVertex((Vertex)(e1.nextElement()));
+	}
+
+	public int spaceBetween(Region r2) {
+		return ((Vertex)(r2.getVertices().nextElement())).leftX()-
+			((Vertex)(vertices.lastElement())).rightX()-
+			20;
+	}
+
+	public boolean touching(Region r2) {
+		return spaceBetween(r2)==0;
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Spline.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,120 @@
+/***************************************************************************
+  Title:      graphbrowser/Spline.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This class is used for drawing spline curves (which are not yet
+  supported by the Java AWT).
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.*;
+import java.util.*;
+import java.io.*;
+
+class SplineSection {
+
+	/*** Section of a spline function ***/
+
+	double x_b,x_c,x_d;
+	double y_b,y_c,y_d;
+	int dx,dy;
+
+	public SplineSection(double xb,double xc,double xd,
+		double yb,double yc,double yd,int dx2,int dy2) {
+		x_b=xb;x_c=xc;x_d=xd;
+		y_b=yb;y_c=yc;y_d=yd;
+		dx=dx2;dy=dy2;
+	}
+
+	public Point draw(Graphics g,Point s) {
+		double m;
+		int s_x,s_y,e_x=0,e_y=0;
+		int x,y;
+
+		s_x=s.x;s_y=s.y;
+		if (dx>=dy) {
+			if (dx==0) return s;
+			m=1/((double)dx);
+			for (x=0;x<dx;x++) {
+				e_x=(int)(Math.round((x_b*x*m+x_c)*x*m+x_d));
+				e_y=(int)(Math.round((y_b*x*m+y_c)*x*m+y_d));
+				g.drawLine(s_x,s_y,e_x,e_y);
+				s_x=e_x;s_y=e_y;
+			}
+		} else {
+			m=1/((double)dy);
+			for (y=0;y<dy;y++) {
+				e_x=(int)(Math.round((x_b*y*m+x_c)*y*m+x_d));
+				e_y=(int)(Math.round((y_b*y*m+y_c)*y*m+y_d));
+				g.drawLine(s_x,s_y,e_x,e_y);
+				s_x=e_x;s_y=e_y;
+			}
+		}
+		return new Point(e_x,e_y);
+	}
+}
+
+public class Spline {
+
+	Vector sections;
+	Vector points;
+	Point start,end;
+
+	public Spline(Vector pts) {
+		int i;
+		double d0,d1,d2,d3;
+		Point p0,p1,p2;
+		SplineSection s;
+		
+		start=(Point)(pts.firstElement());
+		end=(Point)(pts.lastElement());
+
+		sections=new Vector(10,10);
+		for (i=1;i<=pts.size()-4;i+=3) {
+			p0=(Point)(pts.elementAt(i));
+			p1=(Point)(pts.elementAt(i+1));
+			p2=(Point)(pts.elementAt(i+2));
+			s=new SplineSection(
+				(double)(p2.x-2*p1.x+p0.x),
+				2.0*(p1.x-p0.x),
+				(double)(p0.x),
+
+				(double)(p2.y-2*p1.y+p0.y),
+				2.0*(p1.y-p0.y),
+				(double)(p0.y),
+
+				Math.abs(p2.x-p0.x),
+				Math.abs(p2.y-p0.y)
+			);
+
+			sections.addElement(s);
+		}
+		points=pts;
+	}
+
+	public void draw(Graphics g) {
+		Enumeration e1=sections.elements();
+		Point p=start;
+
+		while (e1.hasMoreElements())
+			p=((SplineSection)(e1.nextElement())).draw(g,p);
+		g.drawLine(p.x,p.y,end.x,end.y);
+	}
+
+	public void PS(PrintWriter p) {
+		Point p0,p1,p2;
+		int i;
+
+		p.println("n "+start.x+" "+start.y+" m");
+		for (i=1;i<=points.size()-4;i+=3) {
+			p0=(Point)(points.elementAt(i));
+			p1=(Point)(points.elementAt(i+1));
+			p2=(Point)(points.elementAt(i+2));
+			p.println(p0.x+" "+p0.y+" l");
+			p.println(p0.x+" "+p0.y+" "+p1.x+" "+p1.y+" "+p2.x+" "+p2.y+" c");
+		}
+		p.println(end.x+" "+end.y+" l s");
+	}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/TreeBrowser.java	Fri Jul 16 22:32:56 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();
+		}
+	}
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/TreeNode.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,168 @@
+/***************************************************************************
+  Title:      graphbrowser/TreeNode.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This class contains methods for storing and manipulating directory
+  trees (e.g. collapsing / uncollapsing directory branches).
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.awt.*;
+import java.util.*;
+
+
+public class TreeNode
+{
+	int starty,endy,number;
+	String name,path;
+
+	Vector leaves=new Vector(10,10);
+	boolean unfold=false;
+
+	public void insertNode(String n,String d,String p,int num,boolean u) {
+		if (d.length()==0) {
+			leaves.addElement(new TreeNode(n,p,num));
+			unfold=unfold||u;
+		} else {
+			unfold=unfold||u;
+			String str1,str2;
+			if (d.indexOf('/')<0) {
+				str1=d;str2="";
+			} else {
+				str1=d.substring(0,d.indexOf('/'));
+				str2=d.substring(d.indexOf('/')+1);
+			}
+
+			Enumeration e1=leaves.elements();
+			TreeNode nd=null;
+
+			while (e1.hasMoreElements()) {
+				TreeNode nd2=(TreeNode)(e1.nextElement());
+				if (nd2.name.equals(str1)) {
+					nd=nd2;break;
+				}
+			}
+			if (nd==null) {
+				nd=new TreeNode(str1,"",-1);
+				leaves.addElement(nd);
+			}
+			nd.insertNode(n,str2,p,num,u);
+		}
+	}
+
+	public TreeNode(String n,String p,int num) {
+		name=n;
+		path=p;
+		number=num;
+	}
+
+	public TreeNode(String n,String p,int num,boolean u) {
+		this(n,p,num);
+		unfold=u;
+	}	
+
+	public int getNumber() { return number; }
+
+	public TreeNode lookup(int y)
+	{
+		if (y>=starty && y<endy) return this;
+		else
+		if (unfold)
+			for (int i=0;i<leaves.size();i++)
+			{
+				TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
+				if (t!=null) return t;
+			}
+		return null;
+	}
+
+	public boolean select()
+	{
+		if (!leaves.isEmpty()) {
+			if (unfold) collapse();
+			else unfold=true;
+			return true;
+		}
+		return false; 
+	}
+
+	public void collapse()
+	{
+		unfold=false;
+		/*Integer.valueOf
+		for(int i=0;i<leaves.size();i++)
+			((Tree)leaves.elementAt(i)).collapse();
+		*/
+	}
+
+	void collapsedNodes(Vector v) {
+		if (number>=0) v.addElement(Integer.valueOf(number));
+		Enumeration e1=leaves.elements();
+		while (e1.hasMoreElements())
+			((TreeNode)(e1.nextElement())).collapsedNodes(v);
+	}
+
+	public void collapsedDirectories(Vector v) {
+		if (!unfold) {
+			Vector v2=new Vector(10,10);
+			v.addElement(new Directory(this,name,v2));
+			collapsedNodes(v2);
+		} else {
+			Enumeration e1=leaves.elements();
+			while (e1.hasMoreElements()) {
+				TreeNode tn=(TreeNode)(e1.nextElement());
+				if (!tn.leaves.isEmpty())
+					tn.collapsedDirectories(v);
+			}
+		}
+	}
+
+	public Dimension draw(Graphics g,int x,int y,TreeNode t)
+	{
+		FontMetrics fm=g.getFontMetrics(g.getFont());
+		int h=fm.getHeight();
+		int e=(int) (h / 10) + 1;
+		int down_x[]={x + e, x + h - e, x + (int)(h / 2)};
+		int down_y[]={y + e, y + e, y + (int)(3 * h / 4) - e};
+		int right_x[]={x + e, x + (int)(3 * h / 4) - e, x + e};
+		int right_y[]={y + e, y + (int)(h / 2), y + h - e};
+		int dx=0;
+
+		if (unfold)
+		{
+			g.setColor(Color.green);
+			g.fillPolygon(down_x,down_y,3);
+			g.setColor(Color.black);
+			g.drawString(name,x+h+4,y+fm.getAscent());
+			starty=y;endy=y+h;
+			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
+			y+=h+5;
+			for(int i=0;i<leaves.size();i++)
+			{
+				Dimension d=((TreeNode)leaves.elementAt(i)).draw(g,x+h+4,y,t);
+				y=d.height;
+				dx=Math.max(dx,d.width);
+			}
+		}
+		else
+		{
+			g.setColor(leaves.isEmpty() ? Color.blue : Color.red);
+			g.fillPolygon(right_x,right_y,3);
+			if (this==t && leaves.isEmpty())
+			{
+				g.setColor(Color.white);
+				g.fillRect(x+h+4,y,fm.stringWidth(name),h);
+			}
+			g.setColor(Color.black);
+			g.drawString(name,x+h+4,y+fm.getAscent());
+			starty=y;endy=y+h;
+			dx=Math.max(dx,x+h+4+fm.stringWidth(name));
+			y+=h+5;
+		}
+		return new Dimension(dx,y);
+	}
+}
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Vertex.java	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,213 @@
+/***************************************************************************
+  Title:      graphbrowser/Vertex.java
+  Author:     Stefan Berghofer, TU Muenchen
+  Options:    :tabSize=4:
+
+  This class contains attributes and methods common to all kinds of
+  vertices (e.g. coordinates, successors, predecessors).
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.util.*;
+import java.awt.*;
+import java.io.*;
+
+abstract class Vertex {
+	Vector children=new Vector(10,10);
+	Vector parents=new Vector(10,10);
+	int degree=0;
+	int number=-1;
+	double weight=0;
+	int x,y;
+	Graph gra;
+
+	public abstract Object clone();
+
+	public void setGraph(Graph g) { gra=g; }
+
+	public int countChildren() { return children.size(); }
+
+	/** getInflate returns a vector of vertices which get **/
+	/** inflated again if the user clicks on this vertex  **/
+
+	public void setInflate(Vector v) {}
+
+	public Vector getInflate() { return null; }
+
+	/** getUp returns a vector of vertices which get inflated   **/
+	/** again, if the user clicks on this vertex's upward arrow **/
+
+	public Vector getUp() { return null; }
+
+	public void setUp(Vector v) {}
+
+	/** getUp returns a vector of vertices which get inflated     **/
+	/** again, if the user clicks on this vertex's downward arrow **/
+
+	public Vector getDown() { return null; }
+
+	public void setDown(Vector v) {}
+
+	/** internal number, for decoding / encoding etc. **/
+
+	public int getNumber() { return number; }
+
+	public void setNumber(int n) { number=n; }
+
+	public String getLabel() {return "";}
+
+	public void setLabel(String s) {}
+
+	/** unique identifier **/
+
+	public String getID() {return "";}
+
+	public void setID(String s) {}
+
+	public Box getLabelSize(Graphics g) {
+		AbstractFontMetrics fm = g == null ? 
+      (AbstractFontMetrics) new DefaultFontMetrics(12) : 
+      (AbstractFontMetrics) new AWTFontMetrics(g.getFontMetrics(g.getFont()));
+		
+		return new Box(Math.max(fm.stringWidth("[. . . .]"),
+                            fm.stringWidth(getLabel())),
+                   fm.getAscent()+fm.getDescent());
+	}
+		
+	public String getPath() { return "";}
+
+	public void setPath(String p) {}
+
+	public String getDir() { return ""; }
+
+	public void setDir(String d) {}
+
+	public void setWeight(double w) {weight=w;}
+
+	public double getWeight() {return weight;}
+
+	public void setDegree(int d) { degree=d; }
+
+	public int getDegree() { return degree; }
+
+	public boolean isDummy() { return false; }
+
+	public Enumeration getChildren() {
+		return ((Vector)(children.clone())).elements();
+	}
+
+	public void addChild(Vertex v) {
+		children.addElement(v);
+		v.parents.addElement(this);
+	}
+
+	public void removeChild(Vertex v) {
+		children.removeElement(v);
+		v.parents.removeElement(this);
+	}
+
+	public boolean isChild(Vertex v) {
+		return children.indexOf(v)>=0;
+	}
+
+	public boolean isParent(Vertex v) {
+		return parents.indexOf(v)>=0;
+	}
+
+	public Enumeration getParents() {
+		return ((Vector)(parents.clone())).elements();
+	}
+
+	public void addParent(Vertex v) {
+		parents.addElement(v);
+		v.children.addElement(this);
+	}
+
+	public void removeParent(Vertex v) {
+		parents.removeElement(v);
+		v.children.removeElement(this);
+	}
+
+	/********************************************************************/
+	/*                   get all predecessor vertices                   */
+	/********************************************************************/
+
+	public Vector getPreds() {
+	    Vector preds=new Vector(10,10);
+	    Vector todo=(Vector)(parents.clone());
+	    Vertex vx1,vx2;
+	    Enumeration e;
+
+	    while (!todo.isEmpty()) {
+		vx1=(Vertex)(todo.lastElement());
+		todo.removeElementAt(todo.size()-1);
+		preds.addElement(vx1);
+		e=vx1.parents.elements();
+		while (e.hasMoreElements()) {
+		    vx2=(Vertex)(e.nextElement());
+		    if (preds.indexOf(vx2)<0 && todo.indexOf(vx2)<0)
+			todo.addElement(vx2);
+		}
+	    }
+
+	    return preds;
+	}
+
+	/********************************************************************/
+	/*                     get all successor vertices                   */
+	/********************************************************************/
+
+	public Vector getSuccs() {
+	    Vector succs=new Vector(10,10);
+	    Vector todo=(Vector)(children.clone());
+	    Vertex vx1,vx2;
+	    Enumeration e;
+
+	    while (!todo.isEmpty()) {
+		vx1=(Vertex)(todo.lastElement());
+		todo.removeElementAt(todo.size()-1);
+		succs.addElement(vx1);
+		e=vx1.children.elements();
+		while (e.hasMoreElements()) {
+		    vx2=(Vertex)(e.nextElement());
+		    if (succs.indexOf(vx2)<0 && todo.indexOf(vx2)<0)
+			todo.addElement(vx2);
+		}
+	    }
+
+	    return succs;
+	}
+
+	public int box_width() { return getLabelSize(gra.gfx).width+8; }
+
+	public int box_width2() { return box_width()/2; }
+
+	public void setX(int x) {this.x=x;}
+
+	public void setY(int y) {this.y=y;}
+
+	public int getX() {return x;}
+
+	public int getY() {return y;}
+
+	public abstract int leftX();
+
+	public abstract int rightX();
+
+	public abstract void draw(Graphics g);
+
+	public void drawButtons(Graphics g) {}
+
+	public void drawBox(Graphics g,Color boxColor) {}
+
+	public void removeButtons(Graphics g) {}
+
+	public boolean contains(int x,int y) { return false; }
+
+	public boolean leftButton(int x,int y) { return false; }
+
+	public boolean rightButton(int x,int y) { return false; }
+
+	public void PS(PrintWriter p) {}
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/lib/Tools/browser	Fri Jul 16 22:32:56 2021 +0200
@@ -0,0 +1,108 @@
+#!/usr/bin/env bash
+#
+# Author: Markus Wenzel, TU Muenchen
+#
+# DESCRIPTION: Isabelle graph browser
+
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
+  echo
+  echo "  Options are:"
+  echo "    -b           Admin/build only"
+  echo "    -c           cleanup -- remove GRAPHFILE after use"
+  echo "    -o FILE      output to FILE (ps, eps, pdf)"
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+ADMIN_BUILD=""
+CLEAN=""
+OUTFILE=""
+
+while getopts "bco:" OPT
+do
+  case "$OPT" in
+    b)
+      ADMIN_BUILD=true
+      ;;
+    c)
+      CLEAN=true
+      ;;
+    o)
+      OUTFILE="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+GRAPHFILE=""
+[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+isabelle_scala_build || exit $?
+
+if [ -n "$GRAPHFILE" ]; then
+  PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
+  if [ -n "$CLEAN" ]; then
+    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
+  else
+    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
+  fi
+
+  PDF=""
+  case "$OUTFILE" in
+    *.pdf)
+      OUTFILE="${OUTFILE%%.pdf}.eps"
+      PDF=true
+      ;;
+  esac
+
+  if [ -z "$OUTFILE" ]; then
+    isabelle java isabelle.graphbrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
+  else
+    isabelle java isabelle.graphbrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
+  fi
+  RC="$?"
+
+  if [ -n "$PDF" ]; then
+    (
+      cd "$(dirname "$OUTFILE")"
+      "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
+    )
+  fi
+
+  rm -f "$PRIVATE_FILE"
+elif [ -z "$ADMIN_BUILD" ]; then
+  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
+  exec isabelle java isabelle.graphbrowser.GraphBrowser
+else
+  RC=0
+fi
+
+exit "$RC"
--- a/src/Tools/Setup/isabelle/setup/Build.java	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Fri Jul 16 22:32:56 2021 +0200
@@ -8,8 +8,13 @@
 
 
 import java.io.BufferedOutputStream;
+import java.io.ByteArrayInputStream;
+import java.io.ByteArrayOutputStream;
+import java.io.CharArrayWriter;
 import java.io.File;
 import java.io.IOException;
+import java.io.InputStream;
+import java.io.PrintStream;
 import java.math.BigInteger;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
@@ -196,6 +201,15 @@
         }
     }
 
+    private static void compiler_result(boolean ok, String out, String what)
+    {
+        if (ok) { if (!out.isEmpty()) { System.err.println(out); } }
+        else {
+            String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out);
+            throw new RuntimeException(msg);
+        }
+    }
+
     public static void compile_scala_sources(
         Path target_dir, String more_options, List<Path> deps, List<Path> sources)
         throws IOException, InterruptedException
@@ -215,9 +229,29 @@
             if (p.toString().endsWith(".scala")) { scala_sources = true; }
         }
         if (scala_sources) {
-            MainClass main = new MainClass();
-            boolean ok = main.process(args.toArray(String[]::new));
-            if (!ok) throw new RuntimeException("Failed to compile Scala sources");
+            boolean ok = false;
+
+            InputStream in_orig = System.in;
+            PrintStream out_orig = System.out;
+            PrintStream err_orig = System.err;
+            ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]);
+            ByteArrayOutputStream out = new ByteArrayOutputStream();
+
+            // Single-threaded context!
+            try {
+                PrintStream out_stream = new PrintStream(out);
+                System.setIn(in);
+                System.setOut(out_stream);
+                System.setErr(out_stream);
+                ok = new MainClass().process(args.toArray(String[]::new));
+                out_stream.flush();
+            }
+            finally {
+                System.setIn(in_orig);
+                System.setOut(out_orig);
+                System.setErr(err_orig);
+            }
+            compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources");
         }
     }
 
@@ -245,9 +279,12 @@
                 }
             }
         }
+
         if (!java_sources.isEmpty()) {
-            boolean ok = compiler.getTask(null, file_manager, null, options, null, java_sources).call();
-            if (!ok) throw new RuntimeException("Failed to compile Java sources");
+            CharArrayWriter out = new CharArrayWriter();
+            boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call();
+            out.flush();
+            compiler_result(ok, out.toString(), "Java sources");
         }
     }
 
--- a/src/Tools/Setup/isabelle/setup/Library.java	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Tools/Setup/isabelle/setup/Library.java	Fri Jul 16 22:32:56 2021 +0200
@@ -33,13 +33,9 @@
     {
         if (str.isEmpty()) { return str; }
         else {
-            StringBuilder result = new StringBuilder();
-            for (String s : split_lines(str)) {
-                result.append(prfx);
-                result.append(s);
-                result.append('\n');
-            }
-            return result.toString();
+            List<String> lines = new LinkedList<String>();
+            for (String line : split_lines(str)) { lines.add(prfx + line); }
+            return cat_lines(lines);
         }
     }
 
--- a/src/Tools/jEdit/jedit_base/plugin.props	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Tools/jEdit/jedit_base/plugin.props	Fri Jul 16 22:32:56 2021 +0200
@@ -6,7 +6,7 @@
 plugin.isabelle.jedit_base.Plugin.name=Isabelle Base
 plugin.isabelle.jedit_base.Plugin.author=Makarius Wenzel
 plugin.isabelle.jedit_base.Plugin.version=1.0
-plugin.isabelle.jedit_base.Plugin.description=Isabelle Base: DO NOT UNLOAD!
+plugin.isabelle.jedit_base.Plugin.description=Isabelle/jEdit base plugin: DO NOT UNLOAD!
 
 #system parameters
 plugin.isabelle.jedit_base.Plugin.activate=startup
--- a/src/Tools/jEdit/jedit_main/plugin.props	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Tools/jEdit/jedit_main/plugin.props	Fri Jul 16 22:32:56 2021 +0200
@@ -3,10 +3,10 @@
 ##:wrap=soft:maxLineLen=100:
 
 #identification
-plugin.isabelle.jedit_main.Plugin.name=Isabelle
+plugin.isabelle.jedit_main.Plugin.name=Isabelle Main
 plugin.isabelle.jedit_main.Plugin.author=Johannes H\u00F6lzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
 plugin.isabelle.jedit_main.Plugin.version=11.2
-plugin.isabelle.jedit_main.Plugin.description=Isabelle Prover IDE
+plugin.isabelle.jedit_main.Plugin.description=Isabelle/jEdit main plugin
 
 #system parameters
 plugin.isabelle.jedit_main.Plugin.activate=defer
--- a/src/Tools/jEdit/jedit_main/scala_console.scala	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala	Fri Jul 16 22:32:56 2021 +0200
@@ -34,7 +34,7 @@
       val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
       val str = UTF8.decode_permissive(s)
       GUI_Thread.later {
-        if (global_out == null) System.out.print(str)
+        if (global_out == null) java.lang.System.out.print(str)
         else global_out.writeAttrs(null, str)
       }
       Time.seconds(0.01).sleep()  // FIXME adhoc delay to avoid loosing output
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Jul 16 20:13:12 2021 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jul 16 22:32:56 2021 +0200
@@ -154,12 +154,10 @@
 
 ## main
 
-isabelle_admin_build browser || exit "$?"
-
 if [ -n "$FRESH_BUILD" ]; then
-  isabelle_admin_build jars_fresh || exit "$?"
+  isabelle_scala_build fresh || exit "$?"
 else
-  isabelle_admin_build jars || exit "$?"
+  isabelle_scala_build || exit "$?"
 fi
 
 if [ "$BUILD_ONLY" = false ]