001 /* Copyright 2004, David R. Cok
002 Originally generated as part of a GUI interface to the
003 Esc/Java2 application.
004 */
005
006 package escjava.gui;
007
008 import javax.swing.*;
009 import javax.swing.tree.*;
010 import java.awt.*;
011 import java.awt.event.*;
012 import javax.swing.*;
013 import javax.swing.event.*;
014 import java.util.Vector;
015 import java.util.Enumeration;
016 import java.util.ArrayList;
017 import java.util.Iterator;
018 import java.io.PrintStream;
019 import java.io.ByteArrayOutputStream;
020 import java.io.FileReader;
021 import javafe.ast.CompilationUnit;
022 import javafe.ast.Expr;
023 import javafe.ast.TypeDecl;
024 import javafe.ast.TypeDeclElem;
025 import javafe.ast.RoutineDecl;
026 import javafe.ast.MethodDecl;
027 import javafe.ast.Identifier;
028 import javafe.ast.Util;
029 import javafe.tc.Types;
030 import javafe.tc.OutsideEnv;
031 import javafe.util.Set;
032 import javafe.util.ErrorSet;
033 import javafe.util.Assert;
034 import javafe.util.FatalError;
035 import javafe.util.Location;
036 import javafe.genericfile.GenericFile;
037 import javafe.InputEntry;
038 import javafe.FileInputEntry;
039
040 import escjava.ast.LabelExpr;
041 import escjava.ast.GuardedCmd;
042 import escjava.backpred.FindContributors;
043 import escjava.translate.InitialState;
044 import escjava.translate.Targets;
045 import escjava.translate.VcToString;
046 import escjava.tc.TypeSig;
047 import escjava.tc.TypeCheck;
048 import escjava.translate.Ejp;
049 import escjava.translate.GC;
050 import escjava.translate.GCSanity;
051 import escjava.translate.LabelInfoToString;
052 import escjava.translate.NoWarn;
053 import escjava.translate.Translate;
054 import escjava.translate.UniqName;
055 import escjava.sp.DSA;
056 import escjava.sp.SPVC;
057
058 import escjava.Status;
059
060 import junitutils.Utils;
061
062
063 public class GUI extends escjava.Main {
064
065 static public class Stop extends RuntimeException {}
066 static public final Stop STOP = new Stop();
067
068 volatile public boolean stop = false;
069 private void stopCheck(boolean thr) {
070 if (!stop) return;
071 //System.out.println("STOPPED");
072 if (thr) throw STOP;
073 }
074
075 static GUI gui;
076 static EscFrame escframe;
077 static DefaultMutableTreeNode topNode = new DefaultMutableTreeNode("");
078 static DefaultTreeModel treeModel = new DefaultTreeModel(topNode);
079 EscOutputFrame currentOutputFrame;
080
081 public static void main(String[] args) {
082 //junitutils.Utils.disable = true;
083
084 gui = new GUI();
085
086 Thread t = new WindowThread();
087 t.start();
088
089 gui.run(args); // parses the options and builds the top level tree
090
091 escframe = new EscFrame();
092
093 Thread.currentThread().setPriority( Thread.currentThread().getPriority()-1);
094 // Leave the event queue at a higher priority
095
096 processTasks();
097 }
098
099 /** Reinitializes everything; if the argument is null, the options are
100 not reinitialized.
101 */
102 public void restart(String[] args) {
103 clear(args != null);
104 InputEntry.clear( options.inputEntries );
105 run(args);
106 escframe.init();
107 }
108
109 public /*@non_null*/javafe.Options makeOptions() {
110 return new Options();
111 }
112
113 /** Extends escjava.Options just to set some defaults to more
114 appropriate values for the GUI.
115 */
116 static public class Options extends escjava.Options {
117 public Options() {
118 quiet = true;
119
120 specspath = escjava.Main.jarlocation;
121
122 try {
123 processOption("-nowarn", new String[] { "Deadlock" }, 0);
124 processOption("-source", new String[] { "1.4" }, 0);
125 } catch (javafe.util.UsageError e) {
126 } // FIXME
127 }
128 }
129
130 /** This is overloaded because, instead of automatically running
131 through all inputs, we want to build a gui and give the user
132 control.
133 */
134 public void frontEndToolProcessing(ArrayList args) {
135 preload();
136 handleAllInputEntries();
137 /*
138 loadAllFiles(args);
139 postload(); // FIXME - waht about this ??
140 preprocess();
141 handleAllCUs();
142 postprocess();
143 */
144 }
145
146 public ArrayList extractChildren(DefaultMutableTreeNode d) {
147 ArrayList list = new ArrayList();
148 /* Part of maintaining the tree between reloads, but that is disabled for now
149 Enumeration e = d.children();
150 while (e.hasMoreElements()) {
151 list.add(e.nextElement());
152 }
153 */
154 d.removeAllChildren();
155 return list;
156 }
157
158 public DefaultMutableTreeNode findIEMatch(InputEntry ie, ArrayList oc) {
159 Iterator ii = oc.iterator();
160 while (ii.hasNext()) {
161 DefaultMutableTreeNode d = (DefaultMutableTreeNode)ii.next();
162 IETreeValue v = (IETreeValue)d.getUserObject();
163 if (ie.match(v.ie)) {
164 ii.remove();
165 return d;
166 }
167 }
168 return null;
169 }
170
171 /** Builds the top-level tree, containing just the InputEntry nodes. */
172 public void handleAllInputEntries() {
173 ArrayList args = options().inputEntries;
174 ArrayList oldchildren = extractChildren(topNode);
175 Iterator i = args.iterator();
176 while (i.hasNext()) {
177 InputEntry ie = (InputEntry)i.next();
178 ie = ie.resolve();
179 DefaultMutableTreeNode ienode = findIEMatch(ie,oldchildren);
180 if (ienode != null) {
181 topNode.add(ienode);
182 } else {
183 ienode = IETreeValue.makeNode(ie);
184 topNode.add(ienode);
185 }
186 }
187 treeModel.reload();
188 }
189
190 public void buildCUTree(GFCUTreeValue cuvalue) {
191 CompilationUnit cu = cuvalue.cu;
192 DefaultMutableTreeNode cunode = cuvalue.holder;
193 for (int j=0; j<cu.elems.size(); ++j) {
194 TypeDecl td = cu.elems.elementAt(j);
195 createTDNode(td, cunode);
196 }
197 treeModel.nodeChanged(cunode);
198 if (escframe != null && escframe.guioptionPanel.settings.autoExpand) {
199 escframe.tree.expandPath(new TreePath(cunode.getPath()));
200 int n = cunode.getChildCount();
201 for (int nn=0; nn<n; ++nn) {
202 DefaultMutableTreeNode d = (DefaultMutableTreeNode)cunode.getChildAt(nn);
203 escframe.tree.expandPath(new TreePath(d.getPath()));
204 }
205 }
206 }
207
208 public void createTDNode(TypeDecl td, DefaultMutableTreeNode cunode) {
209 DefaultMutableTreeNode tdnode = TDTreeValue.makeNode(td);
210 cunode.add(tdnode);
211 for (int k=0; k<td.elems.size(); ++k) {
212 TypeDeclElem tde = td.elems.elementAt(k);
213 if (tde instanceof RoutineDecl) {
214 DefaultMutableTreeNode tdenode = RDTreeValue.makeNode((RoutineDecl)tde);
215 tdnode.add(tdenode);
216 } else if (tde instanceof TypeDecl) {
217 createTDNode( (TypeDecl)tde, cunode);
218 }
219 }
220 }
221
222 public void doAll(int action) {
223 if (escframe.guioptionPanel.settings.breadthFirst) {
224 for (int a=0; a<=action; ++a) {
225 Enumeration children = topNode.children();
226 while (children.hasMoreElements()) {
227 Object o = children.nextElement();
228 DefaultMutableTreeNode tn = (DefaultMutableTreeNode)o;
229 EscTreeValue cun = (EscTreeValue)tn.getUserObject();
230 cun.processHelper(a);
231 }
232 }
233 } else {
234 Enumeration children = topNode.children();
235 while (children.hasMoreElements()) {
236 Object o = children.nextElement();
237 DefaultMutableTreeNode tn = (DefaultMutableTreeNode)o;
238 EscTreeValue cun = (EscTreeValue)tn.getUserObject();
239 cun.process(action);
240 }
241 }
242 }
243
244 // This applies the given action to the given type, doing the
245 // parents as well if needed, but not recursively doing all of
246 // the children.
247 //@ requires action == TYPECHECK || action == CHECK;
248 public int processTypeDecl(TDTreeValue tdn, int action) {
249 TypeDecl td = tdn.td;
250 tdn.scope = null;
251 tdn.initState = null;
252 tdn.sig = null;
253 tdn.outputText = null;
254
255 int status = -1;
256
257 try {
258
259 // Duplicates code between here and Main - refactor // FIXME
260 int errorCount = ErrorSet.errors;
261 int cautionCount = ErrorSet.cautions;
262 javafe.tc.TypeSig sig = TypeCheck.inst.getSig(td);
263 sig.typecheck();
264 NoWarn.typecheckRegisteredNowarns();
265 tdn.sig = sig;
266 if (stages >= 2 && ErrorSet.errors == errorCount) {
267 tdn.scope = new FindContributors(sig);
268 VcToString.resetTypeSpecific();
269 }
270 if (stages >= 3 && ErrorSet.errors == errorCount) {
271
272 LabelInfoToString.reset();
273 tdn.initState = new InitialState(tdn.scope);
274 LabelInfoToString.mark();
275 }
276
277 if (ErrorSet.errors > errorCount) {
278 status = Status.TYPECHECKED_ERROR;
279 } else if (ErrorSet.cautions > cautionCount) {
280 status = Status.TYPECHECKED_CAUTION;
281 } else {
282 status = Status.TYPECHECKED_OK;
283 }
284
285 } catch (Stop e) {
286 status = Status.NOTPROCESSED;
287 throw e;
288 } catch (FatalError e) {
289 status = Status.TYPECHECKED_ERROR;
290 } catch (Throwable t) {
291 System.out.println("Exception thrown while handling a type declaration: " + t);
292 t.printStackTrace(System.out);
293 }
294 return status;
295 }
296
297 // This applies the given action to the given routine, doing the
298 // parents as well if needed.
299 // requires action == PARSE;
300 public int processRoutineDecl(RDTreeValue rdn, int action) {
301 RoutineDecl r = rdn.rd;
302 TDTreeValue tdn = (TDTreeValue)rdn.getParent();
303
304 int status = Status.ILLEGAL;
305 ErrorSet.mark();
306 try {
307
308 if (r.body == null) {
309 status = Status.STATICCHECKED_PASSEDIMMED; // FIXME what about cautions
310 } else {
311 Translate.globallyTurnOffChecks(gctranslator.inlineCheckDepth > 0);
312 LabelInfoToString.resetToMark();
313 GuardedCmd gc = computeBody(r, tdn.initState);
314 UniqName.resetUnique();
315 if (gc == null) {
316 status = Status.STATICCHECKED_OK; // passed without checking
317 } else {
318 Set directTargets = Targets.direct(gc);
319 GCSanity.check(gc);
320 // FIXME if (stages<4) ???
321 gc = DSA.dsa(gc);
322 // FIXME if (stages<5) ???
323 Expr vcBody;
324 if (options().spvc) {
325 vcBody = SPVC.compute(gc);
326 } else {
327 vcBody = Ejp.compute(gc, GC.truelit, GC.truelit);
328 }
329 Expr vc = GC.implies(tdn.initState.getInitialState(), vcBody);
330 String label = "vc." + tdn.sig.toString() + ".";
331 if (r instanceof MethodDecl)
332 label += ((MethodDecl)r).id;
333 else
334 label += "<constructor>";
335 label += "." + UniqName.locToSuffix(r.getStartLoc());
336 vc = LabelExpr.make(r.getStartLoc(), r.getEndLoc(),
337 false, Identifier.intern(label), vc);
338
339 // Check for VC too big:
340 int usize = Util.size(vc, options().vclimit);
341 if (usize == -1) {
342 ErrorSet.caution("Unable to check "
343 + TypeCheck.inst.getName(r)
344 + " of type " + TypeSig.getSig(r.parent)
345 + " because its VC is too large");
346 status = Status.STATICCHECKED_TIMEOUT;
347 } else {
348 stopCheck(true);
349
350 // FIXME if (stages<6) ???
351
352 status = Status.STATICCHECKED_ERROR;
353
354 GUI.gui.escframe.showGuiLight(1);
355 status = doProving(vc,r,directTargets,tdn.scope);
356 //System.out.println("DOPROVING " + status);
357 GUI.gui.stopCheck(true);
358 }
359 }
360 }
361
362 } catch (Stop t) {
363 status = Status.NOTPROCESSED;
364 throw t;
365 } catch (escjava.prover.SubProcess.Died t) {
366 ErrorSet.error("Prover died");
367 status = Status.STATICCHECKED_ERROR;
368 } catch (Throwable t) {
369 status = Status.STATICCHECKED_ERROR;
370 System.out.println("An exception was thrown while processing a routine declaration: " + t);
371 t.printStackTrace(System.out);
372 } finally {
373 GUI.gui.escframe.showGuiLight(2);
374 if (ErrorSet.errorsSinceMark())
375 status = Status.STATICCHECKED_ERROR;
376 else if (ErrorSet.cautionsSinceMark() && status == Status.STATICCHECKED_OK)
377 status = Status.STATICCHECKED_CAUTION;
378 }
379 return status;
380 }
381
382 static abstract class EscTreeValue {
383 public int status = Status.NOTPROCESSED;
384 public boolean outOfDate = false;
385 public void setOutOfDate() {
386 outOfDate = true;
387 setOutOfDate(holder);
388 }
389 static public void setOutOfDate(DefaultMutableTreeNode h) {
390 Enumeration e = h.children();
391 while (e.hasMoreElements()) {
392 Object o = e.nextElement();
393 if (!(o instanceof DefaultMutableTreeNode)) return;
394 DefaultMutableTreeNode d = (DefaultMutableTreeNode)o;
395 if (d.getUserObject() instanceof EscTreeValue) {
396 EscTreeValue v = (EscTreeValue)d.getUserObject();
397 v.setOutOfDate();
398 }
399 }
400 }
401 public /*@non_null*/String getStatusText() {
402 return type() + (outOfDate ? " (OUT OF DATE) " : "" )
403 + infoString() + ": " + Status.toString(status);
404 }
405 public /*@non_null*/String infoString() { return toString(); }
406 public String outputText = null;
407 public DefaultMutableTreeNode holder;
408 public int action; // so this can double as a process task
409 abstract public String type();
410 public EscTreeValue getParent() {
411 if (holder == null) return null;
412 Object o = ((DefaultMutableTreeNode)holder.getParent()).getUserObject();
413 if (o instanceof EscTreeValue) return (EscTreeValue)o;
414 return null;
415 }
416 public void setStatus(int status, String outputText) {
417 this.status = status;
418 this.outputText = outputText;
419 if (holder != null) treeModel.nodeChanged(holder);
420 if (escframe != null && escframe.guioptionPanel.settings.autoScroll)
421 escframe.tree.scrollPathToVisible(new TreePath(holder.getPath()));
422 }
423 public void showOutput(boolean showEmpty) {
424 if (!showEmpty && (outputText == null || outputText.length() == 0)) return;
425 if (showEmpty || (escframe != null && escframe.guioptionPanel.settings.autoShowErrors)) {
426 if (GUI.gui.currentOutputFrame == null)
427 GUI.gui.currentOutputFrame = new EscOutputFrame(combinedString(),outputText);
428 else {
429 GUI.gui.currentOutputFrame.setText(outputText);
430 GUI.gui.currentOutputFrame.setTitle(combinedString());
431 }
432 }
433 }
434 public /*@non_null*/String combinedString() { return toString(); }
435
436 // Recursively processes the given action for everything below
437 // this node in the tree
438 public void process(int action) {
439 //System.out.println("PROCESS-" + type() + " " + this + " " + action + " " + Status.toString(status));
440 if (escframe.guioptionPanel.settings.breadthFirst) {
441 for (int a=0; a<=action; ++a) {
442 processHelper(a);
443 }
444 } else {
445 processHelper(action);
446 }
447 //System.out.println("ENDPROCESS-" + type() + " " + this + " " + action + " " + Status.toString(status));
448 }
449 public void processHelper(int action) {
450 if (outOfDate) {
451 outOfDate = false;
452 status = Status.NOTPROCESSED;
453 }
454 processThis(action);
455 if (status == Status.PARSED_ERROR) return;
456 if (status == Status.TYPECHECKED_ERROR) return;
457 Enumeration children = holder.children();
458 while (children.hasMoreElements()) {
459 DefaultMutableTreeNode n = (DefaultMutableTreeNode)children.nextElement();
460 EscTreeValue v = (EscTreeValue)n.getUserObject();
461 v.processHelper(action);
462 }
463 }
464
465 // Processes just this node, not the children, if there is anything to do
466 public void processThis(int action) {
467 GUI.gui.stopCheck(true);
468 if (action == CLEAR) { clearCheck(); return; }
469 int actualAction = actualAction(action);
470 if (actualAction == -10) return;
471 if (actionComplete(status, actualAction)) return;
472
473 EscTreeValue ien = getParent();
474 if (ien != null) {
475 if (!actionComplete(ien.status, actualAction))
476 ien.processThis(actualAction);
477 if (Status.isError(ien.status)) return;
478 }
479 escframe.label.setText(actionString(actualAction) + toString());
480 ByteArrayOutputStream ba = junitutils.Utils.setStreams();
481 try {
482 status = processThisAction(actualAction);
483 } catch (Stop t) {
484 status = Status.NOTPROCESSED;
485 throw t;
486 } catch (Throwable t) {
487 System.out.println("An exception was thrown while processing."
488 + Project.eol + t);
489 t.printStackTrace(System.out);
490 } finally {
491 junitutils.Utils.restoreStreams(true);
492 String out = ba.toString();
493 if (status == Status.NOTPROCESSED) out = "";
494 setStatus(status,out);
495 escframe.label.setText(" ");
496 showOutput(false);
497 if (ien != null) ien.propagateStatus(status);
498 }
499 }
500 abstract public int actualAction(int action);
501 abstract public int processThisAction(int action);
502 abstract public String getFilename();
503 abstract public int getLine();
504
505 public void clearCheck() {
506 // Only TDTreeValues and RDTreeValues do anything
507 }
508
509 public void propagateStatus(int s) {
510 if ((Status.isOK(status) && !Status.isOK(s)) ||
511 (!Status.isError(status) && Status.isError(s))) {
512 setStatus(Status.CHILDERROR,outputText);
513 EscTreeValue v = getParent();
514 if (v != null) v.propagateStatus(s);
515 }
516 if (status == Status.TYPECHECKED_WAITING) {
517 Enumeration c = holder.children();
518 int newstat = Status.PARSED_OK;
519 while (c.hasMoreElements()) {
520 Object o = c.nextElement();
521 DefaultMutableTreeNode d = (DefaultMutableTreeNode)o;
522 o = d.getUserObject();
523 int ss = ((EscTreeValue)o).status;
524 if (ss < newstat) newstat = ss;
525 }
526 if (status != newstat) setStatus(newstat,outputText);
527 }
528 }
529 }
530
531 static class IETreeValue extends EscTreeValue {
532 static public DefaultMutableTreeNode makeNode(InputEntry ie) {
533 EscTreeValue v = new IETreeValue(ie);
534 DefaultMutableTreeNode n = new DefaultMutableTreeNode(v);
535 v.holder = n;
536 v.status = Status.NOTPROCESSED;
537 return n;
538 }
539 public IETreeValue(InputEntry ie) {
540 this.ie = ie;
541 }
542 public InputEntry ie;
543 public String type() { return "Input Entry (" + ie.type() + ") "; }
544 public /*@non_null*/String toString() {
545 return ie.name;
546 }
547 public String getFilename() {
548 if (ie instanceof FileInputEntry)
549 return ie.name;
550 else
551 return null;
552 }
553 public int getLine() { return 1; }
554 public int actualAction(int action) {
555 return RESOLVE;
556 }
557
558 public int processThisAction(int action) {
559 ArrayList a = null;
560 ErrorSet.mark();
561 int s = Status.RESOLVED_ERROR;
562
563 //ByteArrayOutputStream ba = Utils.setStreams();
564 try {
565 a = gui.resolveInputEntry(ie);
566 s = Status.RESOLVED_OK;
567 } catch (Exception e) {
568 System.out.println("Failed to resolve " + ie.name + ": " + e);
569 s = Status.RESOLVED_ERROR;
570 } finally {
571 Utils.restoreStreams(true);
572 }
573 if (ErrorSet.errorsSinceMark()) s = Status.RESOLVED_ERROR;
574 else if (ErrorSet.cautionsSinceMark()) s = Status.RESOLVED_CAUTION;
575
576 if (holder.isLeaf() && a != null && a.size() != 0) {
577 // The contents have not been added to the node tree
578 Iterator i = a.iterator();
579 while (i.hasNext()) {
580 GenericFile gf = (GenericFile)i.next();
581 DefaultMutableTreeNode d = GFCUTreeValue.makeNode(gf,Status.NOTPROCESSED);
582 holder.add(d);
583 }
584 if (escframe != null && escframe.guioptionPanel.settings.autoExpand)
585 escframe.tree.expandPath(new TreePath(holder.getPath()));
586 }
587 return s;
588 }
589 }
590
591 static class GFCUTreeValue extends EscTreeValue {
592 static public DefaultMutableTreeNode makeNode(GenericFile gf, int s) {
593 EscTreeValue v = new GFCUTreeValue(gf);
594 DefaultMutableTreeNode n = new DefaultMutableTreeNode(v);
595 v.holder = n;
596 v.status = s;
597 return n;
598 }
599 public GFCUTreeValue(GenericFile gf) {
600 this.gf = gf;
601 this.cu = null;
602 }
603 public GenericFile gf;
604 public CompilationUnit cu;
605 public String type() { return "Compilation Unit "; }
606 public /*@non_null*/String toString() {
607 return gf.getHumanName();
608 }
609 public /*@non_null*/String infoString() {
610 if (cu == null) return toString();
611 if (!(cu instanceof escjava.RefinementSequence)) return toString();
612 ArrayList a = ((escjava.RefinementSequence)cu).refinements();
613 if (a.size() <= 1) return toString();
614 Iterator i = a.iterator();
615 StringBuffer s = new StringBuffer(((CompilationUnit)i.next()).sourceFile().getHumanName());
616 while (i.hasNext()) {
617 String ss = ((CompilationUnit)i.next()).sourceFile().getHumanName();
618 int n = ss.lastIndexOf('.');
619 s.append("," + ss.substring(n));
620 }
621 return s.toString();
622 }
623 public String getFilename() { return gf.getHumanName(); }
624 public int getLine() { return 1; }
625
626 public int actualAction(int action) {
627 if (action == RESOLVE) return -10;
628 return PARSE;
629 }
630
631 public int processThisAction(int action) {
632 // parse the GenericFile
633 ErrorSet.mark();
634 int s = Status.PARSED_ERROR;
635 CompilationUnit cu = null;
636 try {
637 cu = OutsideEnv.addSource(gf);
638 s = Status.PARSED_OK;
639 } catch (Stop t) {
640 s = Status.NOTPROCESSED;
641 ErrorSet.mark();
642 throw t;
643 } catch (Throwable e) {
644 System.out.println("Parsing failed for " + gf.getHumanName()
645 + ": " + e);
646 e.printStackTrace(System.out);
647 s = Status.PARSED_ERROR;
648 } finally {
649 if (ErrorSet.errorsSinceMark()) s = Status.PARSED_ERROR;
650 else if (ErrorSet.cautionsSinceMark()) s = Status.PARSED_CAUTION;
651 if (cu != null) {
652
653 this.cu = cu;
654
655 if (holder.isLeaf()) {
656 // FIXME - if there are already children are they valid ???
657 // The contents have not been added to the node tree
658 gui.buildCUTree(this);
659 }
660 // FIXME use TYPECHECKED_WAITING???
661 } else {
662 s = Status.PARSED_ERROR;
663 }
664 }
665 return s;
666 }
667 }
668
669 static class TDTreeValue extends EscTreeValue {
670 static public DefaultMutableTreeNode makeNode(TypeDecl td) {
671 EscTreeValue v = new TDTreeValue(td);
672 DefaultMutableTreeNode n = new DefaultMutableTreeNode(v);
673 v.holder = n;
674 v.status = Status.NOTPROCESSED;
675 return n;
676 }
677 public TDTreeValue(TypeDecl td) {
678 this.td = td;
679 }
680 public TypeDecl td;
681 public javafe.tc.TypeSig sig;
682 public InitialState initState;
683 public FindContributors scope;
684 public String type() { return "Type Declaration "; }
685 public /*@non_null*/String toString() {
686 return TypeSig.getSig(td).toString();
687 }
688 public void clearCheck() {
689 if (status == Status.CHILDERROR) setStatus(Status.NOTPROCESSED,null);
690 }
691 public int actualAction(int action) {
692 if (action == CHECK) return TYPECHECK;
693 if (action != TYPECHECK) return -10;
694 return action;
695 }
696 public int processThisAction(int action) {
697 return gui.processTypeDecl(this,action);
698 }
699 public String getFilename() { return Location.toFileName(td.getStartLoc()); }
700 public int getLine() { return Location.toLineNumber(td.getStartLoc()); }
701 }
702
703 static class RDTreeValue extends EscTreeValue {
704 static public DefaultMutableTreeNode makeNode(RoutineDecl rd) {
705 EscTreeValue v = new RDTreeValue(rd);
706 DefaultMutableTreeNode n = new DefaultMutableTreeNode(v);
707 v.holder = n;
708 v.status = Status.NOTPROCESSED;
709 return n;
710 }
711 String sig;
712 public RDTreeValue(RoutineDecl rd) {
713 this.rd = rd;
714 sig = rd.id().toString() + Types.printName(rd.argTypes());
715 }
716 public RoutineDecl rd;
717 public String type() { return "Routine Declaration "; }
718 public /*@non_null*/String toString() {
719 return sig;
720 //return rd.id().toString();
721 }
722 public String getFilename() { return Location.toFileName(rd.getStartLoc()); }
723 public int getLine() { return Location.toLineNumber(rd.getStartLoc()); }
724 public void clearCheck() {
725 if (Status.parsingComplete(status)) setStatus(Status.NOTPROCESSED,null);
726 }
727 public /*@non_null*/String combinedString() { return getParent() + "." + toString(); }
728 public int actualAction(int action) {
729 if (action != CHECK) return -10;
730 return action;
731 }
732 public int processThisAction(int action) {
733 return gui.processRoutineDecl(this,action);
734 }
735 }
736
737 static final int CHECK = 3;
738 static final int TYPECHECK = 2;
739 static final int PARSE = 1;
740 static final int RESOLVE = 0;
741 static final int CLEAR = -1;
742 static final int RELOAD = -2;
743 public static String actionString(int a) {
744 if (a == CHECK) return "Checking ";
745 if (a == TYPECHECK) return "Typechecking ";
746 if (a == PARSE) return "Parsing ";
747 if (a == RESOLVE) return "Resolving ";
748 if (a == CLEAR) return "Clearing ";
749 if (a == RELOAD) return "Reloading files ";
750 return "Unknown Action ";
751 }
752
753 static final boolean actionComplete(int status, int action) {
754 if (action == CHECK) {
755 return Status.checkComplete(status);
756 } else if (action == PARSE) {
757 return Status.parsingComplete(status);
758 } else if (action == TYPECHECK) {
759 return Status.typecheckComplete(status);
760 } else {
761 return Status.resolved(status);
762 }
763 }
764
765 static TaskQueue processTasks = new TaskQueue();
766
767 static void processTasks() {
768 while (true) {
769 try {
770
771 GUI.gui.escframe.showGuiLight(0);
772 Object o = processTasks.getTask();
773 GUI.gui.escframe.showGuiLight(2);
774 if (o instanceof Integer) {
775 int action = ((Integer)o).intValue();
776 //System.out.println("PROCESSING EVERYTHING " + action);
777 if (action == RELOAD) {
778 gui.restart(null);
779 //EscTreeValue.setOutOfDate(topNode);
780 } else {
781 gui.doAll(action);
782 }
783 } else if (o instanceof EscTreeValue) {
784 EscTreeValue v = (EscTreeValue)o;
785 //System.out.println("PROCESSING " + v.action + " " + o.getClass() + " " + o.toString());
786 v.process(v.action);
787 } else if (o instanceof Stop) {
788 GUI.gui.stop = false;
789 } else {
790 System.out.println("UNKNOWN TASK: " + o);
791 }
792
793 } catch (Stop e) {
794 //System.out.println("CAUGHT STOP");
795 } catch (Throwable t) {
796 JOptionPane.showMessageDialog(GUI.gui.escframe,
797 "An exception was thrown while processing: " + t
798 + Project.eol);
799 t.printStackTrace(System.out);
800 }
801 }
802 }
803
804 }
805
806
807 /* Issues:
808
809 - IF a file in an RS has a parse problem (e.g. missing semicolon), no message
810 is reported
811
812 - Problem with Java on XP
813
814 - Is there a problem with options being reset when a project is loaded?
815
816 - Need a button to reset all options to defaults
817
818 - Combine the files of a RS into one entry in the GUI
819
820 - Want skeletons for a whole missing file, a new file in ref sequence, a new method in a file
821 - Integrate other tools - JML, Daikon
822 - Check what happens if there is an error in the RS but not the given file
823 - Chekc the BLue for timeout/big VC
824 - What happens if typechecking depdns on new options after a clear.
825 - Check all the GUI/ESC options
826
827 - Want browse buttons for Classpath, Specpath, Input content
828 - Need checks that Simplify, classpath, spec patah are well-formed
829 - Highlighting a selection on scrolling in an editor does not work
830 - Need more ESC/Options
831 - Would like wild cards for directories, packages, recursive options
832 - Should dispose of editors before there are too many; perhaps limit the number
833 - Provide a menu of created editors
834
835 - Perhaps a button to set the NoWarn options to defaults
836
837 - On windows, the disable All button takes a long time to execute (should not
838 really rebuild the whole pane).
839
840 - Faster stopping of typechecking
841 - Guard against race conditions between checking and new/open projects
842
843 - Change the handling of duplicate inputs
844
845 - would like expand/collapse commands
846
847 - be able to generate skeleton specs
848
849 - Show loaded file info, including spec-only
850
851 - Show other internal info
852
853 - Write documentation
854
855 - Check that all tooltips are available
856
857 - Show project name in title
858 - Allow editing of order of items inthe tree?
859 - Show timem information
860 - Allow skipping of tree items
861 - Cleaing, repainting after an input change takese too long
862 - How to show refinement sequences when creasting an editor
863 - Display a warning when nothing is selected
864 - CHeck all the ... on menu items in Windows
865
866 - Refactor duplicate VC generation code
867
868 - The auto scrolling does not always go to a predicatable position
869
870 - Provide a way to browse for a file to show in an editor
871
872 - Cache the documentation windows
873
874 - Test the combingin of the error ooutput from the methods of a class
875
876 - Allow multiple error windows (and cache them?)
877
878 - Mac won't draw lines in the tree
879
880 - Implement About
881 Accelerator keys
882 New - N
883 Save - S
884 Open - O
885 Editor - E
886 Errors - R
887 Check All - Shift K
888 Check Selected - K
889 Clear ALl - Shift L
890 Clear Selected - L
891 Expand ?
892 Collaps ?
893 Select All - A
894 Clear Selections - Shift A (need on menu also)
895 Stop - Z
896
897 - Be able to filter error messages
898 - keep track of file times and allow updates; track dependencies
899
900 - auto skip items
901
902 - need ssome basic browser capabilty in the documentattion - can we launch a real brwoser?
903
904 - Add an GUI option to turn on/off the memory timer task; set the rate.
905
906 - Enable the Usage menu item, add content
907
908 - Figure out how to reliably set the user.dir from the application
909
910 - the pgc pdsa pvc options don't work (removing duplicated code will help)
911
912 - why does the memory usage keep rising when nothing is happening
913
914
915 */