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