1.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 07 18:44:28 2010 +0200
     1.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 07 21:06:58 2010 +0200
     1.3 @@ -203,6 +203,7 @@
     1.4  view.fontsize=18
     1.5  view.fracFontMetrics=false
     1.6  view.gutter.fontsize=12
     1.7 +view.gutter.selectionAreaWidth=18
     1.8  view.height=787
     1.9  view.middleMousePaste=true
    1.10  view.showToolbar=false

     2.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 18:44:28 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 21:06:58 2010 +0200
     2.3 @@ -17,8 +17,9 @@
     2.4  import javax.swing.{JPanel, ToolTipManager}
     2.5  import javax.swing.event.{CaretListener, CaretEvent}
     2.6  
     2.7 -import org.gjt.sp.jedit.{GUIUtilities, OperatingSystem}
     2.8 +import org.gjt.sp.jedit.{jEdit, GUIUtilities, OperatingSystem}
     2.9  import org.gjt.sp.jedit.gui.RolloverButton
    2.10 +import org.gjt.sp.jedit.options.GutterOptionPane
    2.11  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    2.12  import org.gjt.sp.jedit.syntax.SyntaxStyle
    2.13  
    2.14 @@ -31,8 +32,8 @@
    2.15    val unfinished_color = new Color(255, 228, 225)
    2.16  
    2.17    val regular_color = new Color(192, 192, 192)
    2.18 -  val warning_color = new Color(255, 165, 0)
    2.19 -  val error_color = new Color(255, 106, 106)
    2.20 +  val warning_color = new Color(255, 168, 0)
    2.21 +  val error_color = new Color(255, 80, 80)
    2.22    val bad_color = new Color(255, 204, 153, 100)
    2.23  
    2.24    val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
    2.25 @@ -364,17 +365,21 @@
    2.26        first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.27        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.28      {
    2.29 -      Isabelle.swing_buffer_lock(model.buffer) {
    2.30 -        val snapshot = model.snapshot()
    2.31 -        val saved_color = gfx.getColor
    2.32 -        try {
    2.33 +      val gutter = text_area.getGutter
    2.34 +      val width = GutterOptionPane.getSelectionAreaWidth
    2.35 +      val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
    2.36 +      val FOLD_MARKER_SIZE = 12
    2.37 +
    2.38 +      if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    2.39 +        Isabelle.swing_buffer_lock(model.buffer) {
    2.40 +          val snapshot = model.snapshot()
    2.41            for (i <- 0 until physical_lines.length) {
    2.42              if (physical_lines(i) != -1) {
    2.43                val line_range = proper_line_range(start(i), end(i))
    2.44 -              val cmds = snapshot.node.command_range(snapshot.revert(line_range)).toStream
    2.45  
    2.46                // gutter icons
    2.47 -              val states = cmds.map(p => snapshot.state(p._1))
    2.48 +              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    2.49 +              val states = cmds.map(p => snapshot.state(p._1)).toStream
    2.50                val opt_icon =
    2.51                  if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
    2.52                    Some(Document_View.error_icon)
    2.53 @@ -383,16 +388,14 @@
    2.54                  else None
    2.55                opt_icon match {
    2.56                  case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
    2.57 -                  val FOLD_MARKER_SIZE = 12
    2.58 -                  val x0 = ((FOLD_MARKER_SIZE - icon.getIconWidth) / 2) max 0
    2.59 +                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
    2.60                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
    2.61 -                  icon.paintIcon(text_area.getPainter, gfx, x0, y0)
    2.62 +                  icon.paintIcon(gutter, gfx, x0, y0)
    2.63                  case _ =>
    2.64                }
    2.65              }
    2.66            }
    2.67          }
    2.68 -        finally { gfx.setColor(saved_color) }
    2.69        }
    2.70      }
    2.71    }