blob: aa6ddd23e702064c35b2020c3910bf3bdc537dd7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
;;; proof-auxmodes.el --- Arrange for auxiliary modes to be loaded when required
;;
;; Copyright (C) 2008, 2010 David Aspinall / LFCS Edinburgh
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;; Commentary:
;;
;; Startup code from auxiliary modes are collected here, allowing late
;; loading of their main defining files and the possibility to disable them.
;;
(require 'proof-utils) ; proof-ass, proof-eval...
;;; Code:
;;
;; Maths menu
;;
(defun proof-maths-menu-support-available ()
"A test to see whether maths-menu support is available.
The test loads optional prover-specific config in <foo>-maths-menu.el"
(or (proof-try-require (proof-ass-sym maths-menu)) t))
(proof-eval-when-ready-for-assistant
(if (and (proof-ass maths-menu-enable)
(proof-maths-menu-support-available))
(proof-maths-menu-set-global t)))
;;
;; Unicode tokens
;;
(defun proof-unicode-tokens-support-available ()
"A test to see whether unicode tokens support is available."
;; Requires prover-specific config in <foo>-unicode-tokens.el
;; Loaded before unicode-tokens.el to allow load-time config there
(proof-try-require (proof-ass-sym unicode-tokens)))
(proof-eval-when-ready-for-assistant
(if (and (proof-ass unicode-tokens-enable)
(proof-unicode-tokens-support-available))
(proof-unicode-tokens-set-global t)))
(provide 'proof-auxmodes)
;;; proof-auxmodes.el ends here
|
