Commit 72a9633
committed
Hide REPL pane unless "persistent" is checked
This fixes a bug where resizing the tab's JSplitPane divider to make the
output pane taller instead results in the REPL "emerging" while in
non-persistent mode. This was happening because the screenAndPromptSplit
prioritized keeping its JSplitPane divider at the same integer value,
resulting in the output pane height staying constant and the REPL pane's
height increasing. By setting the REPL pane to invisible, the resizing
logic now instead gives the extra space to the output pane, as desired.1 parent 7780e45 commit 72a9633
1 file changed
+4
-0
lines changedLines changed: 4 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
31 | 31 | | |
32 | 32 | | |
33 | 33 | | |
| 34 | + | |
34 | 35 | | |
35 | 36 | | |
36 | 37 | | |
| |||
251 | 252 | | |
252 | 253 | | |
253 | 254 | | |
| 255 | + | |
| 256 | + | |
254 | 257 | | |
255 | 258 | | |
256 | 259 | | |
| |||
315 | 318 | | |
316 | 319 | | |
317 | 320 | | |
| 321 | + | |
318 | 322 | | |
319 | 323 | | |
320 | 324 | | |
| |||
0 commit comments