| author | wenzelm | 
| Wed, 11 Nov 2020 20:58:36 +0100 | |
| changeset 72573 | a085a1a89388 | 
| parent 72572 | e7e93c0f6d96 | 
| child 72574 | d892f6d66402 | 
--- a/src/Tools/Graphview/graph_file.scala Wed Nov 11 20:55:25 2020 +0100 +++ b/src/Tools/Graphview/graph_file.scala Wed Nov 11 20:58:36 2020 +0100 @@ -44,4 +44,11 @@ write(file, graphview) } + + def make_pdf(options: Options, graph: Graph_Display.Graph): Bytes = + Isabelle_System.with_tmp_file("graph", ext = "pdf")(graph_file => + { + write(options, graph_file.file, graph) + Bytes.read(graph_file) + }) }