src/Tools/jEdit/src/token_markup.scala
changeset 50663 f8d7d332fec0
parent 50210 747db833fbf7
child 53021 d0fa3f446b9d
equal deleted inserted replaced
50662:b1f4291eb916 50663:f8d7d332fec0
    44   def edit_control_style(text_area: TextArea, control: String)
    44   def edit_control_style(text_area: TextArea, control: String)
    45   {
    45   {
    46     Swing_Thread.assert()
    46     Swing_Thread.assert()
    47 
    47 
    48     val buffer = text_area.getBuffer
    48     val buffer = text_area.getBuffer
       
    49 
       
    50     text_area.getSelection.foreach(sel => {
       
    51       val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
       
    52       JEdit_Lib.try_get_text(buffer, before) match {
       
    53         case Some(s) if is_control_style(s) =>
       
    54           text_area.extendSelection(before.start, before.stop)
       
    55         case _ =>
       
    56       }
       
    57     })
    49 
    58 
    50     text_area.getSelection.toList match {
    59     text_area.getSelection.toList match {
    51       case Nil =>
    60       case Nil =>
    52         text_area.setSelectedText(control)
    61         text_area.setSelectedText(control)
    53       case sels =>
    62       case sels =>