# HG changeset patch
# User wenzelm
# Date 1400668467 -7200
# Node ID 6e10bf974693fc5fad5c9cf79b4a1d882a31b82e
# Parent  b24e2b83917f4d5a61716355fad3138fce4d911c
obsolete;

diff -r b24e2b83917f -r 6e10bf974693 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed May 21 12:14:03 2014 +0200
+++ b/src/Pure/build-jars	Wed May 21 12:34:27 2014 +0200
@@ -98,7 +98,6 @@
   term.scala
   term_xml.scala
   "../Tools/Graphview/src/graph_panel.scala"
-  "../Tools/Graphview/src/graphview.scala"
   "../Tools/Graphview/src/layout_pendulum.scala"
   "../Tools/Graphview/src/main_panel.scala"
   "../Tools/Graphview/src/model.scala"
diff -r b24e2b83917f -r 6e10bf974693 src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Wed May 21 12:14:03 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-/*  Title:      Tools/Graphview/src/graphview.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Graphview standalone application.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.Dimension
-import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
-import javax.swing.border.EmptyBorder
-import javax.swing.ToolTipManager
-
-
-object Graphview extends SwingApplication
-{
-  def startup(args : Array[String])
-  {
-    // FIXME avoid I/O etc. on Swing thread
-    val graph: Model.Graph =
-      try {
-        GUI.init_laf()
-        Isabelle_System.init()
-        Isabelle_Font.install_fonts()
-        ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
-
-        args.toList match {
-          case List(arg) =>
-            Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
-              .transitive_reduction_acyclic
-          case _ => error("Bad arguments:\n" + cat_lines(args))
-        }
-      }
-      catch { case exn: Throwable => Output.error_message(Exn.message(exn)); sys.exit(1) }
-
-    val top = new MainFrame {
-      iconImage = GUI.isabelle_image()
-
-      title = "Graphview"
-      minimumSize = new Dimension(640, 480)
-      preferredSize = new Dimension(800, 600)
-
-      contents = new BorderPanel {
-        border = new EmptyBorder(5, 5, 5, 5)
-
-        add(new Main_Panel(graph), BorderPanel.Position.Center)
-      }
-    }
-
-    top.pack()
-    top.visible = true
-  }
-}
\ No newline at end of file