Commit 265fdf76 authored by Sarah Grebing's avatar Sarah Grebing

fixed instantiate commadn in key sources

parent 1bfc2b02
Pipeline #18582 failed with stages
in 0 seconds
......@@ -56,9 +56,7 @@ public class Execute {
//pa.getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
Interpreter<KeyData> inter = interpreterBuilder.build();
KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
inter.newState(new GoalNode<>(null, keyData, keyData.isClosedNode()));
Interpreter<KeyData> inter = interpreterBuilder.startState().build();
inter.interpret(ast.get(0));
return inter;
} catch (ProblemLoaderException | IOException e) {
......
......@@ -89,4 +89,13 @@ public class ExecuteTest {
}
@Test
public void testInstantiate() throws IOException, ParseException, ParserException {
Execute exec = create("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/bigIntProof/compareMagnitude_openCases.key.proof",
"-s", "/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/bigIntProof/instAll.kps");
Interpreter<KeyData> i = exec.run();
State<KeyData> currentState = i.getCurrentState();
System.out.println(currentState);
}
}
\ No newline at end of file
......@@ -205,6 +205,8 @@ public class TacletContextMenu extends ContextMenu {
toAdd.addAll(noFindTaclets);
}
/*toAdd=toAdd.stream().filter(tapp->{
try{
return tapp.isExecutable(goal.proof().getServices());
......
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