src/Tools/jEdit/src/theories_dockable.scala
changeset 52816 c608e0ade554
parent 52815 eaad5fe7bb1b
child 52817 408fb2e563df
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 19:59:14 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 21:13:05 2013 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  import scala.swing.event.{ButtonClicked, MouseClicked}
     1.5  
     1.6  import java.lang.System
     1.7 -import java.awt.{BorderLayout, Graphics2D, Insets}
     1.8 +import java.awt.{BorderLayout, Graphics2D, Insets, Point, Dimension}
     1.9  import javax.swing.{JList, BorderFactory}
    1.10  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    1.11  
    1.12 @@ -29,9 +29,29 @@
    1.13    private val status = new ListView(Nil: List[Document.Node.Name]) {
    1.14      listenTo(mouse.clicks)
    1.15      reactions += {
    1.16 -      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    1.17 +      case MouseClicked(_, point, _, clicks, _) =>
    1.18          val index = peer.locationToIndex(point)
    1.19 -        if (index >= 0) Hyperlink(listData(index).node).follow(view)
    1.20 +        if (index >= 0 && Node_Renderer_Component != null) {
    1.21 +          Node_Renderer_Component.checkbox_geometry match {
    1.22 +            case Some((loc, size)) =>
    1.23 +              val loc0 = peer.indexToLocation(index)
    1.24 +              val in_checkbox =
    1.25 +                loc0.x + loc.x <= point.x && point.x < loc0.x + size.width &&
    1.26 +                loc0.y + loc.y <= point.y && point.y < loc0.y + size.height
    1.27 +
    1.28 +              if (clicks == 1 && in_checkbox) {
    1.29 +                for {
    1.30 +                  buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
    1.31 +                  model <- PIDE.document_model(buffer)
    1.32 +                } model.node_required = !model.node_required
    1.33 +              }
    1.34 +
    1.35 +              if (clicks == 2 && !in_checkbox)
    1.36 +                Hyperlink(listData(index).node).follow(view)
    1.37 +
    1.38 +            case None =>
    1.39 +          }
    1.40 +        }
    1.41      }
    1.42    }
    1.43    status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
    1.44 @@ -90,7 +110,16 @@
    1.45      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    1.46  
    1.47      var node_name = Document.Node.Name.empty
    1.48 -    val required = new CheckBox
    1.49 +
    1.50 +    var checkbox_geometry: Option[(Point, Dimension)] = None
    1.51 +    val checkbox = new CheckBox {
    1.52 +      override def paintComponent(gfx: Graphics2D)
    1.53 +      {
    1.54 +        super.paintComponent(gfx)
    1.55 +        if (location != null && size != null)
    1.56 +          checkbox_geometry = Some((location, size))
    1.57 +      }
    1.58 +    }
    1.59  
    1.60      val label = new Label {
    1.61        opaque = false
    1.62 @@ -127,7 +156,7 @@
    1.63        }
    1.64      }
    1.65  
    1.66 -    layout(required) = BorderPanel.Position.West
    1.67 +    layout(checkbox) = BorderPanel.Position.West
    1.68      layout(label) = BorderPanel.Position.Center
    1.69    }
    1.70  
    1.71 @@ -138,7 +167,7 @@
    1.72      {
    1.73        val component = Node_Renderer_Component
    1.74        component.node_name = name
    1.75 -      component.required.selected = nodes_required.contains(name)
    1.76 +      component.checkbox.selected = nodes_required.contains(name)
    1.77        component.label.text = name.theory
    1.78        component
    1.79      }