author | wenzelm |
Tue, 29 Apr 2014 13:32:13 +0200 | |
changeset 56782 | 433cf57550fa |
parent 56671 | 06853449cf0a |
permissions | -rw-r--r-- |
49575 | 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 | 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 | 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 | 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 | 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 | 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 | 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 |
} |