# HG changeset patch
# User wenzelm
# Date 1442252810 -7200
# Node ID 9791f631c20df648ac0079a42eb4785d7e4da625
# Parent  1d9c121cbe4de5c87b8d12598fb8c1349c744ceb
avoid hardwired colors;
more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);

diff -r 1d9c121cbe4d -r 9791f631c20d src/Tools/Graphview/graph_file.scala
--- a/src/Tools/Graphview/graph_file.scala	Mon Sep 14 18:03:43 2015 +0200
+++ b/src/Tools/Graphview/graph_file.scala	Mon Sep 14 19:46:50 2015 +0200
@@ -23,7 +23,7 @@
 
     def paint(gfx: Graphics2D)
     {
-      gfx.setColor(Color.WHITE)
+      gfx.setColor(graphview.background_color)
       gfx.fillRect(0, 0, w, h)
       gfx.translate(- box.x, - box.y)
       graphview.paint(gfx)
diff -r 1d9c121cbe4d -r 9791f631c20d src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Mon Sep 14 18:03:43 2015 +0200
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Sep 14 19:46:50 2015 +0200
@@ -331,12 +331,22 @@
     tooltip = "Regenerate graph layout according to built-in algorithm"
   }
 
+  private val editor_style = new CheckBox() {
+    selected = graphview.editor_style
+    action = Action("Editor style") {
+      graphview.editor_style = selected
+      graphview.update_layout()
+      refresh()
+    }
+    tooltip = "Use editor font and colors for painting"
+  }
+
   private val colorations = new Button { action = Action("Colorations") { color_dialog.open } }
   private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(show_content, show_arrow_heads, show_dummies,
-      save_image, zoom, fit_window, update_layout) // FIXME colorations, filters
+      save_image, zoom, fit_window, update_layout, editor_style) // FIXME colorations, filters
 
 
 
diff -r 1d9c121cbe4d -r 9791f631c20d src/Tools/Graphview/graphview.scala
--- a/src/Tools/Graphview/graphview.scala	Mon Sep 14 18:03:43 2015 +0200
+++ b/src/Tools/Graphview/graphview.scala	Mon Sep 14 19:46:50 2015 +0200
@@ -94,8 +94,8 @@
 
   def foreground_color: Color = Color.BLACK
   def background_color: Color = Color.WHITE
-  def selection_color: Color = Color.GREEN
-  def highlight_color: Color = Color.YELLOW
+  def selection_color: Color = new Color(204, 204, 255)
+  def highlight_color: Color = new Color(255, 255, 224)
   def error_color: Color = Color.RED
   def dummy_color: Color = Color.GRAY
 
@@ -116,6 +116,7 @@
   var show_content = false
   var show_arrow_heads = false
   var show_dummies = false
+  var editor_style = false
 
   object Colors
   {
diff -r 1d9c121cbe4d -r 9791f631c20d src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Sep 14 18:03:43 2015 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Sep 14 19:46:50 2015 +0200
@@ -76,14 +76,31 @@
           }
 
           override def make_font(): Font =
-            GUI.imitate_font(Font_Info.main().font,
-              options.string("graphview_font_family"),
-              options.real("graphview_font_scale"))
+            if (editor_style) Font_Info.main(PIDE.options.real("graphview_font_scale")).font
+            else
+              GUI.imitate_font(Font_Info.main().font,
+                options.string("graphview_font_family"),
+                options.real("graphview_font_scale"))
+
+          override def foreground_color =
+            if (editor_style) view.getTextArea.getPainter.getForeground
+            else super.foreground_color
 
-          override def foreground_color = view.getTextArea.getPainter.getForeground
-          override def selection_color = view.getTextArea.getPainter.getSelectionColor
-          override def highlight_color = view.getTextArea.getPainter.getLineHighlightColor
+          override def background_color =
+            if (editor_style) view.getTextArea.getPainter.getBackground
+            else super.background_color
+
+          override def selection_color =
+            if (editor_style) view.getTextArea.getPainter.getSelectionColor
+            else super.selection_color
+
+          override def highlight_color =
+            if (editor_style) view.getTextArea.getPainter.getLineHighlightColor
+            else super.highlight_color
+
           override def error_color = PIDE.options.color_value("error_color")
+
+          editor_style = true
         }
         new isabelle.graphview.Main_Panel(graphview)
       case Exn.Exn(exn) => new TextArea(Exn.message(exn))