src/Tools/Graphview/graph_file.scala
changeset 75393 87ebf5a50283
parent 73340 0ffcad1f6130
child 75394 42267c650205
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
    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 }