← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/vl/server/showloc.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/vl/server/showloc.lisp
 
1
; VL Verilog Toolkit
 
2
; Copyright (C) 2008-2014 Centaur Technology
 
3
;
 
4
; Contact:
 
5
;   Centaur Technology Formal Verification Group
 
6
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
 
7
;   http://www.centtech.com/
 
8
;
 
9
; License: (An MIT/X11-style license)
 
10
;
 
11
;   Permission is hereby granted, free of charge, to any person obtaining a
 
12
;   copy of this software and associated documentation files (the "Software"),
 
13
;   to deal in the Software without restriction, including without limitation
 
14
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
15
;   and/or sell copies of the Software, and to permit persons to whom the
 
16
;   Software is furnished to do so, subject to the following conditions:
 
17
;
 
18
;   The above copyright notice and this permission notice shall be included in
 
19
;   all copies or substantial portions of the Software.
 
20
;
 
21
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
22
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
23
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
24
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
25
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
26
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
27
;   DEALINGS IN THE SOFTWARE.
 
28
;
 
29
; Original author: Jared Davis <jared@centtech.com>
 
30
 
 
31
(in-package "VL")
 
32
(include-book "../loader/descriptions")
 
33
(include-book "../loader/inject-comments")
 
34
(include-book "../util/print")
 
35
(local (include-book "../util/arithmetic"))
 
36
 
 
37
 
 
38
; Location display.
 
39
;
 
40
; When the user clicks on a particular location, we want to display a nice
 
41
; page that essentially shows something like this:
 
42
;
 
43
;  module mod ( ... );    } "startline"
 
44
;
 
45
;  ...                    } "hidden before context"  (HBC)
 
46
;
 
47
;  wire w;                } "before" context    (BC)
 
48
;  wire v;                }
 
49
;
 
50
;  assign w = ... ;       } "goal line"
 
51
;
 
52
;  assign v = ... ;       } "after context" (AC)
 
53
;  assign q = ... ;       }
 
54
;
 
55
;  ...                    } "hidden after context" (HAC)
 
56
;
 
57
;  endmodule              } "lastline"
 
58
 
 
59
 
 
60
(define vl-find-description-for-loc ((loc vl-location-p)
 
61
                                     (x   vl-descriptionlist-p))
 
62
  :returns (desc (iff (vl-description-p desc)
 
63
                      desc))
 
64
  ;; Find the first module that contains the desired location.
 
65
  (cond ((atom x)
 
66
         nil)
 
67
        ((vl-location-between-p loc
 
68
                                (vl-description->minloc (car x))
 
69
                                (vl-description->maxloc (car x)))
 
70
         (vl-description-fix (car x)))
 
71
        (t
 
72
         (vl-find-description-for-loc loc (cdr x)))))
 
