001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.visualdebugger.executiontree;
009:
010: import java.util.LinkedList;
011:
012: import javax.swing.SwingUtilities;
013:
014: import de.uka.ilkd.key.gui.AutoModeListener;
015: import de.uka.ilkd.key.gui.KeYMediator;
016: import de.uka.ilkd.key.java.statement.Throw;
017: import de.uka.ilkd.key.logic.*;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.proof.*;
020: import de.uka.ilkd.key.rule.*;
021: import de.uka.ilkd.key.visualdebugger.*;
022:
023: public class ExecutionTree implements AutoModeListener {
024:
025: private static ETNode etNodeRoot = null;
026:
027: private static ETNode etTreeBeforeMerge;
028:
029: private static boolean hideInf = true;
030:
031: private static ITNode itNodeRoot = null;
032:
033: public static final int RAWTREE = 1;
034:
035: public static final int SLET = 2;
036:
037: public static final int SLET2 = 3;
038:
039: public static final int SLET3 = 4;
040:
041: public static int treeStyle = SLET3;
042:
043: public static ETNode getETNode() {
044: return etNodeRoot;
045:
046: }
047:
048: public static ETNode getEtTreeBeforeMerge() {
049: return etTreeBeforeMerge;
050: }
051:
052: public static ITNode getITNode() {
053: return itNodeRoot;
054: }
055:
056: private boolean intro_post;
057:
058: private LinkedList listeners = new LinkedList();
059:
060: private KeYMediator mediator;
061:
062: private VisualDebugger vd = VisualDebugger.getVisualDebugger();
063:
064: public ExecutionTree(Proof p, KeYMediator m, boolean b) {
065: this .mediator = m;
066: intro_post = b;
067: }
068:
069: public void addListener(DebuggerListener listener) {
070: listeners.add(listener);
071: }
072:
073: // duplicate in updatelabel listener
074:
075: public void autoModeStarted(ProofEvent e) {
076: vd.fireDebuggerEvent(new DebuggerEvent(
077: DebuggerEvent.EXEC_STARTED, null));
078: }
079:
080: public void autoModeStopped(ProofEvent e) {
081: if (intro_post) {
082: intro_post();
083: intro_post = false;
084: vd.setInitPhase(false);
085: vd.getBpManager().setNoEx(false);
086: vd.stepToFirstSep();
087: } else {
088: vd.fireDebuggerEvent(new DebuggerEvent(
089: DebuggerEvent.EXEC_FINISHED, null));
090: }
091:
092: final Runnable execTreeThread = new Runnable() {
093: public void run() {
094: // new StateVisualization(node,mediator);
095: createExecutionTree();
096: }
097: };
098: // mediator.invokeAndWait(interfaceSignaller);
099:
100: if (mediator.getProof() != null) {
101: startThread(execTreeThread);
102: }
103: }
104:
105: public void buildETree(ITNode n, ListOfTerm terms, ETNode parent,
106: String exc) {
107: ETNode branch = parent;
108: String newExc = exc;
109: ListOfTerm bc = terms;
110: if (n.getBc() != null) {
111: bc = bc.append(n.getBc());
112: } else {
113: bc = null;
114: }
115:
116: if (n.getStatementId() != null) {
117: branch = new ETStatementNode(bc, n.getStatementId(), parent);
118: branch.addITNode(n);
119: parent.addChild(branch);
120: bc = SLListOfTerm.EMPTY_LIST;
121: newExc = null;
122: } else if (n.getExprId() != null && n.getExprId().isBoolean()) {
123: branch = new ETStatementNode(bc, n.getExprId(), parent);
124: branch.addITNode(n);
125: parent.addChild(branch);
126: bc = SLListOfTerm.EMPTY_LIST;
127: newExc = null;
128: } else if (n.isMethodInvocationForET()) {
129: branch = new ETMethodInvocationNode(bc, n
130: .getProgramMethod(), n.getMethodReference(), n
131: .getParameter(), n.getValues(), parent);
132: branch.addITNode(n);
133: parent.addChild(branch);
134: bc = SLListOfTerm.EMPTY_LIST;
135: newExc = null;
136: } else if (n.isMethodReturn()
137: && n.getParent().getMethodNode()
138: .isMethodInvocationForET()) {
139: branch = new ETMethodReturnNode(bc, n
140: .getMethodReturnResult(), parent);
141: branch.addITNode(n);
142: parent.addChild(branch);
143: bc = SLListOfTerm.EMPTY_LIST;
144: newExc = null;
145: } else if (n.getChildren().length > 1
146: || (n.getChildren().length == 1 && n.getChildren()[0]
147: .getBc() == null)) {// this
148: // case
149: // should
150: // not
151: // happen
152: branch = new ETNode(bc, parent);
153: branch.addITNode(n);
154: if (n.isNobc())
155: branch.setNobc(true);
156: parent.addChild(branch);
157: bc = SLListOfTerm.EMPTY_LIST;
158:
159: } else if (n.getChildren().length == 0) {
160: branch = createLeafNode(n, bc, exc, parent);
161: parent.addChild(branch);
162: bc = SLListOfTerm.EMPTY_LIST;
163: }
164:
165: if (bc == null) {
166: bc = SLListOfTerm.EMPTY_LIST;
167: }
168:
169: if (n.getActStatement() instanceof Throw) {
170: newExc = n.getActStatement().toString();
171: }
172:
173: ITNode[] childs = n.getChildren();
174: for (int i = 0; i < childs.length; i++) {
175: buildETree(childs[i], bc, branch, newExc);
176: }
177:
178: }
179:
180: private void buildITTree(Node n, int currentId,
181: boolean lookingForBC, ITNode parent, ListOfTerm terms) {
182: int newId = currentId;
183: boolean looking = lookingForBC;
184: ITNode newParent = parent;
185: ListOfTerm newTerms = terms;
186:
187: int gId = greatestLabel(n.getNodeInfo()
188: .getVisualDebuggerState().getLabels().values());
189: if (gId > currentId) {
190: newId = gId;
191: looking = true;
192: }
193:
194: ListOfTerm l = SLListOfTerm.EMPTY_LIST;
195:
196: boolean atomic = true;
197: if (looking) {
198: HashMapFromPosInOccurrenceToLabel labels = n.getNodeInfo()
199: .getVisualDebuggerState().getLabels();
200: IteratorOfPosInOccurrence pioIt = labels.keyIterator();
201:
202: // case: {u}post TODO
203: while (pioIt.hasNext()) {
204: PosInOccurrence pio = pioIt.next();
205: PCLabel pcLabel = ((PCLabel) labels.get(pio));
206: // if (!containsJavaBlock(pio.constrainedFormula().formula()))
207: // pc = pc.append(pio.constrainedFormula().formula());
208:
209: if (pcLabel.getId() == newId) {
210:
211: if (!isLiteral(pio)) {
212: atomic = false;
213: break;
214: }
215:
216: if (!containsJavaBlock(pio.constrainedFormula()
217: .formula())) {
218: Term t = pio.constrainedFormula().formula();
219: if (pio.isInAntec())
220: l = l.append(t);
221: else {
222: if (t.op() == Op.NOT) {
223: l = l.append(t.sub(0));
224: } else
225: l = l.append(TermFactory.DEFAULT
226: .createJunctorTermAndSimplify(
227: Op.NOT, t));
228: }
229: }
230: }
231: }
232:
233: if (atomic
234: && (!onlyBCInvolvedInTacletApp(n, newId)
235: || n.childrenCount() > 1 || n
236: .childrenCount() == 0)) {
237: newTerms = l;
238: looking = false;
239: }
240: }
241:
242: if (n.getAppliedRuleApp() != null
243: && n.getAppliedRuleApp().posInOccurrence() != null
244: && modalityTopLevel(n.getAppliedRuleApp()
245: .posInOccurrence())) {
246: newParent = new ITNode(newTerms, getPc(n.getNodeInfo()
247: .getVisualDebuggerState().getLabels()), n, parent);
248: parent.addChild(newParent);
249: newTerms = null;
250: } else if (!looking && n.childrenCount() > 1) {
251: newParent = new ITNode(newTerms, getPc(n.getNodeInfo()
252: .getVisualDebuggerState().getLabels()), n, parent);
253: newParent.setNobc(true);
254: parent.addChild(newParent);
255: newTerms = null;
256: } else if (n.childrenCount() == 0 && !looking) {
257: newParent = new ITNode(newTerms, getPc(n.getNodeInfo()
258: .getVisualDebuggerState().getLabels()), n, parent);
259: parent.addChild(newParent);
260: newTerms = null;
261: }
262:
263: final IteratorOfNode it = n.childrenIterator();
264: while (it.hasNext()) {
265: buildITTree(it.next(), newId, looking, newParent, newTerms);
266: }
267: }
268:
269: public void buildSLETWithoutExpr(ETNode n, ETNode parent,
270: ListOfTerm bc) {
271: ETNode branch = parent;
272:
273: ListOfTerm newBC = bc;
274:
275: if (!(n instanceof ETStatementNode)
276: && !(n instanceof ETLeafNode)
277: && !(n instanceof ETMethodInvocationNode)
278: && !(n instanceof ETMethodReturnNode)) {
279: if (n.getBC() != null)
280: newBC = newBC.append(n.getBC());
281:
282: } else {
283: branch = n.copy(parent);
284: branch.setChildren(new LinkedList());
285: if (n.getBC() != null)
286: branch.appendBC(bc);
287: parent.addChild(branch);
288: newBC = SLListOfTerm.EMPTY_LIST;
289: }
290:
291: ETNode[] childs = n.getChildren();
292: for (int i = 0; i < childs.length; i++) {
293: buildSLETWithoutExpr(childs[i], branch, newBC);
294: }
295:
296: }
297:
298: private boolean containsJavaBlock(Term t) {
299: if (!t.javaBlock().isEmpty() || t.op() == vd.getPostPredicate()) {
300: return true; // TODO
301: }
302: for (int i = 0, ar = t.arity(); i < ar; i++) {
303: if (containsJavaBlock(t.sub(i))) {
304: return true;
305: }
306: }
307: return false;
308: }
309:
310: private void createExecutionTree() {
311: if (mediator.getProof() == null) {
312: itNodeRoot = null;
313: etNodeRoot = null;
314: return;
315: }
316: ITNode root = new ITNode(mediator.getProof().root());
317: buildITTree(mediator.getProof().root(), -1, false, root,
318: SLListOfTerm.EMPTY_LIST);
319: ETNode etrr = new ETNode(SLListOfTerm.EMPTY_LIST, null);
320: itNodeRoot = root;
321:
322: buildETree(root, SLListOfTerm.EMPTY_LIST, etrr, null);
323: etTreeBeforeMerge = etrr;
324: ETNode merged = mergeTree(etrr, null);
325: if (hideInf)
326: merged = this .hideInf(merged, null);
327:
328: ETNode etrr2 = new ETNode(SLListOfTerm.EMPTY_LIST, null);
329: buildSLETWithoutExpr(merged, etrr2, SLListOfTerm.EMPTY_LIST);// mergeTree(etrr);
330:
331: etNodeRoot = etrr2.getChildren()[0];
332: simplifyBC(etNodeRoot);
333:
334: fireTreeChanged(root);
335: }
336:
337: private ETNode createLeafNode(ITNode n, ListOfTerm bc, String exc,
338: ETNode parent) {
339: ETNode branch;
340: if (n.getNode().isClosed()) {
341: // System.out.println("new INf");
342: branch = new ETLeafNode(bc, ETLeafNode.INFEASIBLE, parent);
343: branch.addITNode(n);
344: } else {
345:
346: SourceElementId progC = vd.getProgramCounter(n.getNode());
347: // System.out.println("ProgramC: "+progC);
348: if (progC != null) {
349: branch = new ETStatementNode(bc, progC, parent);
350: branch.addITNode(n);
351: // ((ETLeafNode)branch).setProgramCounter(progC);
352: } else {
353:
354: branch = new ETLeafNode(bc, ETLeafNode.TERMINATED,
355: parent);
356: branch.addITNode(n);
357: ((ETLeafNode) branch).setExceptionName(exc);
358: }
359: }
360:
361: return branch;
362: }
363:
364: public boolean exceptionThrown(Node n) {
365: final Sequent s = n.sequent();
366: for (IteratorOfConstrainedFormula it = s.succedent().iterator(); it
367: .hasNext();) {
368: ConstrainedFormula cfm = it.next();
369: if (vd.modalityTopLevel(new PosInOccurrence(cfm,
370: PosInTerm.TOP_LEVEL, false)) != null)
371: return false;
372:
373: }
374: return true;
375: }
376:
377: public boolean executionTerminatedNormal(Node n) {
378: final Sequent s = n.sequent();
379: for (IteratorOfConstrainedFormula it = s.succedent().iterator(); it
380: .hasNext();) {
381: ConstrainedFormula cfm = it.next();
382: final Term f = cfm.formula();
383: if (f.op() instanceof QuanUpdateOperator) {
384: final Term subOp = ((QuanUpdateOperator) f.op())
385: .target(f);
386: if (subOp.op() == vd.getPostPredicate()
387: && subOp.javaBlock().isEmpty()) {
388: return true;
389: }
390: }
391: }
392: return false;
393: }
394:
395: private void fireTreeChanged(ITNode root) {
396: synchronized (listeners) {
397: DebuggerEvent event = new DebuggerEvent(
398: DebuggerEvent.TREE_CHANGED, root);
399: vd.fireDebuggerEvent(event);
400: }
401: }
402:
403: private ListOfTerm getPc(HashMapFromPosInOccurrenceToLabel labels) {
404: IteratorOfPosInOccurrence pioIt = labels.keyIterator();
405: ListOfTerm pc = SLListOfTerm.EMPTY_LIST;
406:
407: while (pioIt.hasNext()) {
408: PosInOccurrence pio = pioIt.next();
409: // PCLabel pcLabel = ((PCLabel)labels.get(pio));
410: if (!containsJavaBlock(pio.constrainedFormula().formula())) {
411: Term t = pio.constrainedFormula().formula();
412: if (pio.isInAntec())
413: pc = pc.append(t);
414: else {
415: if (t.op() == Op.NOT) {
416: pc = pc.append(t.sub(0));
417: } else
418: pc = pc
419: .append(TermFactory.DEFAULT
420: .createJunctorTermAndSimplify(
421: Op.NOT, t));
422: }
423:
424: // pc = pc.append(pio.constrainedFormula().formula());
425: }
426:
427: }
428: return pc;
429: }
430:
431: private int greatestLabel(IteratorOfLabel it) {
432: int current = -1;
433: if (it != null)
434: while (it.hasNext()) {
435: PCLabel pc = (PCLabel) it.next();
436: if (pc.getId() > current)
437: current = pc.getId();
438: }
439: return current;
440: }
441:
442: public ETNode hideInf(ETNode n, ETNode parent) {
443: ETNode newNode = n.copy(parent);
444: ETNode[] childs = n.getChildren();
445: LinkedList newChilds = new LinkedList();
446:
447: for (int i = 0; i < childs.length; i++) {
448: ETNode child = childs[i];
449: if (child instanceof ETLeafNode
450: && ((ETLeafNode) child).getState() == ETLeafNode.INFEASIBLE) {
451: // System.out.println("asfasfasgag");
452:
453: } else {
454: newChilds.add(hideInf(child, newNode));
455: }
456: }
457: newNode.setChildren(newChilds);
458: return newNode;
459:
460: }
461:
462: private void intro_post() {
463: ListOfGoal goals = mediator.getProof().getSubtreeGoals(
464: mediator.getProof().root());
465:
466: IteratorOfGoal it = goals.iterator();
467: while (it.hasNext()) {
468: Goal g = it.next();
469: Semisequent s = g.node().sequent().succedent();
470: IteratorOfConstrainedFormula cfmIt = s.iterator();
471:
472: while (cfmIt.hasNext()) {
473: ConstrainedFormula cfm = (ConstrainedFormula) cfmIt
474: .next();
475:
476: PosInOccurrence pio = new PosInOccurrence(cfm,
477: PosInTerm.TOP_LEVEL, false);
478:
479: SetOfTacletApp set = mediator.getTacletApplications(g,
480: "introduce_post_predicate", pio);
481:
482: // SetOfTacletApp set = m.getTacletApplications(g,
483: // "cut", pio);
484:
485: if (set.size() > 0) {
486: TacletApp tapp = set.iterator().next();
487: g.node().getNodeInfo().getVisualDebuggerState()
488: .getLabels().put(
489: pio,
490: new PCLabel(g.node().serialNr(),
491: false));
492: vd.extractInput(g.node(), pio);
493: vd.extractPrecondition(g.node(), pio);
494:
495: // VisualDebugger.getVisualDebugger().bpManager.clearSteps();
496: mediator.getInteractiveProver().applyInteractive(
497: tapp, g);
498:
499: }
500:
501: }
502: }
503: }
504:
505: private boolean isInfeasibleLeaf(ETNode n) {
506: return (n instanceof ETLeafNode && ((ETLeafNode) n).getState() == ETLeafNode.INFEASIBLE);
507:
508: }
509:
510: private boolean isLiteral(PosInOccurrence pio) {
511: Term f = pio.constrainedFormula().formula();
512: Operator op = f.op();
513:
514: if (this .modalityTopLevel(pio)) {
515: return true;
516: }
517: if (op == Op.AND
518: || op == Op.OR
519: || op == Op.IF_THEN_ELSE
520: || op == Op.IF_EX_THEN_ELSE
521: || op == Op.EQV
522: || op == Op.IMP
523: || op == Op.AND
524: || (op instanceof IUpdateOperator
525: /* && !containsJavaBlock(pio.constrainedFormula().formula() */)) {
526: return false;
527: }
528: final OpCollector col = new OpCollector();
529: f.execPostOrder(col);
530:
531: return !(col.contains(Op.IF_EX_THEN_ELSE) || col
532: .contains(Op.IF_THEN_ELSE));
533: }
534:
535: private boolean isNoInfeasibleLeaf(ETNode n) {
536: return (n instanceof ETLeafNode && ((ETLeafNode) n).getState() != ETLeafNode.INFEASIBLE);
537: }
538:
539: private ETNode mergeNodes(ETNode n1, ETNode n2, ETNode parent) {
540: // VisualDebugger.print("mergeNodes "+n1.print()+" "+n2.print());
541:
542: if (this .isInfeasibleLeaf(n1)) { // TODO wrong?
543: return n2.copy(parent);
544: } else if (this .isInfeasibleLeaf(n2)) {
545: return n1.copy(parent);
546: } else if (this .isInfeasibleLeaf(n2)) {
547: return n1.copy(parent);
548: }
549: if (this .isNoInfeasibleLeaf(n1)) { // TODO wrong?
550: final ETNode n = n2.copy(parent);
551: n.addITNodes(n1.getITNodes());
552: return n1;
553: } else if (this .isNoInfeasibleLeaf(n2)) {
554: final ETNode n = n1.copy(parent);
555: n.addITNodes(n2.getITNodes());
556: return n2;
557: }
558: if (n1.getChildren().length == 0) { // TODO wrong?
559: final ETNode n = n2.copy(parent);
560: n.addITNodes(n1.getITNodes());
561: return n;
562: } else if (n2.getChildren().length == 0) {
563: final ETNode n = n1.copy(parent);
564: n.addITNodes(n2.getITNodes());
565: return n;
566: }
567:
568: ETNode n = n1.copy(parent);
569: n.addITNodes(n2.getITNodes());
570:
571: n.setChildren(new LinkedList());
572:
573: if (n1.getChildren().length != n2.getChildren().length) {
574: VisualDebugger.print("Merging Nodes: Sth wrong ");
575: VisualDebugger.print("Node "
576: + n1.getITNodesArray()[0].getId() + " "
577: + n1.getITNodesArray()[0].getNode().sequent());
578: VisualDebugger.print("Node "
579: + n2.getITNodesArray()[0].getId() + " "
580: + n2.getITNodesArray()[0].getNode().sequent());
581: VisualDebugger.print("" + n1.getChildren().length);
582: VisualDebugger.print("" + n2.getChildren().length);
583: throw new RuntimeException(
584: "expected same number of childs in mergetree");
585: }
586:
587: for (int i = 0; i < n1.getChildren().length; i++) {
588: n.addChild(mergeNodes(n1.getChildren()[i],
589: n2.getChildren()[i], n));
590: }
591:
592: return n;
593: }
594:
595: public ETNode mergeTree(ETNode n, ETNode parent) {
596: VisualDebugger.print("mergeTree " + n.print());
597:
598: ETNode newNode = n.copy(parent);
599: ETNode[] childs = n.getChildren();
600:
601: LinkedList mergedChilds = new LinkedList();
602:
603: for (int i = 0; i < childs.length; i++) {
604: mergedChilds.add(mergeTree(childs[i], newNode));
605: }
606:
607: newNode.setChildren(mergedChilds);
608:
609: // ETNode[] mergedChildsArray= mergedChilds.toArray();
610:
611: if (mergedChilds.size() > 1) {
612:
613: ETNode m1 = (ETNode) mergedChilds.getFirst();
614: // if (this.maxmerge>0 && this.merged<this.maxmerge)
615: if (n.isNobc()) {
616:
617: // if (m1.getBc()==null){
618: VisualDebugger.print("Merge: "
619: + n.getITNodesArray()[0].getId());
620: for (int i = 1; i < mergedChilds.size(); i++) {
621:
622: m1 = mergeNodes(m1, (ETNode) mergedChilds.get(i),
623: parent);
624:
625: }
626: if (n.getBC() != null)
627: m1.appendBC(n.getBC());
628:
629: return m1;
630:
631: // if (n.getBc()!=null)
632: // m1.getChilds()[0].appendBc(n.getBc()); //TODO ??
633: // return m1.getChilds()[0];
634:
635: }
636:
637: }
638:
639: return newNode;
640: }
641:
642: /**
643: * FIXME reuse method in VisualDebugger
644: *
645: * @param pio
646: * @return
647: */
648: private boolean modalityTopLevel(PosInOccurrence pio) {
649: Term cf = pio.constrainedFormula().formula();
650: if (cf.arity() > 0) {
651: // CHECK: if --> while?
652: if (cf.op() instanceof QuanUpdateOperator) {
653: cf = ((QuanUpdateOperator) cf.op()).target(cf);
654: }
655: if (cf.op() instanceof Modality
656: || cf.op() == vd.getPostPredicate()) {
657: return true;
658: }
659: }
660: return false;
661: }
662:
663: // TODO allow all rules that are not of the form assume(non pc) fing(pc)
664: // TODO splitting rules in updates
665: private boolean onlyBCInvolvedInTacletApp(Node n, int newId) {
666: HashMapFromPosInOccurrenceToLabel labels = n.getNodeInfo()
667: .getVisualDebuggerState().getLabels();
668:
669: if (n.childrenCount() == 0) {
670: // System.out.println("BBBBBBBBB "+n.serialNr());
671: return false;
672:
673: }
674:
675: if (n.getAppliedRuleApp() instanceof TacletApp) {
676: TacletApp tapp = (TacletApp) n.getAppliedRuleApp();
677:
678: PosInOccurrence pioFocus = tapp.posInOccurrence()
679: .topLevel();
680: if (modalityTopLevel(pioFocus))
681: return false;
682:
683: if (!labels.containsKey(pioFocus)
684: || ((PCLabel) labels.get(pioFocus)).getId() != newId)
685: return false;
686:
687: if (tapp.ifFormulaInstantiations() != null)
688: for (IteratorOfIfFormulaInstantiation it = tapp
689: .ifFormulaInstantiations().iterator(); it
690: .hasNext();) {
691: final IfFormulaInstantiation next = it.next();
692: if (next instanceof IfFormulaInstSeq) {
693: IfFormulaInstSeq i = (IfFormulaInstSeq) next;
694: PosInOccurrence pio = new PosInOccurrence(i
695: .getConstrainedFormula(),
696: PosInTerm.TOP_LEVEL, i.inAntec());
697: if (!labels.containsKey(pio)
698: || ((PCLabel) labels.get(pio)).getId() != newId) {
699: return false;
700: }
701: }
702: }
703:
704: }
705:
706: return true;
707: }
708:
709: public void setListeners(LinkedList l) {
710: this .listeners = l;
711: }
712:
713: private void simplifyBC(ETNode n) {
714: ETNode[] children = n.getChildren();
715: if (children.length > 1)
716: for (int i = 0; i < children.length; i++) {
717: children[i].computeSimplifiedBC();
718: }
719:
720: n.removeRedundandITNodes();
721:
722: for (int i = 0; i < children.length; i++) {
723: simplifyBC(children[i]);
724: }
725: }
726:
727: private void startThread(final Runnable r) {
728: mediator.stopInterface(false);
729: Thread appThread = new Thread() {
730: public void run() {
731: try {
732: SwingUtilities.invokeAndWait(r);
733: // worker.start();
734: } catch (Exception e) {
735: e.printStackTrace();
736: }
737: mediator.startInterface(false);
738: mediator.setInteractive(true);
739: VisualDebugger.print("Finished creation of ET "
740: + Thread.currentThread());
741: }
742: };
743: appThread.start();
744: }
745: }
|