equal
deleted
inserted
replaced
23 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} |
23 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} |
24 |
24 |
25 |
25 |
26 object JEdit_Lib |
26 object JEdit_Lib |
27 { |
27 { |
|
28 /* jEdit directories */ |
|
29 |
|
30 def directories: List[JFile] = |
|
31 (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_)) |
|
32 |
|
33 |
28 /* location within multi-screen environment */ |
34 /* location within multi-screen environment */ |
29 |
35 |
30 final case class Screen_Location(point: Point, bounds: Rectangle) |
36 final case class Screen_Location(point: Point, bounds: Rectangle) |
31 { |
37 { |
32 def relative(parent: Component, size: Dimension): Point = |
38 def relative(parent: Component, size: Dimension): Point = |