Skip to content

Commit

Permalink
black
Browse files Browse the repository at this point in the history
  • Loading branch information
Nfsaavedra committed Oct 16, 2023
1 parent fd1c0c1 commit b6aa575
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 7 deletions.
3 changes: 2 additions & 1 deletion coqlspclient/coq_exceptions.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,10 @@ def __init__(self, step: str):
def __str__(self):
return "The step {} is not valid.".format(self.step)


class InvalidFileException(Exception):
def __init__(self, file: str):
self.file: str = file

def __str__(self):
return "The file {} is not valid.".format(self.file)
return "The file {} is not valid.".format(self.file)
4 changes: 2 additions & 2 deletions coqlspclient/coq_file.py
Original file line number Diff line number Diff line change
Expand Up @@ -733,7 +733,7 @@ def add_step(
with open(self.path, "w") as f:
f.write(old_text)
raise InvalidStepException(step_text)

previous_steps.insert(step_index, self.steps[step_index])
for i, step in enumerate(previous_steps):
step.text, step.ast = self.steps[i].text, self.steps[i].ast
Expand Down Expand Up @@ -764,7 +764,7 @@ def current_goals(self) -> Optional[GoalAnswer]:
if end_pos != self.__last_end_pos:
self.__current_goals = self._goals(end_pos)
self.__last_end_pos = end_pos

return self.__current_goals

def save_vo(self):
Expand Down
14 changes: 10 additions & 4 deletions coqlspclient/proof_file.py
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ def __init__(
"""
super().__init__(file_path, library, timeout, workspace)
self.__aux_file = _AuxFile(timeout=self.timeout)

try:
self.context = _AuxFile.get_context(self.path, self.timeout)
self.__program_context: Dict[str, Tuple[Term, List]] = {}
Expand Down Expand Up @@ -456,14 +456,18 @@ def add_proof_step(super, i, goals=None):
break

for i, step in enumerate(proof.steps):
equal_steps = step.ast.range == self.steps[previous_step_index].ast.range
equal_steps = (
step.ast.range == self.steps[previous_step_index].ast.range
)
if step.ast.range >= self.steps[previous_step_index].ast.range:
if not equal_steps:
# If we did not find the exact step we have to calculate the goals
# Because the step may be outside of a proof
add_proof_step(super(), max(0, i - 1))
else:
add_proof_step(super(), min(i + 1, len(proof.steps)), step.goals)
add_proof_step(
super(), min(i + 1, len(proof.steps)), step.goals
)
break
else:
continue
Expand Down Expand Up @@ -491,7 +495,9 @@ def delete_step(self, step_index: int) -> None:
proof.steps[e].goals = self._goals
break
else:
raise NotImplementedError("Deleting steps outside of a proof is not implemented yet")
raise NotImplementedError(
"Deleting steps outside of a proof is not implemented yet"
)

def close(self):
"""Closes all resources used by this object."""
Expand Down

0 comments on commit b6aa575

Please sign in to comment.