Info-use-header-line

[David Reitter]

Header lines may be set by minor modes and not just the major mode  
being implemented.  An example is tabbar.
Is it a good idea to hide the header line if the user chooses to not  
display a header line in a mode?  I think not.

A really good solution would, by the way, show global and local header  
lines, but I think there's only one header line allowed at this point.



*** info.el     06 Apr 2008 07:51:37 -0400      1.501.2.7
--- info.el     17 Oct 2008 22:46:43 -0400      
***************
*** 3454,3463 ****
    (make-local-variable 'Info-history)
    (make-local-variable 'Info-history-forward)
    (make-local-variable 'Info-index-alternatives)
!   (setq header-line-format
!       (if Info-use-header-line
!           '(:eval (get-text-property (point-min) 'header-line))
!         nil)) ; so the header line isn't displayed
    (set (make-local-variable 'tool-bar-map) info-tool-bar-map)
    ;; This is for the sake of the invisible text we use handling  
titles.
    (make-local-variable 'line-move-ignore-invisible)
--- 3454,3462 ----
    (make-local-variable 'Info-history)
    (make-local-variable 'Info-history-forward)
    (make-local-variable 'Info-index-alternatives)
!   (if Info-use-header-line    ; do not override global header lines
!       (setq header-line-format
!           '(:eval (get-text-property (point-min) 'header-line))))
    (set (make-local-variable 'tool-bar-map) info-tool-bar-map)
    ;; This is for the sake of the invisible text we use handling  
titles.
    (make-local-variable 'line-move-ignore-invisible)