Commit e924176
committed
Hide notes buffer whe no notes available.
This revisits #148
and improves the user experience when Idris does not report any errors.
Previously in such case the user is left with empty buffer in some of the windows.
After this change if there is nothing to display the window
the notes either display previous buffer or it is closed completely if notes
buffer was the only buffer displayed in it.1 parent b45ddda commit e924176
1 file changed
+10
-9
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
38 | 38 | | |
39 | 39 | | |
40 | 40 | | |
41 | | - | |
42 | | - | |
43 | | - | |
44 | | - | |
45 | | - | |
46 | | - | |
47 | | - | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
48 | 49 | | |
49 | 50 | | |
50 | 51 | | |
51 | | - | |
52 | | - | |
| 52 | + | |
| 53 | + | |
53 | 54 | | |
54 | 55 | | |
55 | 56 | | |
| |||
0 commit comments