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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
;; phox.el
(require 'proof-site)
(proof-ready-for-assistant 'phox)
(require 'proof)
(require 'proof-easy-config) ; easy configure mechanism
(defconst phox-goal-regexp
"\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|\\(fact\\)\\|\\(cor\\(ollary\\)?\\)\\(theo\\(rem\\)?\\)")
(proof-easy-config
'phox "PhoX"
proof-prog-name "phox"
proof-terminal-string "."
proof-script-command-end-regexp"[.][ \n\t\r]"
proof-script-comment-start "(*"
proof-script-comment-end "*)"
proof-goal-command-regexp (concat "^" phox-goal-regexp)
proof-save-command-regexp "^save"
proof-goal-with-hole-regexp (concat "^" phox-goal-regexp "\\(\\([a-zA-Z0-9_']*\\)\\) ")
proof-save-with-hole-regexp "save \\(\\([a-zA-Z0-9_']*\\)\\).[ \n\t\r]"
proof-non-undoables-regexp "\\(undo\\)\\|\\(abort\\)\\|\\(show\\)\\(.*\\)[ \n\t\r]"
proof-goal-command "fact \"%s\"."
proof-save-command "save \"%s\"."
proof-kill-goal-command "abort."
proof-showproof-command "show."
proof-undo-n-times-cmd "undo %s."
proof-auto-multiple-files t
proof-shell-cd-cmd "cd \"%s\"."
proof-shell-interrupt-regexp "Interrupt."
proof-shell-start-goals-regexp "goal [0-9]+/[0-9]+"
proof-shell-end-goals-regexp "%PhoX%"
proof-shell-quit-cmd "quit."
proof-assistant-home-page "http://www.lama.univ-savoie.fr/~raffalli/phox.html"
proof-shell-annotated-prompt-regexp "^\\(>PhoX>\\)\\|\\(%PhoX%\\) "
; proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
proof-shell-init-cmd ""
; proof-shell-proof-completed-regexp "^No subgoals!"
proof-script-font-lock-keywords
'("Cst" "Import" "Use" "Sort"
"new_intro" "new_elim" "new_rewrite"
"add_path" "author" "cd"
"claim" "close_def" "def" "del" "documents"
"depend" "elim_after_intro" "export"
"edel" "eshow" "flag" "goal" "include"
"institute" "path" "print_sort" "priority"
"quit" "save" "search" "tex" "tex_syntax" "title"
"proposition" "prop" "lemma" "lem" "fact" "corollary" "cor"
"theorem" "theo"
; proof command, FIXME: another color
"abort" "absurd" "apply" "axiom" "constraints"
"elim" "from" "goals" "intros" "intro" "instance"
"local" "lefts" "left" "next" "rewrite" "rewrite_hyp"
"rename" "rmh" "trivial" "slh" "use" "undo" "unfold"
"unfold_hyp")
)
;; code for sisplaying unicode borrowed from
;; Erik Parmann, Pål Drange latex-pretty-symbol
(require 'cl-lib)
(defun substitute-pattern-with-unicode-symbol (pattern symbol)
"Add a font lock hook to replace the matched part of PATTERN with the Unicode
symbol SYMBOL.
Symbol can be the symbol directly, no lookup needed."
(interactive)
(font-lock-add-keywords
nil
`((,pattern
(0 (progn
;;Non-working section kind of able to compose multi-char strings:
;; (compose-string-to-region (match-beginning 1) (match-end 1)
;; ,symbol
;; 'decompose-region)
;; (put-text-property (match-beginning 1) (match-end 1) 'display ,symbol)
(compose-region (match-beginning 1) (match-end 1)
,symbol
'decompose-region)
nil))))))
(defun substitute-patterns-with-unicode-symbol (patterns)
"Mapping over PATTERNS, calling SUBSTITUTE-PATTERN-WITH-UNICODE for each of the patterns."
(mapcar #'(lambda (x)
(substitute-pattern-with-unicode-symbol (car x)
(cl-second x)))
patterns))
(defun phox-escape-regex (str)
"Gets a string, e.g. Alpha, returns the regexp matching the escaped
version of it in Phox code, with no chars in [a-z0-9A-Z] after it."
(interactive "MString:")
(concat "\\(" str "\\)"))
;;Goto http://www.fileformat.info/info/unicode/block/mathematical_operators/list.htm and copy the needed character
(defun phox-unicode-simplified ()
"Adds a bunch of font-lock rules to display phox commands as
their unicode counterpart"
(interactive)
(substitute-patterns-with-unicode-symbol
(list
;;These need to be on top, before the versions which are not subscriptet
(list (phox-escape-regex "/\\\\")"∀")
(list (phox-escape-regex "\\\\/")"∃")
(list (phox-escape-regex "->")"→")
(list (phox-escape-regex "&")"∧")
(list (phox-escape-regex "\\bor\\b")"∨")
)))
(add-hook 'phox-mode-hook 'phox-unicode-simplified)
(add-hook 'phox-goals-mode-hook 'phox-unicode-simplified)
(add-hook 'phox-response-mode-hook 'phox-unicode-simplified)
(provide 'phox)
|
