blob: 84f1ddc1ef48af6abdac4e2c800a734c34abd6d5 (
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
|
(defun ml4pg-save-lemma-aux (string)
(append-to-file string nil (concat ml4pg-home-dir "lemmas.txt"))
)
(defun ml4pg-save-lemma (name value)
(ml4pg-save-lemma-aux (format "%s&%s$" name value)))
(defun ml4pg-save-view-aux (string)
(append-to-file string nil (concat ml4pg-home-dir "views.txt"))
)
(defun ml4pg-save-view (name value)
(sml4pg-ave-view-aux (format "%s&%s$" name value)))
(defun ml4pg-read-lemmas ()
(if (file-exists-p (concat ml4pg-home-dir "coq/lemmas.txt"))
(with-temp-buffer
(insert-file-contents (concat ml4pg-home-dir "coq/lemmas.txt"))
(let ((temp (format "%s" (read (current-buffer)))))
(setf ml4pg-theorems_id (ml4pg-extract-info-from-files temp))
))))
(defun ml4pg-read-views ()
(if (file-exists-p (concat ml4pg-home-dir "coq/views.txt"))
(with-temp-buffer
(insert-file-contents (concat ml4pg-home-dir "coq/views.txt"))
(let ((temp (format "%s" (read (current-buffer)))))
(setf ml4pg-views_id (ml4pg-extract-info-from-files temp))
))))
(defun ml4pg-extract-info-from-files (string)
(do ((temp string)
(temp2 nil))
((not (search "$" temp)) temp2)
(let ((dollar (search "$" temp))
(amper (search "&" temp)))
(progn
(setf temp2 (append temp2 (list (cons (subseq temp 0 amper)
(string-to-number (subseq temp (1+ amper) dollar))))))
(setf temp (subseq temp (1+ dollar)))))))
|
