01: package de.uka.ilkd.key.ocl.gf;
02:
03: import java.util.Vector;
04:
05: /**
06: * Asks GF the Vector of RefinementMenu entries.
07: *
08: * This class can be reused.
09: * @author daniels
10: */
11: class RefinementMenuCollector extends AbstractProber {
12: /**
13: * here the result of this run is saved
14: */
15: Vector refinementMenuContent = null;
16:
17: /**
18: * Standard fill-in-the-parameters constructor
19: * @param gfCapsule The reader/writer to GF
20: */
21: public RefinementMenuCollector(GfCapsule gfCapsule) {
22: super (gfCapsule);
23: }
24:
25: /**
26: * Asks GF (the same GF as the one editor has) to execute a command
27: * and returns the read refinement menu that is offered then.
28: * Uses the readRefinementMenu method from GFEditor2 which does not
29: * change any global variable besides GF itself. So that is safe.
30: *
31: * Note: This method does not do undo automatically, since it is
32: * intended to run several times in a row, so the u should be part of
33: * next command.
34: * @param command The command that is sent to GF. Should contain a mp
35: * to make sure that the command at the right position in the AST
36: * is read
37: * @return a Vector of StringTuple like readRefinementMenu does it.
38: */
39: public Vector readRefinementMenu(String command) {
40: send(command);
41: readGfedit();
42: return this .refinementMenuContent;
43: }
44:
45: /**
46: * parses the refinement menu part and stores it in this.refinementMenuContent
47: */
48: protected void readMenu() {
49: this.refinementMenuContent = gfCapsule.readRefinementMenu();
50: }
51:
52: }
|