Commit 33395854 authored by Sarah Grebing's avatar Sarah Grebing

Bugfix: TacletMenu rule are now filtered

parent eb319d08
Pipeline #16887 failed with stages
in 2 minutes and 41 seconds
......@@ -974,8 +974,10 @@ public class DebuggerMain implements Initializable {
@FXML
public void interactiveMode(ActionEvent actionEvent) {
if (btnInteractiveMode.isSelected()) {
if (!btnInteractiveMode.isSelected()) {
interactiveModeController.setActivated(true);
//SaG: this needs to be set to filter inapplicable rules
this.getFacade().getEnvironment().getProofControl().setMinimizeInteraction(true);
interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
} else {
interactiveModeController.stop();
......
......@@ -62,6 +62,7 @@ public class InteractiveModeController {
this.scriptArea = scriptController.newScript();
this.model = model;
}
public void stop() {
......
......@@ -103,6 +103,7 @@ public class TacletContextMenu extends ContextMenu {
comp = new TacletAppComparator();
insertHiddenController.initViewController(getMainApp(), getContext());
*/
if (pos == null)
throw new IllegalArgumentException(
"Argument pos must not be null.");
......@@ -112,10 +113,12 @@ public class TacletContextMenu extends ContextMenu {
occ = pos.getPosInOccurrence();
//MediatorProofControl c = new MediatorProofControl(new DefaultAbstractMediatorUserInterfaceControlAdapter());
ProofControl c = DebuggerMain.FACADE.getEnvironment().getUi().getProofControl();
final ImmutableList<BuiltInRule> builtInRules = c.getBuiltInRule(goal, occ);
ImmutableList<TacletApp> findTaclet = c.getFindTaclet(goal, occ);
createTacletMenu(
removeRewrites(c.getFindTaclet(goal, occ))
removeRewrites(findTaclet)
.prepend(c.getRewriteTaclet(goal, occ)),
c.getNoFindTaclet(goal), builtInRules);
......
......@@ -3,7 +3,7 @@
script test1234(){
impRight;
auto;
//auto;
}
script test23(){
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment