--- 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 ]