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 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 String getStatusText() {
402                return type() + (outOfDate ? " (OUT OF DATE) " : "" )
403                    + infoString() + ": " + Status.toString(status);
404            }
405            public 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 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 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 String toString() {
607                return gf.getHumanName();
608            }
609            public 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 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 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 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    */