# HG changeset patch
# User wenzelm
# Date 1348664505 -7200
# Node ID 7529c77ee92e3a8daeee974c433e29c750a23409
# Parent  f27cb2662edaf099bb828f91cfc363eaf1482e02
more uniform graphview terminology;

diff -r f27cb2662eda -r 7529c77ee92e src/Tools/Graphview/lib/Tools/graphview
--- a/src/Tools/Graphview/lib/Tools/graphview	Wed Sep 26 14:56:59 2012 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview	Wed Sep 26 15:01:45 2012 +0200
@@ -9,8 +9,8 @@
 
 declare -a SOURCES=(
   "src/floating_dialog.scala"
-  "src/frame.scala"
   "src/graph_panel.scala"
+  "src/graphview.scala"
   "src/layout_pendulum.scala"
   "src/main_panel.scala"
   "src/model.scala"
@@ -166,7 +166,7 @@
     cp -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPH_FILE"
   fi
 
-  "$ISABELLE_TOOL" java $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Frame "$PRIVATE_FILE"
+  "$ISABELLE_TOOL" java $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Graphview "$PRIVATE_FILE"
   RC="$?"
 
   rm -f "$PRIVATE_FILE"
diff -r f27cb2662eda -r 7529c77ee92e src/Tools/Graphview/src/frame.scala
--- a/src/Tools/Graphview/src/frame.scala	Wed Sep 26 14:56:59 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-/*  Title:      Tools/Graphview/src/frame.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Graphview standalone frame.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.Dimension
-import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
-import javax.swing.border.EmptyBorder
-
-
-object Frame extends SwingApplication
-{
-  def startup(args : Array[String])
-  {
-    // FIXME avoid I/O etc. on Swing thread
-    val graph: Model.Graph =
-      try {
-        Platform.init_laf()
-        Isabelle_System.init()
-        Isabelle_System.install_fonts()
-
-        args.toList match {
-          case List(arg) =>
-            Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
-          case _ => error("Bad arguments:\n" + cat_lines(args))
-        }
-      }
-      catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
-
-    val top = new MainFrame {
-      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
diff -r f27cb2662eda -r 7529c77ee92e src/Tools/Graphview/src/graphview.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/graphview.scala	Wed Sep 26 15:01:45 2012 +0200
@@ -0,0 +1,51 @@
+/*  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
+
+
+object Graphview extends SwingApplication
+{
+  def startup(args : Array[String])
+  {
+    // FIXME avoid I/O etc. on Swing thread
+    val graph: Model.Graph =
+      try {
+        Platform.init_laf()
+        Isabelle_System.init()
+        Isabelle_System.install_fonts()
+
+        args.toList match {
+          case List(arg) =>
+            Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
+          case _ => error("Bad arguments:\n" + cat_lines(args))
+        }
+      }
+      catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
+
+    val top = new MainFrame {
+      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