← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/misc/process-book-readme.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/misc/process-book-readme.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(program)
 
4
 
 
5
(set-state-ok t)
 
6
 
 
7
(defun next-newline (str pos len)
 
8
 
 
9
; Return the position of the next newline character in str starting with pos,
 
10
; if any; else return len.
 
11
 
 
12
  (cond ((int= pos len)
 
13
         len)
 
14
        ((eql (char str pos) #\Newline)
 
15
         pos)
 
16
        (t (next-newline str (1+ pos) len))))
 
17
 
 
18
(defun break-string-into-lines-rec (str pos len acc)
 
19
 
 
20
; Break str into lines, discarding empty lines.
 
21
 
 
22
  (cond ((int= pos len)
 
23
         (reverse acc))
 
24
        ((eql (char str pos) #\Newline)
 
25
         (break-string-into-lines-rec str (1+ pos) len acc))
 
26
        (t (let ((new-pos (next-newline str pos len)))
 
27
             (break-string-into-lines-rec str new-pos len
 
28
                                          (cons (subseq str pos new-pos)
 
29
                                                acc))))))
 
30
 
 
31
(defun find-whitespace-string (string-list)
 
32
  (cond ((endp string-list)
 
33
         nil)
 
34
        ((let* ((str (car string-list))
 
35
                (len (length str)))
 
36
           (or (member-char-stringp #\Space str (1- len))
 
37
               (member-char-stringp #\Tab str (1- len))))
 
38
         (car string-list))
 
39
        (t (find-whitespace-string (cdr string-list)))))
 
40
 
 
41
(defun break-string-into-lines (str msg ctx state)
 
42
  (let* ((lines (break-string-into-lines-rec str 0 (length str) nil))
 
43
         (bad-line (find-whitespace-string lines)))
 
44
    (cond (bad-line (er soft ctx
 
45
                        "Found ~@0 line with whitespace:~%~x1~|"
 
46
                        msg
 
47
                        bad-line))
 
48
          (t (value lines)))))
 
49
 
 
50
(defun process-book-readme-fn (readme-filename state)
 
51
  (declare (xargs :guard (stringp readme-filename)))
 
52
  (let ((ctx 'process-book-readme))
 
53
    (mv-let
 
54
     (channel state)
 
55
     (open-input-channel readme-filename :object state)
 
56
     (cond
 
57
      ((null channel)
 
58
       (er soft ctx
 
59
           "Unable to open file ~x0 for input."
 
60
           readme-filename))
 
61
      (t (mv-let
 
62
          (eofp alist state)
 
63
          (read-object channel state)
 
64
          (pprogn
 
65
           (close-input-channel channel state)
 
66
           (cond (eofp (er soft ctx
 
67
                           "No form could be read from input file ~x0."
 
68
                           readme-filename))
 
69
                 ((not (and (true-list-listp alist)
 
70
                            (alistp (strip-cdrs alist))))
 
71
                  (er soft ctx
 
72
                      "The form read from a book's Readme.lsp file should be ~
 
73
                       an list of true lists each with at least two elements, ~
 
74
                       but ~X01 is not."
 
75
                      alist (default-evisc-tuple state)))
 
76
                 (t (let* ((files-entry    (assoc-eq :FILES alist))
 
77
                           (title-entry    (assoc-eq :TITLE alist))
 
78
                           (author/s-entry (assoc-eq :AUTHOR/S alist))
 
79
                           (keywords-entry (assoc-eq :KEYWORDS alist))
 
80
                           (abstract-entry (assoc-eq :ABSTRACT alist))
 
81
                           (perm-entry     (assoc-eq :PERMISSION alist))
 
82
                           (files    (and (true-listp files-entry)
 
83
                                          (eql (length files-entry) 2)
 
84
                                          (stringp (cadr files-entry))
 
85
                                          (cadr files-entry)))
 
86
                           (title    (and (true-listp title-entry)
 
87
                                          (eql (length title-entry) 2)
 
88
                                          (stringp (cadr title-entry))
 
89
                                          (cadr title-entry)))
 
90
                           (author/s (and (string-listp (cdr author/s-entry))
 
91
                                          (cdr author/s-entry)))
 
92
                           (keywords (and (string-listp (cdr keywords-entry))
 
93
                                          (cdr keywords-entry)))
 
94
                           (abstract (and (true-listp abstract-entry)
 
95
                                          (eql (length abstract-entry) 2)
 
96
                                          (stringp (cadr abstract-entry))
 
97
                                          (cadr abstract-entry)))
 
98
                           (perm     (and (true-listp perm-entry)
 
99
                                          (eql (length perm-entry) 2)
 
100
                                          (stringp (cadr perm-entry))
 
101
                                          (cadr perm-entry))))
 
102
                      (cond
 
103
                       ((not (and files title author/s keywords abstract perm))
 
104
                        (er soft ctx
 
105
                            "No valid field for ~x0 in Readme.lsp alist."
 
106
                            (cond
 
107
                             ((not files) :FILES)
 
108
                             ((not title) :TITLE)
 
109
                             ((not author/s) :AUTHOR/S)
 
110
                             ((not keywords) :KEYWORDS)
 
111
                             ((not abstract) :ABSTRACT)
 
112
                             (t :PERMISSION))))
 
113
                       (t
 
114
                        (pprogn (fms "File ~s0 PASSES the check.~|"
 
115
                                     (list (cons #\0 readme-filename))
 
116
                                     (standard-co state) state nil)
 
117
                                (value :invisible))))))))))))))
 
118
 
 
119
(defmacro process-book-readme (&key dir)
 
120
  (declare (xargs :guard (or (null dir)
 
121
                             (stringp dir))))
 
122
  `(process-book-readme-fn
 
123
    (concatenate
 
124
     'string
 
125
     (let ((dir ,dir))
 
126
       (cond (dir
 
127
              (cond ((eql (char dir (1- (length dir)))
 
128
                          *directory-separator*)
 
129
                     dir)
 
130
                    (t (concatenate 'string dir
 
131
                                    *directory-separator-string*))))
 
132
             (t (cbd))))
 
133
     "Readme.lsp")
 
134
    state))
 
135
 
 
136
; Last updated: Fri Feb 24 11:36:55 2006
 
137