author | wenzelm |
Sat, 17 Jul 2021 13:42:21 +0200 | |
changeset 74029 | 0701ff55780d |
parent 74015 | 12b1f4649ab1 |
child 79015 | 3befd4d1e6f2 |
permissions | -rw-r--r-- |
74029
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74015
diff
changeset
|
1 |
title = graph browser |
0701ff55780d
clarified build_props: empty module means no build;
wenzelm
parents:
74015
diff
changeset
|
2 |
module = $ISABELLE_HOME/lib/classes/isabelle_graphbrowser.jar |
74011 | 3 |
javac_options = -source 7 -target 7 |
4 |
sources = \ |
|
74015 | 5 |
awt/Border.java \ |
6 |
awt/MessageDialog.java \ |
|
7 |
awt/TextFrame.java \ |
|
8 |
graphbrowser/AWTFontMetrics.java \ |
|
9 |
graphbrowser/AbstractFontMetrics.java \ |
|
10 |
graphbrowser/Box.java \ |
|
11 |
graphbrowser/Console.java \ |
|
12 |
graphbrowser/DefaultFontMetrics.java \ |
|
13 |
graphbrowser/Directory.java \ |
|
14 |
graphbrowser/DummyVertex.java \ |
|
15 |
graphbrowser/Graph.java \ |
|
16 |
graphbrowser/GraphBrowser.java \ |
|
17 |
graphbrowser/GraphBrowserFrame.java \ |
|
18 |
graphbrowser/GraphView.java \ |
|
19 |
graphbrowser/NormalVertex.java \ |
|
20 |
graphbrowser/ParseError.java \ |
|
21 |
graphbrowser/Region.java \ |
|
22 |
graphbrowser/Spline.java \ |
|
23 |
graphbrowser/TreeBrowser.java \ |
|
24 |
graphbrowser/TreeNode.java \ |
|
25 |
graphbrowser/Vertex.java |