1    	package acl2s.plugin.parse;
2    	
3    	import java.util.Stack;
4    	
5    	import org.eclipse.jface.text.BadLocationException;
6    	import org.eclipse.jface.text.IDocument;
7    	import org.eclipse.jface.text.IRegion;
8    	import org.eclipse.jface.text.Position;
9    	import org.eclipse.jface.text.Region;
10   	import org.eclipse.jface.text.source.Annotation;
11   	import org.eclipse.jface.text.source.IAnnotationModel;
12   	
13   	import acl2s.lib.parse.ObjectNotSupported;
14   	import acl2s.lib.parse.ParseException;
15   	import acl2s.lib.parse.Parser;
16   	import acl2s.lib.parse.StringParser;
17   	import acl2s.lib.parse.SymOrNumFns;
18   	import acl2s.lib.parse.obj.Atom;
19   	import acl2s.lib.parse.obj.Char;
20   	import acl2s.lib.parse.obj.LispObject;
21   	import acl2s.lib.parse.obj.Str;
22   	import acl2s.lib.parse.obj.Sym;
23   	import acl2s.plugin.editors.lisp.LispEditor;
24   	
25   	public class LispToken implements Comparable<LispToken> {
26   		// ******************** CONSTANTS ***************** //
27   		public static final char QUOTE_TOK =   '\'';
28   		public static final char BACKTICK_TOK = '`';
29   		public static final char COMMA_TOK =    ',';
30   		public static final char COMAT_TOK =    '@';
31   		public static final char OPAREN_TOK =   '(';
32   		public static final char CPAREN_TOK =   ')';
33   		public static final char STRING_TOK =   '"';
34   		public static final char DOC_TOK =      'd';  // ACL2 doc-string
35   		public static final char DOT_TOK =      '.';
36   		
37   		//those starting with #
38   		public static final char CHAR_TOK =    '\\';  // not necessarily valid
39   		public static final char PQUOTE_TOK =   'f';
40   		public static final char READ_TIME =    '+';
41   		
42   		//could start with #
43   		public static final char NUM_TOK =      'i'; // #c( part of a complex
44   	
45   		public static final char SYM_TOK =      's';
46   		
47   		//fallback case (unrecognized #, potential number, etc.) 
48   		public static final char INVALID_TOK =  'x';
49   		
50   		public static final char EOF_TOK =      'e';
51   		
52   		// special purpose
53   		public static final char NONE_TOK =     '\0';
54   		public static final char SPACE_TOK =    ' ';
55   		
56   		// as contexts only
57   		public static final char POST_OPAREN =   '9';
58   		public static final char POST_DOT =      '>';
59   		public static final char POST_READ_TIME ='=';
60   		
61   		public static final char[] tokenTypes = new char[] {
62   			QUOTE_TOK, BACKTICK_TOK, COMMA_TOK, COMAT_TOK, OPAREN_TOK, CPAREN_TOK,
63   			STRING_TOK, DOC_TOK, DOT_TOK, CHAR_TOK, PQUOTE_TOK, READ_TIME,
64   			NUM_TOK, SYM_TOK, INVALID_TOK, EOF_TOK, NONE_TOK, SPACE_TOK
65   		};
66   		
67   		public static final int tokenIndexLen;
68   		static {
69   			int len = 0;
70   			for (int i = 0; i < LispToken.tokenTypes.length; i++) {
71   				if (LispToken.tokenTypes[i] > len) {
72   					len = LispToken.tokenTypes[i] + 1;
73   				}
74   			}
75   			tokenIndexLen = len;
76   		}
77   		
78   		// *************** INSTANCE STUFF ************** //
79   		public char type;   // one of the above
80   		public boolean newline; // newline in whitespace
81   		public int offset;
82   		public int length;
83   		public int preSpaceLen;
84   		public LispToken ctx;
85   		public MatchingPairNode pairs;  // left & right are w.r.t. offset!
86   		public AnnotationNode tokAnns;
87   		public AnnotationNode ctxErrs;
88   		
89   		public LispToken() {
90   			this(NONE_TOK,0,0,0);
91   		}
92   		
93   		public LispToken(char t, int o, int l, int pl) {
94   			this(t,o,l,pl,null,null, false);
95   		}
96   	
97   		public LispToken(char t, int o, int l, int pl, LispToken c, MatchingPairNode p, boolean n) {
98   			type = t;
99   			offset = o;
100  			length = l;
101  			preSpaceLen = pl;
102  			ctx = c;
103  			pairs = p;
104  			tokAnns = null;
105  			ctxErrs = null;
106  			n = false;
107  		}
108  		
109  		public boolean equals(Object o) {
110  			if (o instanceof LispToken) {
111  				LispToken that = (LispToken) o;
112  				return this.offset == that.offset &&
113  				this.type == that.type;
114  			} else {
115  				return false;
116  			}
117  		}
118  		
119  		public int compareTo(LispToken that) {
120  			return this.offset - that.offset;
121  		}
122  	
123  		public void addPair(int left, int right) {
124  			pairs = new MatchingPairNode(left, right, pairs);
125  		}
126  		
127  		public int absoluteStart() {
128  			return offset - preSpaceLen;
129  		}
130  		
131  		public int absoluteEnd() {
132  			return offset + length;
133  		}
134  		
135  		public IRegion getPreSpaceRegion() {
136  			return new Region(offset - preSpaceLen, preSpaceLen);
137  		}
138  		
139  		public IRegion getTextRegion() {
140  			return new Region(offset, length);
141  		}
142  		
143  		public IRegion getWholeRegion() {
144  			return new Region(offset - preSpaceLen, preSpaceLen + length);
145  		}
146  		
147  		public boolean isOParen() {
148  			return type == OPAREN_TOK;
149  		}
150  		
151  		public boolean isCParen() {
152  			return type == CPAREN_TOK;
153  		}
154  		
155  		public boolean isAtom() {
156  			return type == STRING_TOK || type == DOC_TOK || type == CHAR_TOK || type == NUM_TOK || type == SYM_TOK;
157  		}
158  		
159  		public boolean hasWhitespaceNewline() {
160  			return newline;
161  		}
162  		
163  		public int parenDelta() {
164  			switch (type) {
165  			case OPAREN_TOK:
166  				return 1;
167  			case CPAREN_TOK:
168  				return -1;
169  			default:
170  				return 0;
171  			}
172  		}
173  		
174  		public int matchWithin(int docPos) {
175  			int fromOffset = docPos - offset;
176  			MatchingPairNode cur = pairs;
177  			while (cur != null) {
178  				if (cur.left == fromOffset) {
179  					return offset + cur.right;
180  				}
181  				if (cur.right == fromOffset) {
182  					return offset + cur.left;
183  				}
184  				cur = cur.next;
185  			}
186  			return -1;
187  		}
188  		
189  		private LispToken cloneWithType(char t) {
190  			return new LispToken(t,offset,length,preSpaceLen,ctx,pairs,newline);
191  		}
192  		
193  		public void addAnnotation(IAnnotationModel model, boolean ctxp, String typ, String msg) {
194  			addAnnotation(model, ctxp, typ, msg, offset, length);
195  		}
196  	
197  		public void addAnnotation(IAnnotationModel model, boolean ctxp, String typ, String msg, int start, int len) {
198  			Annotation ann = new Annotation(typ,false,msg);
199  			Position pos = new Position(start,len);
200  			model.addAnnotation(ann,pos);
201  			if (ctxp) {
202  				ctxErrs = new AnnotationNode(ann,pos,ctxErrs);
203  			} else {
204  				tokAnns = new AnnotationNode(ann,pos,tokAnns);
205  			}
206  		}
207  	
208  		public void addError(IAnnotationModel model, boolean ctxp, String msg) {
209  			addError(model, ctxp, msg, offset, length);
210  		}
211  		
212  		public void addError(IAnnotationModel model, boolean ctxp, String msg, int start, int len) {
213  			if (msg != null && model != null) {
214  				addAnnotation(model, ctxp, LispEditor.ERROR_ANNOTATION_TYPE, msg, start, len);
215  			}
216  		}
217  		
218  		public void addWarning(IAnnotationModel model, boolean ctxp, String msg) {
219  			addWarning(model, ctxp, msg, offset, length);
220  		}
221  		
222  		public void addWarning(IAnnotationModel model, boolean ctxp, String msg, int start, int len) {
223  			if (msg != null && model != null) {
224  				addAnnotation(model, ctxp, LispEditor.WARNING_ANNOTATION_TYPE, msg, start, len);
225  			}
226  		}
227  	
228  		public void addTask(IAnnotationModel model, String msg, int start, int len) {
229  			if (msg != null && model != null) {
230  				addAnnotation(model, false, LispEditor.TASK_ANNOTATION_TYPE, msg, start, len);
231  			}
232  		}
233  		
234  		public void removeAllAnnotations(IAnnotationModel model) {
235  			removeTokAnnotations(model);
236  			removeCtxAnnotations(model);
237  		}
238  		
239  		public void removeTokAnnotations(IAnnotationModel model) {
240  			if (tokAnns != null) {
241  				tokAnns.removeFromModel(model);
242  				tokAnns = null;
243  			}
244  		}
245  	
246  		public void removeCtxAnnotations(IAnnotationModel model) {
247  			if (ctxErrs != null) {
248  				ctxErrs.removeFromModel(model);
249  				ctxErrs = null;
250  			}
251  		}
252  	
253  		public boolean hasErrors() {
254  			if (ctxErrs != null) return true;
255  			AnnotationNode cur = tokAnns;
256  			while (cur != null) {
257  				String typ = cur.data.getType();
258  				if (typ.equals(LispEditor.ERROR_ANNOTATION_TYPE) ||
259  					typ.equals(LispEditor.WARNING_ANNOTATION_TYPE)) {
260  					return true;
261  				}
262  				cur = cur.next;
263  			}
264  			return false;
265  		}
266  		
267  		/**
268  		 * Basically, if we insert a newline at document position qoff (within this token), will that be
269  		 * interpreted literally (true) or just as whitespace (false)?.
270  		 * 
271  		 * @throws BadLocationException i hate it.
272  		 */
273  		public boolean isLiteralMode(int qoff, IDocument doc) throws BadLocationException {
274  			if (qoff <= offset) return false;
275  			if (qoff >= offset + length) return false;
276  			switch (type) {
277  			case CHAR_TOK:
278  				return qoff == offset + 2;
279  			case DOC_TOK:
280  			case STRING_TOK:
281  				return true;
282  			case SYM_TOK:
283  				int pos = offset;
284  				for (;;) {
285  					char ch = doc.getChar(pos);
286  					
287  					if (ch == '\\') {
288  						pos++;
289  						if (pos == qoff) return true;
290  					} else if (ch == '|') {
291  						pos++;
292  						if (pos == qoff) return true;
293  						for (;;) {
294  							ch = doc.getChar(pos);
295  							if (ch == '|') break;
296  							if (ch == '\\') {
297  								pos++;
298  								if (pos == qoff) return true;
299  							}
300  							pos++;
301  							if (pos == qoff) return true;
302  						}
303  					}
304  					pos++;
305  					if (pos == qoff) return false;
306  				}
307  			default:
308  				return false;
309  			}
310  		}
311  		
312  		public void toLowercase(IDocument doc) throws BadLocationException {
313  			if (type == SYM_TOK) {
314  				int pos = offset;
315  				int after = offset + length;
316  				for (; pos < after;) {
317  					char ch = doc.getChar(pos);
318  					
319  					if (ch == '\\') {
320  						pos++;
321  					} else if (ch == '|') {
322  						pos++;
323  						for (;;) {
324  							if (pos >= after) break;
325  							ch = doc.getChar(pos);
326  							if (ch == '|') break;
327  							if (ch == '\\') {
328  								pos++;
329  							}
330  							pos++;
331  						}
332  					} else if (Character.isUpperCase(ch)) {
333  						doc.replace(pos, 1, String.valueOf(Character.toLowerCase(ch)));
334  					}
335  					pos++;
336  				}
337  			} else {
338  				// leave everything else as-is
339  			}
340  		}
341  		
342  		public boolean inHashComment(int relOffset) {
343  			if (relOffset >= 0 || relOffset < -preSpaceLen) return false;
344  			MatchingPairNode node = pairs;
345  			while (node != null) {
346  				if (node.left < relOffset && node.right > relOffset) return true;
347  				node = node.next;
348  			}
349  			return false;
350  		}
351  		
352  		public Atom asAtom(IDocument doc) {
353  			assert isAtom();
354  			try {
355  				String str = doc.get(offset, length);
356  				return (Atom) LispObject.parse(new StringParser(null,str));
357  			} catch (BadLocationException e) {
358  				throw new IllegalArgumentException(e);
359  			} catch (ParseException e) {
360  				throw new IllegalArgumentException(e);
361  			}
362  		}
363  		
364  		public Atom asAtom(DocumentParser dp) {
365  			assert isAtom();
366  			try {
367  				dp.setPos(offset);
368  				return (Atom) LispObject.parse(dp);
369  			} catch (ParseException e) {
370  				throw new IllegalArgumentException(e);
371  			}
372  		}
373  		
374  		// ****** PARSING ****** //
375  		public void parseFrom(DocumentParser dp, IAnnotationModel model) {
376  			final int searchStart = dp.getPos();
377  	
378  			pairs = null;
379  			ctx = null;
380  			
381  			skipSpaceAndComments(dp,model);
382  			
383  			offset = dp.getPos();
384  			preSpaceLen = offset - searchStart;
385  			
386  			absolutePairsToRelPairs();
387  			
388  			// look for tasks in comments
389  			String comments = dp.substring(searchStart, offset);
390  			int cPos = 0;
391  			for (;;) {
392  				cPos = comments.indexOf("TODO", cPos); // TODO: add Fixme
393  				if (cPos < 0) break;
394  				int newLinePos = comments.indexOf("\n", cPos);
395  				if (newLinePos < 0) newLinePos = comments.length();
396  				addTask(model, comments.substring(cPos, newLinePos), cPos + searchStart, newLinePos - cPos);
397  				cPos = newLinePos;
398  			}
399  			
400  			// continue with parsing
401  			char ch0 = dp.peek();
402  			char ch1 = dp.peek(1);
403  			switch (ch0) {
404  			case '\'':
405  			case '`':
406  			case '(':
407  			case ')':
408  				type = ch0;
409  				length = 1;
410  				dp.advance(1);
411  				break;
412  			case ',':
413  				if (ch1 == '@') {
414  					type = COMAT_TOK;
415  					length = 2;
416  					dp.advance(2);
417  				} else {
418  					type = COMMA_TOK;
419  					length = 1;
420  					dp.advance(1);
421  				}
422  				break;
423  			case '"':
424  				finishParseString(dp,model);
425  				break;
426  			case ';':
427  				throw new IllegalStateException();
428  			case '#':
429  				switch (ch1) {
430  				case '\\':
431  					type = CHAR_TOK;
432  					dp.advance(2); // another is skipped with first call to next below
433  					if (dp.peek() == Parser.EOF) {
434  						length = 2;
435  						addWarning(model, false, MSG_EOF_IN_CHAR);
436  					} else {
437  						char ch;
438  						do {
439  							ch = dp.next();
440  						} while (!isTerminator(ch));
441  					
442  						length = dp.getPos() - offset;
443  						if (length > 3) {
444  							String s = dp.get(offset+2,length-2);
445  							if (Char.lookupName(s) == null) {
446  								addError(model, false, MSG_INVALID_CHAR_NAME);
447  							}
448  						}
449  					}
450  					break;
451  				case '\'':
452  					type = PQUOTE_TOK;
453  					length = 2;
454  					break;
455  				case '+':
456  				case '-':
457  					type = READ_TIME;
458  					length = 2;
459  					break;
460  				case '|':
461  					throw new IllegalStateException();
462  				default:
463  					finishParseSymOrNum(dp,model);
464  				}
465  				break;
466  			case '.':
467  				if (isTerminator(ch1)) {
468  					type = DOT_TOK;
469  					length = 1;
470  				} else {
471  					finishParseSymOrNum(dp,model);
472  				}
473  				break;
474  			case Parser.EOF:
475  				type = EOF_TOK;
476  				length = 0;
477  				break;
478  			default:
479  				finishParseSymOrNum(dp,model);
480  			}
481  		}
482  		
483  		private void finishParseSymOrNum(DocumentParser dp, IAnnotationModel model) {
484  			int start = dp.getPos();
485  			try {
486  				acl2s.lib.parse.no_obj.Num.parse(dp);
487  				int end = dp.getPos();
488  				type = NUM_TOK;
489  				length = end - start;
490  				if (length >= 4) { // paren match for complex
491  					if (dp.get(start,3).equalsIgnoreCase("#C(")) {
492  						addPair(2,length-1);
493  					}
494  				}
495  				return;
496  			} catch (ObjectNotSupported ons) {
497  				type = INVALID_TOK;
498  				length = dp.getPos() - start;
499  				addError(model, false, ons.getLocalizedMessage());
500  			} catch (ParseException pe) {
501  				try {
502  					dp.setPos(start); // restore
503  					acl2s.lib.parse.no_obj.Sym.parse(dp);
504  					type = SYM_TOK;
505  					length = dp.getPos() - start;
506  					// now, just add the matching pairs
507  					String txt = dp.get(start,length);
508  					int match = -1;
509  					for (int i = 0; i < txt.length(); i++) {
510  						if (txt.charAt(i) == '\\') {
511  							i++;
512  						} else if (txt.charAt(i) == '|') {
513  							if (match < 0) {
514  								match = i;
515  							} else {
516  								addPair(match,i);
517  								match = -1;
518  							}
519  						}
520  					}
521  				} catch (ObjectNotSupported ons) {
522  					type = INVALID_TOK;
523  					length = dp.getPos() - start;
524  					addError(model, false, ons.getLocalizedMessage());
525  				} catch (ParseException pe2) {
526  					length = dp.getPos() - start;
527  					if (pe2.getMessage().substring(0,3).equals("EOF")) {
528  						type = SYM_TOK;
529  						addWarning(model,false,pe2.getLocalizedMessage());
530  					} else {
531  						type = INVALID_TOK;
532  						addError(model,false,pe2.getLocalizedMessage());
533  					}
534  				}
535  			}
536  		}
537  		
538  		private void skipSpaceAndComments(DocumentParser dp, IAnnotationModel model) {
539  			char c;
540  			for(;;) {
541  				switch (dp.peek()) {
542  				case '\r':
543  				case '\n':
544  						newline = true;
545  						// fall through
546  				case ' ':
547  				case '\t':
548  				case '\f':
549  						dp.advance(1);
550  						continue;
551  				case ';':
552  						do {
553  							dp.advance(1);
554  							c = dp.peek();
555  						} while (c != '\n' && c != '\r' && c != Parser.EOF);
556  						continue;
557  				case '#':
558  					if (dp.peek(1) == '|') {
559  						Stack<Integer> stack = new Stack<Integer>();
560  						stack.push(Integer.valueOf(dp.getPos()));
561  						dp.advance(2);  // skip known "#|"
562  						char last = ' ';
563  						for (;;) {
Event example: Example of checking the function's return value.
Also see events: [check_return][example][example][example][example]
564  							char ch = dp.pop();
565  							if (last == '|' && ch == '#') {
566  								int match = stack.pop().intValue();
567  								addPair(match,dp.getPos()-1);
568  								addPair(match+1,dp.getPos()-2);
569  								if (stack.isEmpty()) break;
570  								last = ' ';
571  							} else if (last == '#' && ch == '|') {
572  								stack.push(Integer.valueOf(dp.getPos()-2));
573  								last = ' ';
574  							} else if (ch == Parser.EOF) {
575  								int begin;
576  								dp.setPos(dp.length());
577  								do {
578  									begin = stack.pop().intValue();
579  								} while (!stack.isEmpty());
580  								addWarning(model, false, MSG_EOF_IN_PPCOMMENT,begin,dp.getPos()-begin);
581  								break;
582  							} else {
583  								last = ch;
584  							}
585  						}
586  						continue;
587  					} else {
588  						return; //some other # construct
589  					}
590  				default:
591  					return; // not space or comment
592  				}
593  			}
594  			
595  		}
596  	
597  		private void finishParseString(DocumentParser dp, IAnnotationModel model) {
598  			int start = dp.getPos();
599  			dp.advance(1);
600  			char ch;
601  			for (;;) {
602  				ch = dp.peek();
603  				if (ch == Parser.EOF) {
604  					break;
605  				}
606  				if (ch == '"') {
607  					addPair(0,dp.getPos() - start);
608  					dp.advance(1);
609  					break;
610  				}
611  				if (ch == '\\') {
612  					dp.advance(1);
613  					ch = dp.peek();
614  					if (ch == Parser.EOF) {
615  						break;
616  					}
617  				}
618  				dp.advance(1);
619  			}
620  			length = dp.getPos() - start;
621  			if (length >= 13 && dp.substring(start + 1, start + 13).equalsIgnoreCase(":doc-section")) {
622  				type = DOC_TOK;
623  				if (ch == Parser.EOF) {
624  					addWarning(model, false, MSG_EOF_IN_STRING);
625  				} else {
626  					finishParseDocString(Str.unescapeRobust(dp.substring(start + 13, dp.getPos())), model);
627  				}
628  			} else {
629  				type = STRING_TOK;
630  				if (ch == Parser.EOF) {
631  					addWarning(model, false, MSG_EOF_IN_STRING);
632  				}
633  			}
634  		}
635  	
636  		// text starts after :doc-section
637  		private void finishParseDocString(String text, IAnnotationModel model) {
638  			int len = text.length();
639  			int pos = 0;
640  			if (pos >= len || text.charAt(pos) != ' ') {
641  				addWarning(model, false, "Expecting space after \":doc-section\".");
642  				return;
643  			}
644  			do {
645  				pos++;
646  			} while (pos < len && text.charAt(pos) == ' ');
647  			if (pos >= text.length() || text.charAt(pos) == '\n') {
648  				addWarning(model, false, "Expecting section name after \":doc-section \".");
649  				return;
650  			}
651  			do {
652  				pos++;
653  			} while (pos < len && text.charAt(pos) != '\n');
654  			if (pos >= text.length()) {
655  				addWarning(model, false, "Expecting newline after doc-section name.");
656  				return;
657  			}
658  			pos++;
659  	
660  			// one-liner ; TODO: can't be empty
661  			pos++;
662  			for (;;) {
663  				if (pos >= len) {
664  					addWarning(model, false, "Expecting at least two more \"~/\" separators.");
665  					return;
666  				}
667  				if ((text.charAt(pos - 1) == '~' && text.charAt(pos) == '/')) {
668  					pos++;
669  					break;
670  				}
671  				pos++;
672  			}
673  	
674  			// notes
675  			pos++;
676  			for (;;) {
677  				if (pos >= len) {
678  					addWarning(model, false, "Expecting at least one more \"~/\" separator.");
679  					return;
680  				}
681  				if ((text.charAt(pos - 1) == '~' && text.charAt(pos) == '/')) {
682  					pos++;
683  					break;
684  				}
685  				pos++;
686  			}
687  	
688  			// details ; TODO: can't be empty
689  			pos++;
690  			for (;;) {
691  				if (pos >= len) {
692  					// ok; no separator for & no citations section
693  					return;
694  				}
695  				if ((text.charAt(pos - 1) == '~' && text.charAt(pos) == '/')) {
696  					pos++;
697  					break;
698  				}
699  				pos++;
700  			}
701  	
702  			// citations ; TODO: syntax of citations
703  			return;
704  		}
705  		
706  		private void absolutePairsToRelPairs() {
707  			MatchingPairNode cur = pairs;
708  			while (cur != null) {
709  				cur.left -= offset;
710  				cur.right -= offset;
711  				cur = cur.next;
712  			}
713  		}
714  		
715  		
716  		// **************** CONTEXT STUFF ***************** //
717  		
718  		public void setCtx(LispToken ctx, IAnnotationModel model) {
719  			removeCtxAnnotations(model);
720  			this.ctx = ctx;
721  			String msg = validateContext();
722  			if (msg != null) {
723  				if (msg.startsWith("EOF")) {
724  					addWarning(model,true,msg);
725  				} else {
726  					addError(model,true,msg);
727  				}
728  			}
729  		}
730  		
731  		public boolean hasContextOffset(int ctxOff) {
732  			return ctxOff < 0 || (ctx != null && (ctx.offset == ctxOff || ctx.hasContextOffset(ctxOff)));
733  		}
734  	
735  		public static LispToken nextCtx(LispToken ctx) {
736  			LispToken c = ctx;
737  			while (c != null) {
738  				switch (c.type) {
739  				case CHAR_TOK:
740  				case DOC_TOK:
741  				case STRING_TOK:
742  				case CPAREN_TOK:
743  				case NONE_TOK:
744  				case SYM_TOK:
745  				case NUM_TOK:
746  				case INVALID_TOK:
747  				case EOF_TOK:
748  				default:
749  					throw new IllegalArgumentException();
750  				
751  				case READ_TIME:
752  					return c.cloneWithType(POST_READ_TIME);
753  	
754  				case OPAREN_TOK:
755  					return c.cloneWithType(POST_OPAREN);
756  	
757  				case DOT_TOK:
758  					return c.cloneWithType(POST_DOT);
759  	
760  				case POST_OPAREN:
761  				case POST_DOT:
762  					return c;
763  					
764  				case POST_READ_TIME:
765  				case PQUOTE_TOK:
766  				case QUOTE_TOK:
767  				case BACKTICK_TOK:
768  				case COMAT_TOK:
769  				case COMMA_TOK:
770  					c = c.ctx;
771  					// keep going
772  				}
773  			}
774  			return null;
775  		}
776  		
777  		public LispToken getPostCtx() {
778  			LispToken c = ctx;
779  			switch (type) {
780  			case CPAREN_TOK:
781  			case DOT_TOK:
782  				c = nextCtx(c);
783  				if (c == null) return c;
784  				switch (c.type) {
785  				case OPAREN_TOK:
786  				case DOT_TOK:
787  				case POST_OPAREN:
788  				case POST_DOT:
789  					break;
790  				default:
791  					return c;
792  				}
793  				if (type == DOT_TOK) return c.cloneWithType(DOT_TOK); // re-push
794  				// else do this and fall through
795  				c = c.ctx;
796  			case CHAR_TOK:
797  			case DOC_TOK:
798  			case STRING_TOK:
799  			case SYM_TOK:
800  			case NUM_TOK:
801  			case INVALID_TOK:
802  				c = nextCtx(c);
803  				return c;
804  				
805  			case OPAREN_TOK:
806  			case PQUOTE_TOK:
807  			case QUOTE_TOK:
808  			case BACKTICK_TOK:
809  			case COMAT_TOK:
810  			case COMMA_TOK:
811  			case READ_TIME:
812  				return this;  // push
813  				
814  			case NONE_TOK:
815  				return c;   // no change
816  				
817  			case EOF_TOK:
818  				return null;  // pop all
819  				
820  			default:
821  				throw new IllegalStateException();
822  			}
823  		}
824  		
825  		
826  		
827  		// ************ ERROR CHECKING STUFF ********** //
828  		
829  	
830  		static final String MSG_NONE 				= null;
831  		static final String MSG_CLOSE_NO_OPEN		= "Close paren has no matching open paren";
832  		static final String MSG_OBJECT_BEFORE_CLOSE	= "Object expected before close paren";
833  		static final String MSG_INVALID_CHAR_NAME	= "Invalid named character";
834  		static final String MSG_INVALID_NUM			= "Number format not supported by ACL2";
835  		static final String MSG_INVALID_SYM			= "Invalid format for number or symbol";
836  		static final String MSG_EOF_IN_SYM			= "EOF expecting rest of symbol";
837  		static final String MSG_EOF_NO_OBJECT		= "EOF expecting object";
838  		static final String MSG_EOF_EITHER			= "EOF expecting close paren or object";
839  		static final String MSG_COMMA_NO_BACKTICK	= "Comma has no matching backtick (`) above";
840  		static final String MSG_EOF_IN_CHAR			= "EOF expecting rest of character constant";
841  		static final String MSG_EOF_IN_PPCOMMENT	= "EOF expecting close of #| comment";
842  		static final String MSG_UNSUPPORTED_SYM		= "Unsupported symbol format";
843  		static final String MSG_EOF_IN_STRING		= "EOF expecting close of string";
844  		static final String MSG_ILLEGAL_DOT			= "Illegal dot";
845  		static final String MSG_EOF_NO_CLOSE		= "EOF expecting close paren";
846  		static final String MSG_AFTER_DOT			= "Only one object can follow a dot";
847  		
848  		
849  	
850  		
851  		public String validateContext() {
852  			switch (type) {
853  			case INVALID_TOK:
854  			case NONE_TOK:
855  				return MSG_NONE; // good;  no restrictions
856  	
857  			case CPAREN_TOK:
858  				if (ctx == null) {
859  					return MSG_CLOSE_NO_OPEN;
860  				} else if (ctx.type == OPAREN_TOK || ctx.type == POST_OPAREN || ctx.type == POST_DOT) {
861  					return MSG_NONE; // good
862  				} else {
863  					return MSG_OBJECT_BEFORE_CLOSE;
864  				}
865  	
866  			case DOT_TOK:
867  				if (ctx != null && ctx.type == POST_OPAREN) {
868  					return MSG_NONE; // good
869  				} else {
870  					return MSG_ILLEGAL_DOT;
871  				}
872  				
873  			case CHAR_TOK:
874  			case DOC_TOK:
875  			case STRING_TOK:
876  			case OPAREN_TOK:
877  			case PQUOTE_TOK:
878  			case QUOTE_TOK:
879  			case BACKTICK_TOK:
880  			case READ_TIME:
881  			case SYM_TOK:
882  			case NUM_TOK:
883  				if (ctx != null && ctx.type == POST_DOT) {
884  					return MSG_AFTER_DOT;
885  				}
886  				return MSG_NONE;
887  				
888  			case EOF_TOK:
889  				if (ctx == null)
890  					return MSG_NONE;  // good
891  				else
892  					switch (ctx.type) {
893  					case OPAREN_TOK:
894  					case POST_OPAREN:
895  						return MSG_EOF_EITHER;
896  						
897  					case POST_DOT:
898  						return MSG_EOF_NO_CLOSE;
899  						
900  					case DOT_TOK:
901  					case POST_READ_TIME:
902  					case READ_TIME:
903  					case PQUOTE_TOK:
904  					case QUOTE_TOK:
905  					case BACKTICK_TOK:
906  					case COMAT_TOK:
907  					case COMMA_TOK:
908  						return MSG_EOF_NO_OBJECT;
909  						
910  					default:
911  						throw new IllegalArgumentException();
912  					}
913  				
914  			case COMMA_TOK:  // ... the hard one!
915  			case COMAT_TOK:
916  				if (matchComma(ctx,1) != null) {
917  					return MSG_NONE; // matched; good
918  				} else {
919  					return MSG_COMMA_NO_BACKTICK;
920  				}
921  				
922  			default:
923  				throw new IllegalStateException();
924  			}
925  		
926  		}
927  		
928  		static LispToken matchComma(LispToken ctx, int balance) {
929  			if (ctx == null) return null;
930  			if (ctx.type == BACKTICK_TOK) {
931  				balance--;
932  			} else if (ctx.type == COMMA_TOK) {
933  				balance++;
934  			} else if (ctx.type == COMAT_TOK) {
935  				balance++;
936  			}
937  			if (balance <= 0) {
938  				return ctx;
939  			} else {
940  				return matchComma(ctx.ctx, balance);
941  			}
942  		}
943  	
944  		
945  		// *************** LATER PARSING STUFF ************* //
946  		
947  		public Sym asSym(DocumentParser dp) {
948  			if (type != SYM_TOK) return null;
949  			dp.setPos(offset);
950  			try {
951  				return Sym.parse(dp);
952  			} catch (ParseException pe) {
953  				return null; // shouldn't happen
954  			}
955  		}
956  		
957  		
958  		
959  		// ***************** STATIC STUFF ***************** //
960  		private static boolean isTerminator(char x) {
961  			return SymOrNumFns.isTerminator(x);
962  		}
963  		
964  		public static LispToken parse(DocumentParser dp, IAnnotationModel model) {
965  			LispToken tok = new LispToken();
966  			tok.parseFrom(dp,model);
967  			return tok;
968  		}
969  	
970  		public static int contextOffset(LispToken t) {
971  			if (t == null) {
972  				return -1;
973  			} else {
974  				return t.offset;
975  			}
976  		}
977  		
978  		public static LispToken meetContexts(LispToken t1, LispToken t2) {
979  			int c1 = contextOffset(t1);
980  			int c2 = contextOffset(t2);
981  			if (c1 == c2) {
982  				return t1;
983  			} else if (c1 < c2) {
984  				assert t2 != null;
985  				return meetContexts(t1,t2.ctx);
986  			} else {
987  				assert t1 != null;
988  				return meetContexts(t1.ctx,t2);
989  			}
990  		}
991  	
992  	
993  		/*
994  		private static boolean isEOL(char x) {
995  			return x == '\n' || x == '\r' || x == '\f';
996  		}
997  	
998  		
999  		
1000 		// -1 -> no autoindent
1001 		// 0  ->  indent at 0
1002 		// 1  -> compute indent like code
1003 		public int customIndent(A2sDocument doc) {
1004 			if (type == SEMI_COMMENT) {
1005 				try {
1006 					int i = offset + 1;
1007 					while (i < doc.getLength() && doc.getChar(i) == ';') i++;
1008 					int semiCount = i - offset;
1009 					if (semiCount == 1) {
1010 						return 0;
1011 					} else if (semiCount == 2) {
1012 						return 1;
1013 					} else {
1014 						return -1;
1015 					}
1016 				} catch (BadLocationException e) {
1017 					e.printStackTrace();
1018 				} // fall through (impossible anyway)
1019 			}
1020 			return 1;
1021 		}
1022 		*/
1023 	}