# HG changeset patch # User wenzelm # Date 1626467576 -7200 # Node ID c4c612d92fcc924c0a6c9211e0032b0a8eb48d8f # Parent 4cca14dc577c16c51252c01e85ea7f6799230b56# Parent d609fa3e816d5fa6b727bfcf1dba0cbc2701f200 merged diff -r 4cca14dc577c -r c4c612d92fcc .hgignore --- 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/ diff -r 4cca14dc577c -r c4c612d92fcc Admin/build --- 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 <&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 diff -r 4cca14dc577c -r c4c612d92fcc Admin/build_history --- 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 "$@" diff -r 4cca14dc577c -r c4c612d92fcc Admin/build_release --- 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 "$@" diff -r 4cca14dc577c -r c4c612d92fcc Admin/components/components.sha1 --- 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 diff -r 4cca14dc577c -r c4c612d92fcc Admin/components/main --- 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 diff -r 4cca14dc577c -r c4c612d92fcc bin/isabelle --- 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 "$@" diff -r 4cca14dc577c -r c4c612d92fcc etc/components --- 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 diff -r 4cca14dc577c -r c4c612d92fcc lib/Tools/browser --- 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" diff -r 4cca14dc577c -r c4c612d92fcc lib/Tools/components --- 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[@]}" diff -r 4cca14dc577c -r c4c612d92fcc lib/Tools/console --- 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)" diff -r 4cca14dc577c -r c4c612d92fcc lib/Tools/scala --- 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=() diff -r 4cca14dc577c -r c4c612d92fcc lib/Tools/scalac --- 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 diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/AWTFontMetrics.java --- 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(); - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/AbstractFontMetrics.java --- 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(); -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/Box.java --- 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; - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/Console.java --- 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 [ + ] "+ - "[ < | > ] [ [ ... [ ] ... ] ] ;"); - } - } - - 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]); - } - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/DefaultFontMetrics.java --- 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; - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/Directory.java --- 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; } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/DummyVertex.java --- 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) {} -} - diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/Graph.java --- 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') { - 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=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)=oldcr) return cr; - } - } - } - } - if (l=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;l0) { - if (topdown) { - /** top-down-traversal **/ - - layers2=new Vector(10,10); - for (l=0;l0) - vx1.setWeight(((double)(k))/z); - else if (first) - vx1.setWeight(Double.MAX_VALUE); - for (i=0;i=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=2) { - do { - change=false; - d1=((Region)(l.firstElement())).pred_deflection(); - for (i=0;i 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;i0) offset=-Math.min( - ((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1); - if (d1>=0 && i0 && (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; - } -} - diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/GraphBrowser.java --- 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 [ + ] [ < | > ] [ [ ... [ ] ... ] ] ;"); - } - } - - 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]); - } - } -} - diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/GraphBrowserFrame.java --- 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); - } - }); - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/GraphView.java --- 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) {} -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/NormalVertex.java --- 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=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"); - } - } -} - diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/ParseError.java --- 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); } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/Region.java --- 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; - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/GraphBrowser/Spline.java --- 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=starty && y=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=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) {} -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/awtUtilities/Border.java --- 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); - } -} diff -r 4cca14dc577c -r c4c612d92fcc lib/browser/awtUtilities/MessageDialog.java --- 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&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 diff -r 4cca14dc577c -r c4c612d92fcc lib/scripts/getfunctions --- 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 () diff -r 4cca14dc577c -r c4c612d92fcc src/Pure/Admin/build_release.scala --- 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) } diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/awt/Border.java --- /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); + } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/awt/MessageDialog.java --- /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 [ + ] "+ + "[ < | > ] [ [ ... [ ] ... ] ] ;"); + } + } + + 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]); + } + } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/DefaultFontMetrics.java --- /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; + } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/Directory.java --- /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; } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/DummyVertex.java --- /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) {} +} + diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/Graph.java --- /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') { + 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=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)=oldcr) return cr; + } + } + } + } + if (l=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;l0) { + if (topdown) { + /** top-down-traversal **/ + + layers2=new Vector(10,10); + for (l=0;l0) + vx1.setWeight(((double)(k))/z); + else if (first) + vx1.setWeight(Double.MAX_VALUE); + for (i=0;i=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=2) { + do { + change=false; + d1=((Region)(l.firstElement())).pred_deflection(); + for (i=0;i 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;i0) offset=-Math.min( + ((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1); + if (d1>=0 && i0 && (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; + } +} + diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java --- /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 [ + ] [ < | > ] [ [ ... [ ] ... ] ] ;"); + } + } + + 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]); + } + } +} + diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/GraphBrowserFrame.java --- /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); + } + }); + } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/GraphView.java --- /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) {} +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/NormalVertex.java --- /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=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"); + } + } +} + diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/ParseError.java --- /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); } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/Region.java --- /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; + } +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/graphbrowser/Spline.java --- /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=starty && y=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=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) {} +} diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/GraphBrowser/lib/Tools/browser --- /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" diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/Setup/isabelle/setup/Build.java --- 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 deps, List 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"); } } diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/Setup/isabelle/setup/Library.java --- 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 lines = new LinkedList(); + for (String line : split_lines(str)) { lines.add(prfx + line); } + return cat_lines(lines); } } diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/jEdit/jedit_base/plugin.props --- 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 diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/jEdit/jedit_main/plugin.props --- 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 diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/jEdit/jedit_main/scala_console.scala --- 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 diff -r 4cca14dc577c -r c4c612d92fcc src/Tools/jEdit/lib/Tools/jedit --- 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 ]