author | wenzelm |
Mon, 28 Jun 2021 12:29:00 +0200 | |
changeset 73888 | 9c2dd041477b |
parent 73340 | 0ffcad1f6130 |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
59441 | 1 |
/* Title: Tools/Graphview/graph_file.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
File system operations for graph output. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.graphview |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import java.io.{File => JFile} |
|
13 |
import java.awt.{Color, Graphics2D} |
|
14 |
||
15 |
||
16 |
object Graph_File |
|
17 |
{ |
|
73340 | 18 |
def write(file: JFile, graphview: Graphview): Unit = |
59441 | 19 |
{ |
59459 | 20 |
val box = graphview.bounding_box() |
59441 | 21 |
val w = box.width.ceil.toInt |
22 |
val h = box.height.ceil.toInt |
|
23 |
||
73340 | 24 |
def paint(gfx: Graphics2D): Unit = |
59441 | 25 |
{ |
61176 | 26 |
gfx.setColor(graphview.background_color) |
59441 | 27 |
gfx.fillRect(0, 0, w, h) |
28 |
gfx.translate(- box.x, - box.y) |
|
59460 | 29 |
graphview.paint(gfx) |
59441 | 30 |
} |
31 |
||
32 |
val name = file.getName |
|
71601 | 33 |
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) |
|
59441 | 35 |
else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") |
36 |
} |
|
59443
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59441
diff
changeset
|
37 |
|
73340 | 38 |
def write(options: Options, file: JFile, graph: Graph_Display.Graph): Unit = |
59443
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59441
diff
changeset
|
39 |
{ |
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59441
diff
changeset
|
40 |
val the_options = options |
59462 | 41 |
val graphview = |
42 |
new Graphview(graph.transitive_reduction_acyclic) { def options = the_options } |
|
59459 | 43 |
graphview.update_layout() |
59443
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59441
diff
changeset
|
44 |
|
59459 | 45 |
write(file, graphview) |
59443
5b552b4f63a5
support for off-line graph output, without GUI thread;
wenzelm
parents:
59441
diff
changeset
|
46 |
} |
72573 | 47 |
|
48 |
def make_pdf(options: Options, graph: Graph_Display.Graph): Bytes = |
|
49 |
Isabelle_System.with_tmp_file("graph", ext = "pdf")(graph_file => |
|
50 |
{ |
|
51 |
write(options, graph_file.file, graph) |
|
52 |
Bytes.read(graph_file) |
|
53 |
}) |
|
59441 | 54 |
} |