1 package acl2s.lib.session;
2
3 import java.io.File;
4 import java.io.FileInputStream;
5 import java.io.FileWriter;
6 import java.io.IOException;
7 import java.util.ArrayList;
8
9 import javax.xml.parsers.ParserConfigurationException;
10 import javax.xml.parsers.SAXParserFactory;
11
12 import org.peterd.util.io.StreamCopier;
13 import org.xml.sax.Attributes;
14 import org.xml.sax.SAXException;
15 import org.xml.sax.helpers.DefaultHandler;
16
17 import acl2s.lib.parse.IParseContext;
18 import acl2s.lib.parse.ParseException;
19 import acl2s.lib.parse.StringParser;
20 import acl2s.lib.parse.obj.Cons;
21 import acl2s.lib.parse.obj.LispObject;
22 import acl2s.lib.parse.obj.Sym;
23 import acl2s.lib_driver.IAcl2sLibErrorHandler;
24
25 public class ModeDir {
26 protected final Sym includeBookDirSym;
27 protected final File home;
28 protected final Sym[] deps;
29 protected final File[] certOrder;
30 protected final SessionMode[] modes;
31 protected final String addIncludeBookDirString;
32
33 ModeDir(File home, Sym includeBookDirSym, Sym[] deps, File[] certOrder, SessionMode[] modes) {
34 if (certOrder == null) certOrder = new File[] {};
35 this.certOrder = certOrder;
36 if (deps == null) deps = new Sym[] {};
37 this.deps = deps;
38 this.home = home;
39 this.includeBookDirSym = includeBookDirSym;
40 if (modes == null) modes = new SessionMode[] {};
41 this.modes = modes;
42 this.addIncludeBookDirString =
43 includeBookDirSym == null ? "" :
44 "(acl2::add-include-book-dir " + includeBookDirSym.toString() +
45 " \"" + MyBaseConfig.toAcl2PathDir(home) + "\")\n";
46 }
47
48 public Sym getIncludeBookDirSym() {
49 return includeBookDirSym;
50 }
51
52 public File getHome() {
53 return home;
54 }
55
56 public Sym[] getDeps() {
57 return deps;
58 }
59
60 public File[] getCertOrder() {
61 return certOrder;
62 }
63
64 public SessionMode[] getModes() {
65 return modes;
66 }
67
68 public String getAddIncludeBookDirString() {
69 return addIncludeBookDirString;
70 }
71
72
73 void maybeWriteDirLsp() {
74 File dirLsp = new File(home, "dir.lsp");
75 if (!dirLsp.exists() || dirLsp.canWrite()) {
76 try {
77 FileWriter w = new FileWriter(dirLsp);
78 w.append(addIncludeBookDirString);
79 w.close();
80 } catch (IOException e) {
81 // ignore
82 }
83 }
84 }
85
86 static final IParseContext bootstrappc = BootstrapParseContext.instance;
87 static final IParseContext keywordpc = BootstrapParseContext.keywordParseInstance;
88
89 static class ModeDirParser extends DefaultHandler {
90 protected IAcl2sLibErrorHandler err;
91 protected File dir;
92 protected String msgPrefix;
93
94 ModeDirParser(IAcl2sLibErrorHandler err, File dir) {
95 this.err = err;
96 this.dir = dir;
97 this.msgPrefix = "While parsing plugin.xml for mode dir " + dir.getAbsolutePath() + ":\n";
98 }
99
100 protected Sym includeBookDir;
101 protected final ArrayList<Sym> deps = new ArrayList<Sym>();
102 protected final ArrayList<File> order = new ArrayList<File>();
103 protected final ArrayList<SessionMode> modes = new ArrayList<SessionMode>();
104
105 boolean inExtension = false;
106
107 @Override
108 public void startElement(String uri, String localName, String name, Attributes attributes)
109 throws SAXException {
|
At conditional (1): this.inExtension: Taking true branch.
|
110 if (inExtension) {
|
At conditional (2): name.equals("include-book-dir-entry"): Taking false branch.
|
111 if (name.equals("include-book-dir-entry")) {
112 int len = attributes.getLength();
113 for (int i = 0; i < len; i++) {
114 if (attributes.getQName(i).equals("keyword")) {
115 String val = attributes.getValue(i);
116 try {
117 includeBookDir = Sym.parse(new StringParser(keywordpc, val));
118 if (!includeBookDir.isKeyword()) {
119 err.error("include-book-dir-entry must be a keyword symbol", null);
120 includeBookDir = null;
121 }
122 } catch (ParseException e) {
123 err.error("Malformed include-book-dir-entry", e);
124 }
125 }
126 }
127 return;
128 }
|
At conditional (3): name.equals("certify-order-element"): Taking false branch.
|
129 if (name.equals("certify-order-element")) {
130 int len = attributes.getLength();
131 for (int i = 0; i < len; i++) {
132 if (attributes.getQName(i).equals("book")) {
133 String val = attributes.getValue(i);
134 String cpath = MyBaseConfig.toSystemPathString(val + ".lisp");
135
136 File f = new File(dir, cpath);
137 if (f.canRead()) {
138 order.add(f);
139 } else {
140 err.error(msgPrefix + "certify-order-element book does not exist: " + val + " (" + cpath + ")", null);
141 }
142 }
143 }
144 return;
145 }
|
At conditional (4): name.equals("dependency"): Taking false branch.
|
146 if (name.equals("dependency")) {
147 int len = attributes.getLength();
148 for (int i = 0; i < len; i++) {
149 if (attributes.getQName(i).equals("keyword")) {
150 String val = attributes.getValue(i);
151 try {
152 Sym d = Sym.parse(new StringParser(keywordpc, val));
153 if (d.isKeyword()) {
154 deps.add(d);
155 } else {
156 err.error(msgPrefix + "include-book-dir-entry must be a keyword symbol", null);
157 }
158 } catch (ParseException e) {
159 err.error(msgPrefix + "Malformed include-book-dir-entry", e);
160 }
161 }
162 }
163 return;
164 }
|
At conditional (5): name.equals("mode"): Taking true branch.
|
165 if (name.equals("mode")) {
166 String mname = null;
167 String sdesc = null;
168 String ldesc = null;
169 boolean bookdev = true;
170 boolean introductory = false;
171 LispObject ttags = Sym.nilInstance;
172 LispObject extraImports = Sym.nilInstance;
173 int precedence = 500;
174 String initData = "";
175
176 int len = attributes.getLength();
|
At conditional (6): (i < len): Taking true branch.
|
|
At conditional (16): (i < len): Taking true branch.
|
|
At conditional (26): (i < len): Taking true branch.
|
|
At conditional (36): (i < len): Taking true branch.
|
|
At conditional (46): (i < len): Taking true branch.
|
|
At conditional (58): (i < len): Taking true branch.
|
|
At conditional (68): (i < len): Taking true branch.
|
|
At conditional (77): (i < len): Taking true branch.
|
|
At conditional (88): (i < len): Taking true branch.
|
|
At conditional (97): (i < len): Taking true branch.
|
|
At conditional (106): (i < len): Taking true branch.
|
|
At conditional (115): (i < len): Taking true branch.
|
|
At conditional (124): (i < len): Taking true branch.
|
|
At conditional (131): (i < len): Taking true branch.
|
|
At conditional (137): (i < len): Taking true branch.
|
|
At conditional (142): (i < len): Taking true branch.
|
|
At conditional (146): (i < len): Taking true branch.
|
|
At conditional (149): (i < len): Taking true branch.
|
|
At conditional (151): (i < len): Taking false branch.
|
177 for (int i = 0; i < len; i++) {
178 String aname = attributes.getQName(i);
179 String val = attributes.getValue(i);
|
At conditional (7): aname.equals("name"): Taking false branch.
|
|
At conditional (17): aname.equals("name"): Taking false branch.
|
|
At conditional (27): aname.equals("name"): Taking false branch.
|
|
At conditional (37): aname.equals("name"): Taking false branch.
|
|
At conditional (47): aname.equals("name"): Taking false branch.
|
|
At conditional (59): aname.equals("name"): Taking false branch.
|
|
At conditional (69): aname.equals("name"): Taking false branch.
|
|
At conditional (78): aname.equals("name"): Taking false branch.
|
|
At conditional (89): aname.equals("name"): Taking false branch.
|
|
At conditional (98): aname.equals("name"): Taking false branch.
|
|
At conditional (107): aname.equals("name"): Taking false branch.
|
|
At conditional (116): aname.equals("name"): Taking false branch.
|
|
At conditional (125): aname.equals("name"): Taking false branch.
|
|
At conditional (132): aname.equals("name"): Taking false branch.
|
|
At conditional (138): aname.equals("name"): Taking false branch.
|
|
At conditional (143): aname.equals("name"): Taking false branch.
|
|
At conditional (147): aname.equals("name"): Taking false branch.
|
|
At conditional (150): aname.equals("name"): Taking true branch.
|
180 if (aname.equals("name")) {
181 mname = val;
|
At conditional (8): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (18): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (28): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (38): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (48): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (60): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (70): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (79): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (90): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (99): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (108): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (117): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (126): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (133): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (139): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (144): aname.equals("short_desc"): Taking false branch.
|
|
At conditional (148): aname.equals("short_desc"): Taking true branch.
|
182 } else if (aname.equals("short_desc")) {
183 sdesc = val;
|
At conditional (9): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (19): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (29): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (39): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (49): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (61): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (71): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (80): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (91): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (100): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (109): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (118): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (127): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (134): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (140): aname.equals("long_desc"): Taking false branch.
|
|
At conditional (145): aname.equals("long_desc"): Taking true branch.
|
184 } else if (aname.equals("long_desc")) {
185 ldesc = val;
|
At conditional (10): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (20): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (30): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (40): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (50): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (62): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (72): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (81): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (92): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (101): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (110): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (119): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (128): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (135): aname.equals("book_dev"): Taking false branch.
|
|
At conditional (141): aname.equals("book_dev"): Taking true branch.
|
186 } else if (aname.equals("book_dev")) {
187 bookdev = Boolean.parseBoolean(val);
|
At conditional (11): aname.equals("ttags"): Taking false branch.
|
|
At conditional (21): aname.equals("ttags"): Taking false branch.
|
|
At conditional (31): aname.equals("ttags"): Taking false branch.
|
|
At conditional (41): aname.equals("ttags"): Taking false branch.
|
|
At conditional (51): aname.equals("ttags"): Taking false branch.
|
|
At conditional (63): aname.equals("ttags"): Taking false branch.
|
|
At conditional (73): aname.equals("ttags"): Taking false branch.
|
|
At conditional (82): aname.equals("ttags"): Taking false branch.
|
|
At conditional (93): aname.equals("ttags"): Taking false branch.
|
|
At conditional (102): aname.equals("ttags"): Taking false branch.
|
|
At conditional (111): aname.equals("ttags"): Taking false branch.
|
|
At conditional (120): aname.equals("ttags"): Taking false branch.
|
|
At conditional (129): aname.equals("ttags"): Taking false branch.
|
|
At conditional (136): aname.equals("ttags"): Taking true branch.
|
188 } else if (aname.equals("ttags")) {
189 try {
190 ttags = LispObject.parseOne(new StringParser(bootstrappc, val));
191 } catch (ParseException e) {
192 err.error(msgPrefix + "Malformed ttags spec for mode", e);
193 }
|
At conditional (12): aname.equals("introductory"): Taking false branch.
|
|
At conditional (22): aname.equals("introductory"): Taking false branch.
|
|
At conditional (32): aname.equals("introductory"): Taking false branch.
|
|
At conditional (42): aname.equals("introductory"): Taking false branch.
|
|
At conditional (52): aname.equals("introductory"): Taking false branch.
|
|
At conditional (64): aname.equals("introductory"): Taking false branch.
|
|
At conditional (74): aname.equals("introductory"): Taking false branch.
|
|
At conditional (83): aname.equals("introductory"): Taking false branch.
|
|
At conditional (94): aname.equals("introductory"): Taking false branch.
|
|
At conditional (103): aname.equals("introductory"): Taking false branch.
|
|
At conditional (112): aname.equals("introductory"): Taking false branch.
|
|
At conditional (121): aname.equals("introductory"): Taking false branch.
|
|
At conditional (130): aname.equals("introductory"): Taking true branch.
|
194 } else if (aname.equals("introductory")) {
195 introductory = Boolean.parseBoolean(val);
|
At conditional (13): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (23): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (33): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (43): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (53): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (65): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (75): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (84): aname.equals("extra_imports"): Taking false branch.
|
|
At conditional (95): aname.equals("extra_imports"): Taking true branch.
|
|
At conditional (104): aname.equals("extra_imports"): Taking true branch.
|
|
At conditional (113): aname.equals("extra_imports"): Taking true branch.
|
|
At conditional (122): aname.equals("extra_imports"): Taking true branch.
|
196 } else if (aname.equals("extra_imports")) {
197 try {
198 extraImports = LispObject.parseOne(new StringParser(bootstrappc, val));
199 extraImports = Cons.maybeDeQuote(extraImports);
200
|
At conditional (96): (acl2s.lib.parse.obj.LispObject.isNotNil(...) != 0): Taking false branch.
|
|
At conditional (105): (acl2s.lib.parse.obj.LispObject.isNotNil(...) != 0): Taking true branch.
|
|
At conditional (114): (acl2s.lib.parse.obj.LispObject.isNotNil(...) != 0): Taking false branch.
|
|
At conditional (123): (acl2s.lib.parse.obj.LispObject.isNotNil(...) != 0): Taking false branch.
|
201 if (extraImports.isNotNil()) {
202 extraImports = Cons.quote(extraImports);
203 }
204 } catch (ParseException e) {
205 err.error(msgPrefix + "Malformed ttags spec for mode", e);
206 }
|
At conditional (14): aname.equals("precedence"): Taking false branch.
|
|
At conditional (24): aname.equals("precedence"): Taking false branch.
|
|
At conditional (34): aname.equals("precedence"): Taking false branch.
|
|
At conditional (44): aname.equals("precedence"): Taking false branch.
|
|
At conditional (54): aname.equals("precedence"): Taking false branch.
|
|
At conditional (66): aname.equals("precedence"): Taking false branch.
|
|
At conditional (76): aname.equals("precedence"): Taking true branch.
|
|
At conditional (85): aname.equals("precedence"): Taking true branch.
|
207 } else if (aname.equals("precedence")) {
208 try {
|
At conditional (86): thrown exception java.lang.NumberFormatException caught on line 210: Taking true branch.
|
209 precedence = Integer.parseInt(val);
|
At conditional (87): caught exception java.lang.NumberFormatException thrown on line 209: Taking true branch.
|
210 } catch (NumberFormatException e) {
211 err.error(msgPrefix + "Malformed precedence for mode", e);
212 }
|
At conditional (15): aname.equals("init_file"): Taking false branch.
|
|
At conditional (25): aname.equals("init_file"): Taking false branch.
|
|
At conditional (35): aname.equals("init_file"): Taking false branch.
|
|
At conditional (45): aname.equals("init_file"): Taking true branch.
|
|
At conditional (55): aname.equals("init_file"): Taking true branch.
|
|
At conditional (67): aname.equals("init_file"): Taking true branch.
|
213 } else if (aname.equals("init_file")) {
214 val = MyBaseConfig.toSystemPathString(val);
215 File initFile = new File(dir,val);
216 try {
|
Event modeled_event: |
Opening a resource with "new java.io.FileInputStream()". |
|
Event alias: |
Assigning: new java.io.FileInputStream() |
| Also see events: |
[return_without_close] |
217 FileInputStream stream = new FileInputStream(initFile);
|
At conditional (56): thrown exception java.io.IOException caught on line 220: Taking true branch.
|
218 initData = new String(StreamCopier.dump(stream));
219 stream.close();
|
At conditional (57): caught exception java.io.IOException thrown on line 218: Taking true branch.
|
220 } catch (IOException e) {
221 err.error(msgPrefix + "Error reading init file " + initFile.getAbsolutePath(), e);
222 }
223 }
224 }
|
At conditional (152): (mname != null): Taking false branch.
|
225 if (mname != null) {
226 modes.add(new SessionMode(dir, mname, sdesc, ldesc, bookdev, ttags.isNotNil(), introductory, extraImports, precedence, new String[] {initData}));
227 }
|
Event return_without_close: |
Returning from routine while a resource is still open. |
| Also see events: |
[modeled_event][alias] |
228 return;
229 }
230 } else {
231 if (name.equals("extension")) {
232 int len = attributes.getLength();
233 for (int i = 0; i < len; i++) {
234 if (attributes.getQName(i).equals("point")) {
235 if (attributes.getValue(i).equals("acl2s.modedir")) {
236 inExtension = true;
237 break;
238 }
239 }
240 }
241 return;
242 }
243 }
244 }
245
246 @Override
247 public void endElement(String uri, String localName, String name)
248 throws SAXException {
249 if (localName.equals("extension")) {
250 inExtension = false;
251 }
252 }
253
254 public ModeDir go() {
255 File pluginFile = new File(dir, "plugin.xml");
256 ModeDir ret = null;
257 try {
258 saxFactory.newSAXParser().parse(pluginFile, this);
259 ret = new ModeDir(dir,includeBookDir,
260 deps.toArray(new Sym[deps.size()]),
261 order.toArray(new File[order.size()]),
262 modes.toArray(new SessionMode[modes.size()]));
263 } catch (SAXException e) {
264 err.error(msgPrefix + "Error parsing " + pluginFile.getAbsolutePath(), e);
265 } catch (IOException e) {
266 err.error(msgPrefix + "Error parsing " + pluginFile.getAbsolutePath(), e);
267 } catch (ParserConfigurationException e) {
268 err.error(msgPrefix + "Error parsing " + pluginFile.getAbsolutePath(), e);
269 }
270 if (ret != null) {
271 ret.maybeWriteDirLsp();
272 }
273 return ret;
274 }
275 }
276
277 public static ModeDir maybeCreate(IAcl2sLibErrorHandler err, File home) {
278 return new ModeDirParser(err, home).go();
279 }
280
281 static SAXParserFactory saxFactory = SAXParserFactory.newInstance();
282 }