blob: 75995f0563fd5f5e706f75d2bdcc4959a65f0c5b (
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
(add-to-list 'load-path "~/.emacs.d")
;; wrap long lines
(setq truncate-partial-width-windows nil)
;; show parens
(show-paren-mode 1)
;; line numbering
(global-linum-mode 1)
(setq linum-format "%4d ")
;; scrollbar on the right
(set-scroll-bar-mode 'right)
;; theming
(require 'color-theme)
(color-theme-initialize)
(color-theme-charcoal-black)
;; use Poly/ML as SML interpreter
(setq sml-program-name "poly")
;; key bindings
(add-hook 'proof-mode-hook
(lambda () (local-set-key (kbd "M-c") 'unicode-tokens-insert-token)))
(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(indent-tabs-mode nil)
'(isar-display:show-main-goal t)
'(isar-maths-menu-enable t)
'(isar-symbol-shortcuts (quote (("\\/" . "\\<or>") ("/\\" . "\\<and>") ("+O" . "\\<oplus>") ("-O" . "\\<ominus>") ("xO" . "\\<otimes>") ("/O" . "\\<oslash>") (".O" . "\\<odot>") ("|+" . "\\<dagger>") ("|++" . "\\<ddagger>") ("<=" . "\\<le>") ("|-" . "\\<turnstile>") (">=" . "\\<ge>") ("-|" . "\\<stileturn>") ("||" . "\\<parallel>") ("==" . "\\<equiv>") ("~=" . "\\<noteq>") ("~:" . "\\<notin>") ("~~~" . "\\<notapprox>") ("~~" . "\\<approx>") ("~==" . "\\<cong>") ("|<>|" . "\\<bowtie>") ("|=" . "\\<Turnstile>") ("=." . "\\<doteq>") ("_|_" . "\\<bottom>") ("</" . "\\<notle>") ("~>=" . "\\<notge>") ("==/" . "\\<notequiv>") ("~/" . "\\<notsim>") ("~=/" . "\\<notsimeq>") ("~~/" . "\\<notsimeq>") ("<-" . "\\<leftarrow>") ("<=" . "\\<Leftarrow>") ("->" . "\\<rightarrow>") ("=>" . "\\<Rightarrow>") ("<->" . "\\<leftrightarrow>") ("<=>" . "\\<Leftrightarrow>") ("|->" . "\\<mapsto>") ("<--" . "\\<longleftarrow>") ("<==" . "\\<Longleftarrow>") ("-->" . "\\<longrightarrow>") ("==>" . "\\<Longrightarrow>") ("<==>" . "\\<Longleftrightarrow>") ("|-->" . "\\<longmapsto>") ("<->" . "\\<longleftrightarrow>") ("<<" . "\\<guillemotleft>") (">>" . "\\<guillemotright>") ("<>" . "\\<diamond>") ("[|" . "\\<lbrakk>") ("|]" . "\\<rbrakk>") ("{|" . "\\<lbrace>") ("|}" . "\\<rbrace>") ("(|" . "\\<lparr>") ("|)" . "\\<rparr>") ("ALL" . "\\<forall>") ("EX" . "\\<exists>") ("!!" . "\\<And>") ("<|" . "\\<triangleleft>")
("<-->" . "\\<longleftrightarrow>")
("\\sse" . "\\<subseteq>") ("\\ess" . "\\<supseteq>")
("\\|" . "\\<^isub>")
("/|" . "\\<^isup>")
("\\a" . "\\<alpha>")
("\\b" . "\\<beta>")
("\\c" . "\\<chi>")
("\\d" . "\\<delta>")
("\\D" . "\\<Delta>")
("\\e" . "\\<epsilon>")
("\\f" . "\\<phi>")
("\\F" . "\\<Phi>")
("\\g" . "\\<gamma>")
("\\G" . "\\<Gamma>")
("\\i" . "\\<iota>")
("\\k" . "\\<kappa>")
("\\l" . "\\<lambda>")
("\\L" . "\\<Lambda>")
("\\m" . "\\<mu>")
("\\n" . "\\<nu>")
("\\o" . "\\<omega>")
("\\O" . "\\<Omega>")
("\\P" . "\\<Pi>")
("\\p" . "\\<pi>")
("\\q" . "\\<psi>")
("\\Q" . "\\<Psi>")
("\\r" . "\\<rho>")
("\\R" . "\\<Rho>")
("\\s" . "\\<sigma>")
("\\S" . "\\<Sigma>")
("\\t" . "\\<tau>")
("\\x" . "\\<xi>")
("\\X" . "\\<Xi>")
("\\z" . "\\<zeta>")
)))
'(isar-tracing:auto-try nil)
'(isar-unicode-tokens-enable t)
'(isar-unicode-tokens2-enable t)
'(isar-use-find-theorems-form nil)
'(isar-x-symbol-enable nil)
'(proof-delete-empty-windows nil)
'(proof-imenu-enable t)
'(proof-three-window-enable t)
'(show-paren-mode t))
(custom-set-faces
;; custom-set-faces was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(default ((t (:inherit nil :stipple nil :background "Grey15" :foreground "Grey" :inverse-video nil :box nil :strike-through nil :overline nil :underline nil :slant normal :weight normal :height 113 :width normal :foundry "unknown" :family "Inconsolata"))))
'(isabelle-free-name-face ((((type x) (class color) (background dark)) (:foreground "lightblue"))))
'(isabelle-quote-face ((t (:foreground "grey21"))))
'(isabelle-string-face ((((type x) (class color) (background dark)) (:foreground "cyan3"))))
'(isabelle-var-name-face ((((type x) (class color) (background dark)) (:foreground "lightblue3"))))
'(linum ((t (:inherit (shadow default) :foreground "gold"))))
'(proof-boring-face ((((type x) (class color) (background dark)) (:foreground "cyan3"))))
'(proof-highlight-dependency-face ((((type x) (class color) (background dark)) (:background "peru" :foreground "black"))))
'(proof-highlight-dependent-face ((((type x) (class color) (background dark)) (:background "darkorange" :foreground "black"))))
'(proof-region-mouse-highlight-face ((((type x) (class color) (background dark)) (:background "yellow3" :foreground "black"))))
'(proof-warning-face ((((type x) (class color) (background dark)) (:background "orange2" :foreground "black"))))
'(unicode-tokens-symbol-font-face ((t (:slant normal :weight normal :height 113 :width normal :foundry "unknown" :family "DejaVu Sans Mono")))))
|
