src/Tools/GraphBrowser/etc/build.props
author wenzelm
Fri, 16 Jul 2021 12:40:39 +0200
changeset 74013 f114e11fe21d
parent 74011 1d366486a812
child 74015 12b1f4649ab1
permissions -rw-r--r--
clarified directory;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74011
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     1
description = graph browser
74013
f114e11fe21d clarified directory;
wenzelm
parents: 74011
diff changeset
     2
lib = $ISABELLE_HOME/lib/classes
74011
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     3
name = GraphBrowser
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     4
javac_options = -source 7 -target 7
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     5
sources = \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     6
  GraphBrowser/AWTFontMetrics.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     7
  GraphBrowser/AbstractFontMetrics.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     8
  GraphBrowser/Box.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
     9
  GraphBrowser/Console.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    10
  GraphBrowser/DefaultFontMetrics.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    11
  GraphBrowser/Directory.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    12
  GraphBrowser/DummyVertex.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    13
  GraphBrowser/Graph.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    14
  GraphBrowser/GraphBrowser.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    15
  GraphBrowser/GraphBrowserFrame.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    16
  GraphBrowser/GraphView.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    17
  GraphBrowser/NormalVertex.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    18
  GraphBrowser/ParseError.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    19
  GraphBrowser/Region.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    20
  GraphBrowser/Spline.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    21
  GraphBrowser/TreeBrowser.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    22
  GraphBrowser/TreeNode.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    23
  GraphBrowser/Vertex.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    24
  awtUtilities/Border.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    25
  awtUtilities/MessageDialog.java \
1d366486a812 clarified component setup for old graph browser;
wenzelm
parents:
diff changeset
    26
  awtUtilities/TextFrame.java