+
+(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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
