src/Tools/Graphview/src/frame.scala
author wenzelm
Wed, 26 Sep 2012 14:13:07 +0200
changeset 49568 6e4510ccf1bb
parent 49565 ea4308b7ef0f
child 49574 f27cb2662eda
permissions -rw-r--r--
proper install_fonts;

/*  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(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
  }
}