Diffusion Isabelle 1d366486a812

clarified component setup for old graph browser;
1d366486a812
Actions

Description

clarified component setup for old graph browser;

Details

Provenance

makarius

Authored on

Parents

rISABELLE4f60db51a263: redundant: *.class and *.jar are already ignored;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE1d366486a812: clarified component setup for old graph browser;.Jul 16 2021, 12:11 PM

Changes (64)

Path

Size

Admin/

etc/

AbstractFontMetrics.java

Box.java

Console.java

DefaultFontMetrics.java

GraphBrowserFrame.java

Pure/

Admin/

jEdit/

lib/

Tools/

jedit

	src/

	Tools/	GraphBrowser/
	lib/	browser/

GraphBrowser/

AWTFontMetrics.java

AbstractFontMetrics.java

Box.java

Console.java

DefaultFontMetrics.java

GraphBrowserFrame.java

awtUtilities/

	Tools/	GraphBrowser/	lib/	Tools/
			lib/	Tools/

browser

rISABELLE1d366486a812

View Options

Admin/build

View Options

etc/components

View Options

lib/Tools/browser

View Options

lib/browser/GraphBrowser/AWTFontMetrics.java

View Options

lib/browser/GraphBrowser/AbstractFontMetrics.java

View Options

lib/browser/GraphBrowser/Box.java

View Options

lib/browser/GraphBrowser/Console.java

View Options

lib/browser/GraphBrowser/DefaultFontMetrics.java

View Options

lib/browser/GraphBrowser/Directory.java

View Options

lib/browser/GraphBrowser/DummyVertex.java

View Options

lib/browser/GraphBrowser/Graph.java

View Options

lib/browser/GraphBrowser/GraphBrowser.java

View Options

lib/browser/GraphBrowser/GraphBrowserFrame.java

View Options

lib/browser/GraphBrowser/GraphView.java

View Options

lib/browser/GraphBrowser/NormalVertex.java

View Options

lib/browser/GraphBrowser/ParseError.java

View Options

lib/browser/GraphBrowser/Region.java

View Options

lib/browser/GraphBrowser/Spline.java

View Options

lib/browser/GraphBrowser/TreeBrowser.java

View Options

lib/browser/GraphBrowser/TreeNode.java

View Options

lib/browser/GraphBrowser/Vertex.java

View Options

lib/browser/awtUtilities/Border.java

View Options

lib/browser/awtUtilities/MessageDialog.java

View Options

lib/browser/awtUtilities/TextFrame.java

View Options

lib/browser/build

View Options

src/Pure/Admin/build_release.scala

View Options

src/Tools/GraphBrowser/GraphBrowser/AWTFontMetrics.java

View Options

src/Tools/GraphBrowser/GraphBrowser/AbstractFontMetrics.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Box.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Console.java

View Options

src/Tools/GraphBrowser/GraphBrowser/DefaultFontMetrics.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Directory.java

View Options

src/Tools/GraphBrowser/GraphBrowser/DummyVertex.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Graph.java

View Options

src/Tools/GraphBrowser/GraphBrowser/GraphBrowser.java

View Options

src/Tools/GraphBrowser/GraphBrowser/GraphBrowserFrame.java

View Options

src/Tools/GraphBrowser/GraphBrowser/GraphView.java

View Options

src/Tools/GraphBrowser/GraphBrowser/NormalVertex.java

View Options

src/Tools/GraphBrowser/GraphBrowser/ParseError.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Region.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Spline.java

View Options

src/Tools/GraphBrowser/GraphBrowser/TreeBrowser.java

View Options

src/Tools/GraphBrowser/GraphBrowser/TreeNode.java

View Options

src/Tools/GraphBrowser/GraphBrowser/Vertex.java

View Options

src/Tools/GraphBrowser/awtUtilities/Border.java

View Options

src/Tools/GraphBrowser/awtUtilities/MessageDialog.java

View Options

src/Tools/GraphBrowser/awtUtilities/TextFrame.java

View Options

src/Tools/GraphBrowser/etc/build.props

View Options

src/Tools/GraphBrowser/etc/settings

View Options

src/Tools/GraphBrowser/lib/Tools/browser

View Options

src/Tools/jEdit/lib/Tools/jedit

clarified component setup for old graph browser;1d366486a812Actions

Description

Details

Event Timeline

Changes (64)

rISABELLE1d366486a812

Admin/build

etc/components

lib/Tools/browser

lib/browser/GraphBrowser/AWTFontMetrics.java

lib/browser/GraphBrowser/AbstractFontMetrics.java

lib/browser/GraphBrowser/Box.java

lib/browser/GraphBrowser/Console.java

lib/browser/GraphBrowser/DefaultFontMetrics.java

lib/browser/GraphBrowser/Directory.java

lib/browser/GraphBrowser/DummyVertex.java

lib/browser/GraphBrowser/Graph.java

lib/browser/GraphBrowser/GraphBrowser.java

lib/browser/GraphBrowser/GraphBrowserFrame.java

lib/browser/GraphBrowser/GraphView.java

lib/browser/GraphBrowser/NormalVertex.java

lib/browser/GraphBrowser/ParseError.java

lib/browser/GraphBrowser/Region.java

lib/browser/GraphBrowser/Spline.java

lib/browser/GraphBrowser/TreeBrowser.java

lib/browser/GraphBrowser/TreeNode.java

lib/browser/GraphBrowser/Vertex.java

lib/browser/awtUtilities/Border.java

lib/browser/awtUtilities/MessageDialog.java

lib/browser/awtUtilities/TextFrame.java

lib/browser/build

src/Pure/Admin/build_release.scala

src/Tools/GraphBrowser/GraphBrowser/AWTFontMetrics.java

src/Tools/GraphBrowser/GraphBrowser/AbstractFontMetrics.java

src/Tools/GraphBrowser/GraphBrowser/Box.java

src/Tools/GraphBrowser/GraphBrowser/Console.java

src/Tools/GraphBrowser/GraphBrowser/DefaultFontMetrics.java

src/Tools/GraphBrowser/GraphBrowser/Directory.java

src/Tools/GraphBrowser/GraphBrowser/DummyVertex.java

src/Tools/GraphBrowser/GraphBrowser/Graph.java

src/Tools/GraphBrowser/GraphBrowser/GraphBrowser.java

src/Tools/GraphBrowser/GraphBrowser/GraphBrowserFrame.java

src/Tools/GraphBrowser/GraphBrowser/GraphView.java

src/Tools/GraphBrowser/GraphBrowser/NormalVertex.java

src/Tools/GraphBrowser/GraphBrowser/ParseError.java

src/Tools/GraphBrowser/GraphBrowser/Region.java

src/Tools/GraphBrowser/GraphBrowser/Spline.java

src/Tools/GraphBrowser/GraphBrowser/TreeBrowser.java

src/Tools/GraphBrowser/GraphBrowser/TreeNode.java

src/Tools/GraphBrowser/GraphBrowser/Vertex.java

src/Tools/GraphBrowser/awtUtilities/Border.java

src/Tools/GraphBrowser/awtUtilities/MessageDialog.java

src/Tools/GraphBrowser/awtUtilities/TextFrame.java

src/Tools/GraphBrowser/etc/build.props

src/Tools/GraphBrowser/etc/settings

src/Tools/GraphBrowser/lib/Tools/browser

src/Tools/jEdit/lib/Tools/jedit

clarified component setup for old graph browser;
1d366486a812
Actions