1256 |
;; set top scroll margin |
;; set top scroll margin |
1257 |
(or (string= top "") |
(or (string= top "") |
1258 |
(if (string= "%" (substring top -1)) |
(if (string= "%" (substring top -1)) |
1259 |
(setq edt-top-scroll-margin (string-to-int top)) |
(setq edt-top-scroll-margin (string-to-number top)) |
1260 |
(setq edt-top-scroll-margin |
(setq edt-top-scroll-margin |
1261 |
(/ (1- (+ (* (string-to-int top) 100) (window-height))) |
(/ (1- (+ (* (string-to-number top) 100) (window-height))) |
1262 |
(window-height))))) |
(window-height))))) |
1263 |
;; set bottom scroll margin |
;; set bottom scroll margin |
1264 |
(or (string= bottom "") |
(or (string= bottom "") |
1265 |
(if (string= "%" (substring bottom -1)) |
(if (string= "%" (substring bottom -1)) |
1266 |
(setq edt-bottom-scroll-margin (string-to-int bottom)) |
(setq edt-bottom-scroll-margin (string-to-number bottom)) |
1267 |
(setq edt-bottom-scroll-margin |
(setq edt-bottom-scroll-margin |
1268 |
(/ (1- (+ (* (string-to-int bottom) 100) (window-height))) |
(/ (1- (+ (* (string-to-number bottom) 100) (window-height))) |
1269 |
(window-height))))) |
(window-height))))) |
1270 |
;; report scroll margin settings if running interactively |
;; report scroll margin settings if running interactively |
1271 |
(and (interactive-p) |
(and (interactive-p) |