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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     1
/*  Title:      Tools/Graphview/src/frame.scala
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     2
    Author:     Markus Kaiser, TU Muenchen
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     3
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     4
Graphview standalone frame.
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     5
*/
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     6
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     7
package isabelle.graphview
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     8
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     9
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    10
import isabelle._
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    11
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    12
import java.awt.Dimension
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    13
import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    14
import javax.swing.border.EmptyBorder
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    15
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    16
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    17
object Frame extends SwingApplication
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    18
{
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    19
  def startup(args : Array[String])
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    20
  {
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    21
    // FIXME avoid I/O etc. on Swing thread
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    22
    val graph: Model.Graph =
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    23
      try {
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    24
        Platform.init_laf()
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    25
        Isabelle_System.init()
49568
6e4510ccf1bb proper install_fonts;
wenzelm
parents: 49565
diff changeset
    26
        Isabelle_System.install_fonts()
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    27
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    28
        args.toList match {
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    29
          case List(arg) =>
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    30
            Model.decode_graph(YXML.parse_body(File.read(Path.explode(arg))))
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    31
          case _ => error("Bad arguments:\n" + cat_lines(args))
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    32
        }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    33
      }
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    34
      catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    35
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    36
    val top = new MainFrame {
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    37
      title = "Graphview"
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    38
      minimumSize = new Dimension(640, 480)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    39
      preferredSize = new Dimension(800, 600)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    40
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    41
      contents = new BorderPanel {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    42
        border = new EmptyBorder(5, 5, 5, 5)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    43
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    44
        add(new Main_Panel(graph), BorderPanel.Position.Center)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    45
      }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    46
    }
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    47
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    48
    top.pack()
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    49
    top.visible = true
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    50
  }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    51
}