    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    */