# HG changeset patch
# User wenzelm
# Date 1422213387 -3600
# Node ID 5b552b4f63a5eaa1fc894733f6e6db85f6d06258
# Parent  9f45b95d35435a1ab3a50fa4fa799e8c9a1f04b8
support for off-line graph output, without GUI thread;

diff -r 9f45b95d3543 -r 5b552b4f63a5 src/Tools/Graphview/graph_file.scala
--- a/src/Tools/Graphview/graph_file.scala	Sun Jan 25 18:31:35 2015 +0100
+++ b/src/Tools/Graphview/graph_file.scala	Sun Jan 25 20:16:27 2015 +0100
@@ -15,7 +15,7 @@
 
 object Graph_File
 {
-  def write(visualizer: Visualizer, file: JFile)
+  def write(file: JFile, visualizer: Visualizer)
   {
     val box = visualizer.bounding_box()
     val w = box.width.ceil.toInt
@@ -34,4 +34,15 @@
     else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
     else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
   }
+
+  def write(options: Options, file: JFile, graph: Graph_Display.Graph)
+  {
+    val model = new Model(graph.transitive_reduction_acyclic)
+
+    val the_options = options
+    val visualizer = new Visualizer(model) { def options = the_options }
+    visualizer.update_layout()
+
+    write(file, visualizer)
+  }
 }
diff -r 9f45b95d3543 -r 5b552b4f63a5 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Sun Jan 25 18:31:35 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sun Jan 25 20:16:27 2015 +0100
@@ -306,7 +306,7 @@
     action = Action("Save image") {
       chooser.showSaveDialog(this) match {
         case FileChooser.Result.Approve =>
-          try { Graph_File.write(visualizer, chooser.selectedFile) }
+          try { Graph_File.write(chooser.selectedFile, visualizer) }
           catch {
             case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
           }
diff -r 9f45b95d3543 -r 5b552b4f63a5 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 25 18:31:35 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 25 20:16:27 2015 +0100
@@ -153,14 +153,13 @@
 
   object Selection
   {
-    // owned by GUI thread
-    private var state: List[Graph_Display.Node] = Nil
+    private val state = Synchronized(List.empty[Graph_Display.Node])
 
-    def get(): List[Graph_Display.Node] = GUI_Thread.require { state }
+    def get(): List[Graph_Display.Node] = state.value
     def contains(node: Graph_Display.Node): Boolean = get().contains(node)
 
-    def add(node: Graph_Display.Node): Unit = GUI_Thread.require { state = node :: state }
-    def clear(): Unit = GUI_Thread.require { state = Nil }
+    def add(node: Graph_Display.Node): Unit = state.change(node :: _)
+    def clear(): Unit = state.change(_ => Nil)
   }
 
   sealed case class Node_Color(border: Color, background: Color, foreground: Color)