.emacs-my
changeset 875 ad6675a2cc8e
parent 874 02cbb7560e64
child 876 054d954a435e
equal deleted inserted replaced
874:02cbb7560e64 875:ad6675a2cc8e
  2146 (add-to-list 'auto-mode-alist '("\\.cygport\\'" . shell-script-mode))
  2146 (add-to-list 'auto-mode-alist '("\\.cygport\\'" . shell-script-mode))
  2147 
  2147 
  2148 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  2148 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  2149 (message "pg, Proof General")
  2149 (message "pg, Proof General")
  2150 
  2150 
  2151 (setq proof-splash-enable t)
  2151 (setq proof-splash-enable nil)
  2152 ;; (setq proof-toolbar-enable nil)
  2152 ;; (setq proof-toolbar-enable nil)
  2153 
  2153 
  2154 (setq isar-display:show-types t)
  2154 (setq
  2155 (setq isar-display:show-sorts t)
  2155  isar-display:show-types t
  2156 (setq isar-display:show-consts t)
  2156  isar-display:show-sorts t
  2157 (setq isar-display:show-brackets t)
  2157  isar-display:show-main-goal t
  2158 (setq isar-display:show-main-goal t)
  2158  isar-display:show-brackets t
       
  2159  ;; Too many output, so commented:
       
  2160  ;; isar-display:show-consts t
       
  2161  )
  2159 
  2162 
  2160 (eval-after-load 'proof
  2163 (eval-after-load 'proof
  2161   '(progn
  2164   '(progn
  2162      ;; (proof-maths-menu-toggle 1)
  2165      ;; (proof-maths-menu-toggle 1)
  2163      ;; (unicode-tokens-mode 1)
  2166      ;; (unicode-tokens-mode 1)