blob: cd495e41d05600fca272a6b0f5285b5aee3d05ba (
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
;;here is the code to return a list of all the dependencies
;;FIXME: doesn't even slightly work. First prob is that span-at does not return a span, only nil. Therefore cannot test the rest of the code as just fails at this point.
(defun make-dependency-list (file)
(make-deps-list '() (span-at (point-min file) 'dependencies) (point-max file)))
(defun make-deps-list (list span end-point)
(if (eql (span-end span) end-point)
(append list (span-property span 'dependencies))
(make-deps-list (append list (span-property span 'dependencies)) (next-span span 'dependencies) end-point)))
(defun mytest ()
(save-excursion
(set-buffer proof-script-buffer)
(span-at (point-min) 'type)))
(defun find-span (buffer)
(save-excursion
(set-buffer buffer)
(span-at (point-min) 'type)))
(span-property (find-span "loading.ML") 'type)
(find-span "loading.ML")
(defun find-next-span (buffer span)
(save-excursion
(set-buffer buffer)
(next-span span 'type)))
(span-property (find-next-span "loading.ML" (find-span "loading.ML")) 'dependencies)
;; this is code to add dependency info to files not read through the interface.
;;some testing for matching stuff
So ... one idea is: find out where the message starts, move on x nos of steps from there and then return everything between that place and where we find val it = ().
So ... what buffer is this in? - response buffer
(let ((proof-last-theorem-dependencies
(string-match proof-shell-theorem-dependency-list-regexp message)
(setq p-s-t-d-l-r "Proof General, the theorem dependencies are: ")
(goto-char (+ 45 (string-match p-s-t-d-l-r messq)) (get-buffer "empty"))
;;this returns 60
(search-forward "val it" nil nil nil (get-buffer "empty"))
;;this returns 217
;;so we know that all the information we want is contained in the buffer "empty" between lines 61 and 217.
(car (setq lala (read-from-string "blah blah blah Proof General, the theorem dependencies are: (ProtoPure.rev_triv_goal Protopure.triv_goal HOL.TrueI ProtoPure.rev_triv_goal ProtoPure.triv_goal ProtoPure.revcut_rl HOL.subst loading.even_Suc_Suc)
val it = () : unit
this is a file with lots of stuff in it so that I can practice
searching and see what happens
lots of fun la di la" 60)))
(read-from-string "A short string" 0 10)
(setq noodle (buffer-string (point-min "*isabelle*") (point-max "*isabelle*") (get-buffer "*isabelle*")))
(read-from-string noodle (goto-char (+ 45 (string-match p-s-t-d-l-r noodle)) "*isabelle*"))
(get-buffer "*isabelle*")
(save-excursion
(set-buffer "*isabelle*")
(end-of-buffer)
(search-backward p-s-t-d-l-r)
(setq beginning (+ 47 (point)))
(search-forward "val it")
(buffer-string beginning (- (point) 10)))
(setq messq "blah blah blah Proof General, the theorem dependencies are: ProtoPure.rev_triv_goal ProtoPure.triv_goal HOL.TrueI ProtoPure.rev_triv_goal ProtoPure.triv_goal ProtoPure.revcut_rl HOL.subst loading.even_Suc_Suc
val it = () : unit")
;;sort-deps-list will sort through the list of dependencies and return all those that are not either Protopure or HOL - i.e. will return only those theorems that are written within the file and subject to alteration
;;FIXME: check that ProtoPure and HOL are the only cases that need to be checked for.
(defun sort-deps-list (list1)
(if (null list1)
nil
(if (or (string= '"ProtoPure" (substring (prin1-to-string (car list1)) 0 9))
(string= '"HOL" (substring (prin1-to-string (car list1)) 0 3)))
(sort-deps-list (cdr list1))
(cons (car list1) (sort-deps-list (cdr list1))))))
(sort-deps-list (car lala))
|
