src/Tools/jEdit/src/session_dockable.scala
changeset 50250 267bd685a69f
parent 50209 907373a080b9
equal deleted inserted replaced
50249:3f0920f8a24e 50250:267bd685a69f
    31       case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    31       case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    32         val index = peer.locationToIndex(point)
    32         val index = peer.locationToIndex(point)
    33         if (index >= 0) jEdit.openFile(view, listData(index).node)
    33         if (index >= 0) jEdit.openFile(view, listData(index).node)
    34     }
    34     }
    35   }
    35   }
    36   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    36   status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
       
    37   status.peer.setVisibleRowCount(0)
    37   status.selection.intervalMode = ListView.IntervalMode.Single
    38   status.selection.intervalMode = ListView.IntervalMode.Single
    38 
    39 
    39   set_content(new ScrollPane(status))
    40   set_content(new ScrollPane(status))
    40 
    41 
    41 
    42