equal
deleted
inserted
replaced
36 } |
36 } |
37 |
37 |
38 private val continuous_checking = new JEdit_Options.continuous_checking.GUI |
38 private val continuous_checking = new JEdit_Options.continuous_checking.GUI |
39 continuous_checking.focusable = false |
39 continuous_checking.focusable = false |
40 |
40 |
41 private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true) |
41 private val logic = JEdit_Sessions.logic_selector(PIDE.options, standalone = true) |
42 |
42 |
43 private val controls = |
43 private val controls = |
44 Wrap_Panel(List(purge, continuous_checking, session_phase, logic)) |
44 Wrap_Panel(List(purge, continuous_checking, session_phase, logic)) |
45 |
45 |
46 add(controls.peer, BorderLayout.NORTH) |
46 add(controls.peer, BorderLayout.NORTH) |