73
 
 
74
 
 
75
(define vls-showloc-print-bc (contents start goal &key (ps 'ps))
 
76
  ;; Assumes the starting line has already been printed
 
77
  :guard (and (stringp contents)
 
78
              (posp start)
 
79
              (posp goal))
 
80
  ;; The before-context is everything between start and goal, exclusive.
 
81
  (b* ((bc-start  (+ 1 start))
 
82
       (bc-stop   (- goal 1))
 
83
       (bc-nlines (+ 1 (- goal bc-start))))
 
84
    (cond
 
85
     ((< bc-stop bc-start)
 
86
      ;; There's no before context at all, so there's nothing to print.
 
87
      ps)
 
88
 
 
89
     ((<= bc-nlines 5)
 
90
      ;; The before-context is pretty small, so don't hide any of it.
 
91
      (vl-ps-seq
 
92
       (vl-println-markup "<div id=\"showloc_bc\">")
 
93
       (vl-print (str::strlines bc-start bc-stop contents))
 
94
       (vl-println-markup "</div>")))
 
95
 
 
96
     (t
 
97
      ;; The before-context is pretty large.
 
98
      (vl-ps-seq
 
99
       (vl-println-markup "  <a id=\"showloc_hbc_link\" href=\"javascript:void(0)\" onclick=\"showloc_hbc()\">...</a>")
 
100
       (vl-println-markup "<div id=\"showloc_hbc\" style=\"display: none\">")
 
101
       (vl-print (str::strlines bc-start (- bc-stop 4) contents))
 
102
       (vl-println-markup "</div>") ;
 
103
       (vl-println-markup "<div id=\"showloc_bc\">")
 
104
       (vl-print (str::strlines (- bc-stop 3) bc-stop contents))
 
105
       (vl-println-markup "</div>"))))))
 
106
 
 
107
(define vls-showloc-print-ac (contents goal end &key (ps 'ps))
 
108
  ;; Assumes everything up through and including the goal line have already
 
109
  ;; been printed.
 
110
  :guard (and (stringp contents)
 
111
              (posp goal)
 
112
              (posp end))
 
113
  ;; The after-context is everything between goal and end, exclusive.
 
114
  (b* ((ac-start (+ goal 1))
 
115
       (ac-stop  (- end 1))
 
116
       (ac-nlines (+ 1 (- end ac-start))))
 
117
      (cond
 
118
       ((< ac-stop ac-start)
 
119
        ;; No after-context, so nothing to print
 
120
        ps)
 
121
 
 
122
       ((<= ac-nlines 5)
 
123
        ;; The before-context is pretty small, so don't hide any of it.
 
124
        (vl-ps-seq
 
125
         (vl-println-markup "<div id=\"showloc_ac\">")
 
126
         (vl-print (str::strlines ac-start ac-stop contents))
 
127
         (vl-println-markup "</div>")))
 
128
 
 
129
       (t
 
130
        ;; The before-context is pretty large.
 
131
        (vl-ps-seq
 
132
         (vl-println-markup "<div id=\"showloc_ac\">")
 
133
         (vl-print (str::strlines ac-start (+ ac-start 3) contents))
 
134
         (vl-println-markup "</div>")
 
135
         (vl-println-markup "<a id=\"showloc_hac_link\" href=\"javascript:void(0)\" onClick=\"showloc_hac()\">...</a>")
 
136
         (vl-println-markup "<div id=\"showloc_hac\" style=\"display: none\">")
 
137
         (vl-print (str::strlines (+ ac-start 4) ac-stop contents))
 
138
         (vl-println-markup "</div>")
 
139
         )))))
 
140
 
 
141
(define vls-showloc-print-goal (line col &key (ps 'ps))
 
142
  :guard (and (stringp line)
 
143
              (natp col))
 
144
  (vl-ps-seq
 
145
   (vl-println-markup "<div id=\"showloc_goal\">")
 
146
   (vl-println-markup "<a name=\"hac_goal\">")
 
147
   (let ((len (length line)))
 
148
     (if (>= col len)
 
149
         ;; Really this is an error, there's no such column on the goal line.
 
150
         ;; We'll just print whatever the line is.
 
151
         (vl-println line)
 
152
       (vl-ps-seq
 
153
        (vl-print (subseq line 0 col))
 
154
        (vl-print-markup "<span class=\"showloc_goalcol\">")
 
155
        (vl-print (char line col))
 
156
        (vl-print-markup "</span>")
 
157
        (vl-println (subseq line (+ col 1) nil)))))
 
158
   (vl-println-markup "</a>")
 
159
   (vl-println-markup "</div>")))
 
160
 
 
161
(define vls-showloc-print (contents min max line col &key (ps 'ps))
 
162
  :guard (and (stringp contents)
 
163
              (posp min)
 
164
              (posp max)
 
165
              (posp line)
 
166
              (natp col))
 
167
  (vl-ps-seq
 
168
   (if (equal min line)
 
169
       ps
 
170
     (vl-ps-seq (vl-println-markup "<div id=\"showloc_start\">")
 
171
                (vl-println (str::strline min contents))
 
172
                (vl-println-markup "</div>")))
 
173
   (vls-showloc-print-bc contents min line)
 
174
   (vls-showloc-print-goal (str::strline line contents) col)
 
175
   (vls-showloc-print-ac contents line max)
 
176
   (if (equal max line)
 
177
       ps
 
178
     (vl-ps-seq (vl-println-markup "<div id=\"showloc_end\">")
 
179
                (vl-println (str::strline max contents))
 
180
                (vl-println-markup "</div>")))))
 
181