# HG changeset patch
# User wenzelm
# Date 1355516761 -3600
# Node ID 48cb76b785da085b2e3dac74672d8b3584a175be
# Parent  08ce81aeeacc834f75815827a35c7d96b85f1818
init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;

diff -r 08ce81aeeacc -r 48cb76b785da src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 14 20:05:08 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 14 21:26:01 2012 +0100
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Font, FontMetrics, Toolkit}
+import java.awt.{Color, Font, FontMetrics, Toolkit}
 import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
 import javax.swing.{KeyStroke, JComponent}
 
@@ -52,7 +52,9 @@
   }
 }
 
-class Pretty_Text_Area(view: View) extends JEditEmbeddedTextArea
+class Pretty_Text_Area(
+  view: View,
+  background: Option[Color] = None) extends JEditEmbeddedTextArea
 {
   text_area =>
 
@@ -81,8 +83,23 @@
     getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
 
     if (getWidth > 0) {
+      getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
+      getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
+      background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+      getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
+      getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
+      getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
+      getGutter.setBorder(0,
+        jEdit.getColorProperty("view.gutter.focusBorderColor"),
+        jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
+        getPainter.getBackground)
+      getGutter.setFoldPainter(getFoldPainter)
+
+      getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
+
       val font_metrics = getPainter.getFontMetrics(font)
-      val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
+      val margin =
+        ((getWidth - getGutter.getWidth) / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
 
       val base_snapshot = current_base_snapshot
       val base_results = current_base_results
diff -r 08ce81aeeacc -r 48cb76b785da src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Dec 14 20:05:08 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Dec 14 21:26:01 2012 +0100
@@ -68,8 +68,7 @@
 
   /* pretty text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
+  val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color))
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
   pretty_text_area.update(rendering.snapshot, results, body)