src/Tools/Graphview/graph_file.scala
author wenzelm
Sun, 25 Jan 2015 17:48:14 +0100
changeset 59441 ab2c3597f1d3
child 59443 5b552b4f63a5
permissions -rw-r--r--
separate module Graph_File;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59441
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/Graphview/graph_file.scala
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     3
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     4
File system operations for graph output.
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     5
*/
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     6
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     7
package isabelle.graphview
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     8
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
     9
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    10
import isabelle._
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    11
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    12
import java.io.{File => JFile}
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    13
import java.awt.{Color, Graphics2D}
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    14
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    15
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    16
object Graph_File
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    17
{
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    18
  def write(visualizer: Visualizer, file: JFile)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    19
  {
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    20
    val box = visualizer.bounding_box()
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    21
    val w = box.width.ceil.toInt
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    22
    val h = box.height.ceil.toInt
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    23
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    24
    def paint(gfx: Graphics2D)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    25
    {
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    26
      gfx.setColor(Color.WHITE)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    27
      gfx.fillRect(0, 0, w, h)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    28
      gfx.translate(- box.x, - box.y)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    29
      visualizer.paint_all_visible(gfx)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    30
    }
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    31
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    32
    val name = file.getName
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    33
    if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    34
    else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    35
    else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    36
  }
ab2c3597f1d3 separate module Graph_File;
wenzelm
parents:
diff changeset
    37
}