+(if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t))
  ;; Unicode

That doesn't sound right: tool-bar-mode is enabled globally by default,
so forcefully re-enabling it can only undo the user's preference.

The standard Mac port seems to disable it globally by default, this is what Makarius is trying to address.

The code he's showing is only invoked when starting PG via Isabelle's wrapper script, not for all users with all provers, which I think makes it less objectionable. If a user is Emacs-savvy enough to not want the toolbar they can probably start Emacs directly and then load up PG and Isabelle (personally how I've always done it).

 - D.
ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to