src/Tools/Graphview/src/graphview.scala
author wenzelm
Tue, 29 Apr 2014 13:32:13 +0200
changeset 56782 433cf57550fa
parent 56671 06853449cf0a
permissions -rw-r--r--
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49575
7529c77ee92e more uniform graphview terminology;
wenzelm
parents: 49574
diff changeset
     1
/*  Title:      Tools/Graphview/src/graphview.scala
49557
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
49575
7529c77ee92e more uniform graphview terminology;
wenzelm
parents: 49574
diff changeset
     4
Graphview standalone application.
49557
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
49729
f53a8f73b40f more basic tooltips;
wenzelm
parents: 49575
diff changeset
    15
import javax.swing.ToolTipManager
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    16
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    17
49575
7529c77ee92e more uniform graphview terminology;
wenzelm
parents: 49574
diff changeset
    18
object Graphview extends SwingApplication
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    19
{
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    20
  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
    21
  {
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    22
    // 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
    23
    val graph: Model.Graph =
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    24
      try {
51617
4e49bba9772d tuned signature -- concentrate GUI tools;
wenzelm
parents: 51615
diff changeset
    25
        GUI.init_laf()
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    26
        Isabelle_System.init()
51614
22d1dd43f089 separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents: 50854
diff changeset
    27
        Isabelle_Font.install_fonts()
49729
f53a8f73b40f more basic tooltips;
wenzelm
parents: 49575
diff changeset
    28
        ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    29
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    30
        args.toList match {
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    31
          case List(arg) =>
49574
f27cb2662eda proper Symbol.decode -- especially relevant for Proof General;
wenzelm
parents: 49568
diff changeset
    32
            Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
50446
8dc05db0bf69 always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
wenzelm
parents: 49729
diff changeset
    33
              .transitive_reduction_acyclic
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    34
          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
    35
        }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    36
      }
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents: 56671
diff changeset
    37
      catch { case exn: Throwable => Output.error_message(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
    38
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    39
    val top = new MainFrame {
51615
072a7249e1ac separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents: 51614
diff changeset
    40
      iconImage = GUI.isabelle_image()
50854
2b15227b17e8 add icon for toplevel windows;
wenzelm
parents: 50446
diff changeset
    41
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    42
      title = "Graphview"
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    43
      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
    44
      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
    45
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    46
      contents = new BorderPanel {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    47
        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
    48
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    49
        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
    50
      }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    51
    }
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    52
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    53
    top.pack()
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49557
diff changeset
    54
    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
    55
  }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    56
}