12 import java.awt.Dimension |
12 import java.awt.Dimension |
13 import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication} |
13 import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication} |
14 import javax.swing.border.EmptyBorder |
14 import javax.swing.border.EmptyBorder |
15 |
15 |
16 |
16 |
17 object Graphview_Frame extends SwingApplication |
17 object Frame extends SwingApplication |
18 { |
18 { |
19 def startup(args : Array[String]) |
19 def startup(args : Array[String]) |
20 { |
20 { |
21 try { |
21 // FIXME avoid I/O etc. on Swing thread |
22 Platform.init_laf() |
22 val graph: Model.Graph = |
23 Isabelle_System.init() |
23 try { |
24 } |
24 Platform.init_laf() |
25 catch { case exn: Throwable => println(Exn.message(exn)); System.exit(1) } |
25 Isabelle_System.init() |
26 |
26 |
27 val opt_xml: Option[XML.Tree] = |
27 args.toList match { |
28 try { |
28 case List(arg) => |
29 Some(YXML.parse_body( |
29 Model.decode_graph(YXML.parse_body(File.read(Path.explode(arg)))) |
30 Symbol.decode(io.Source.fromFile(args(0)).mkString)).head) |
30 case _ => error("Bad arguments:\n" + cat_lines(args)) |
31 } catch { |
31 } |
32 case _ : ArrayIndexOutOfBoundsException => None |
|
33 case _ : java.io.FileNotFoundException => None |
|
34 } |
32 } |
35 |
33 catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) } |
36 //Textfiles will still be valid and result in an empty frame |
|
37 //since they are valid to YXML. |
|
38 opt_xml match { |
|
39 case None => |
|
40 println("No valid YXML-File given.\n" + |
|
41 "Usage: java -jar graphview.jar <yxmlfile>") |
|
42 System.exit(1) |
|
43 case Some(xml) => |
|
44 val top = frame(xml) |
|
45 top.pack() |
|
46 top.visible = true |
|
47 } |
|
48 |
34 |
49 def frame(xml: XML.Tree): Window = new MainFrame { |
35 val top = new MainFrame { |
50 title = "Graphview" |
36 title = "Graphview" |
51 minimumSize = new Dimension(640, 480) |
37 minimumSize = new Dimension(640, 480) |
52 preferredSize = new Dimension(800, 600) |
38 preferredSize = new Dimension(800, 600) |
53 |
39 |
54 contents = new BorderPanel { |
40 contents = new BorderPanel { |
55 border = new EmptyBorder(5, 5, 5, 5) |
41 border = new EmptyBorder(5, 5, 5, 5) |
56 |
42 |
57 add(new Main_Panel(xml), BorderPanel.Position.Center) |
43 add(new Main_Panel(graph), BorderPanel.Position.Center) |
58 } |
44 } |
59 } |
45 } |
|
46 |
|
47 top.pack() |
|
48 top.visible = true |
60 } |
49 } |
61 } |
50 } |