11 |
11 |
12 import java.io.{File => JFile} |
12 import java.io.{File => JFile} |
13 import java.awt.{Color, Graphics2D} |
13 import java.awt.{Color, Graphics2D} |
14 |
14 |
15 |
15 |
16 object Graph_File |
16 object Graph_File { |
17 { |
17 def write(file: JFile, graphview: Graphview): Unit = { |
18 def write(file: JFile, graphview: Graphview): Unit = |
|
19 { |
|
20 val box = graphview.bounding_box() |
18 val box = graphview.bounding_box() |
21 val w = box.width.ceil.toInt |
19 val w = box.width.ceil.toInt |
22 val h = box.height.ceil.toInt |
20 val h = box.height.ceil.toInt |
23 |
21 |
24 def paint(gfx: Graphics2D): Unit = |
22 def paint(gfx: Graphics2D): Unit = { |
25 { |
|
26 gfx.setColor(graphview.background_color) |
23 gfx.setColor(graphview.background_color) |
27 gfx.fillRect(0, 0, w, h) |
24 gfx.fillRect(0, 0, w, h) |
28 gfx.translate(- box.x, - box.y) |
25 gfx.translate(- box.x, - box.y) |
29 graphview.paint(gfx) |
26 graphview.paint(gfx) |
30 } |
27 } |
33 if (name.endsWith(".png")) Graphics_File.write_png(file, paint, w, h) |
30 if (name.endsWith(".png")) Graphics_File.write_png(file, paint, w, h) |
34 else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint, w, h) |
31 else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint, w, h) |
35 else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") |
32 else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") |
36 } |
33 } |
37 |
34 |
38 def write(options: Options, file: JFile, graph: Graph_Display.Graph): Unit = |
35 def write(options: Options, file: JFile, graph: Graph_Display.Graph): Unit = { |
39 { |
|
40 val the_options = options |
36 val the_options = options |
41 val graphview = |
37 val graphview = |
42 new Graphview(graph.transitive_reduction_acyclic) { def options = the_options } |
38 new Graphview(graph.transitive_reduction_acyclic) { def options = the_options } |
43 graphview.update_layout() |
39 graphview.update_layout() |
44 |
40 |
45 write(file, graphview) |
41 write(file, graphview) |
46 } |
42 } |
47 |
43 |
48 def make_pdf(options: Options, graph: Graph_Display.Graph): Bytes = |
44 def make_pdf(options: Options, graph: Graph_Display.Graph): Bytes = |
49 Isabelle_System.with_tmp_file("graph", ext = "pdf")(graph_file => |
45 Isabelle_System.with_tmp_file("graph", ext = "pdf")(graph_file => { |
50 { |
|
51 write(options, graph_file.file, graph) |
46 write(options, graph_file.file, graph) |
52 Bytes.read(graph_file) |
47 Bytes.read(graph_file) |
53 }) |
48 }) |
54 } |
49 } |