--- a/src/Tools/Graphview/src/frame.scala Tue Sep 25 18:24:49 2012 +0200
+++ b/src/Tools/Graphview/src/frame.scala Tue Sep 25 20:28:47 2012 +0200
@@ -14,39 +14,25 @@
import javax.swing.border.EmptyBorder
-object Graphview_Frame extends SwingApplication
+object Frame extends SwingApplication
{
def startup(args : Array[String])
{
- try {
- Platform.init_laf()
- Isabelle_System.init()
- }
- catch { case exn: Throwable => println(Exn.message(exn)); System.exit(1) }
+ // FIXME avoid I/O etc. on Swing thread
+ val graph: Model.Graph =
+ try {
+ Platform.init_laf()
+ Isabelle_System.init()
- val opt_xml: Option[XML.Tree] =
- try {
- Some(YXML.parse_body(
- Symbol.decode(io.Source.fromFile(args(0)).mkString)).head)
- } catch {
- case _ : ArrayIndexOutOfBoundsException => None
- case _ : java.io.FileNotFoundException => None
+ args.toList match {
+ case List(arg) =>
+ Model.decode_graph(YXML.parse_body(File.read(Path.explode(arg))))
+ case _ => error("Bad arguments:\n" + cat_lines(args))
+ }
}
-
- //Textfiles will still be valid and result in an empty frame
- //since they are valid to YXML.
- opt_xml match {
- case None =>
- println("No valid YXML-File given.\n" +
- "Usage: java -jar graphview.jar <yxmlfile>")
- System.exit(1)
- case Some(xml) =>
- val top = frame(xml)
- top.pack()
- top.visible = true
- }
+ catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
- def frame(xml: XML.Tree): Window = new MainFrame {
+ val top = new MainFrame {
title = "Graphview"
minimumSize = new Dimension(640, 480)
preferredSize = new Dimension(800, 600)
@@ -54,8 +40,11 @@
contents = new BorderPanel {
border = new EmptyBorder(5, 5, 5, 5)
- add(new Main_Panel(xml), BorderPanel.Position.Center)
+ add(new Main_Panel(graph), BorderPanel.Position.Center)
}
}
+
+ top.pack()
+ top.visible = true
}
}
\ No newline at end of file