more operations;
authorwenzelm
Wed, 11 Nov 2020 20:58:36 +0100
changeset 72573 a085a1a89388
parent 72572 e7e93c0f6d96
child 72574 d892f6d66402
more operations;
src/Tools/Graphview/graph_file.scala
--- 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)
+    })
 }