Small fixes

coqlspclient/coq_file.py

@@ -226,7 +226,7 @@ def __slice_line(
 
         # For where-notations, the character count does not include the closing
         # parenthesis when present.
-        if stop is not None and chr(line[stop]) == ")":
+        if stop is not None and len(line) > stop and chr(line[stop]) == ")":
             stop += 1
         return line[start:stop].decode()
 
@@ -704,11 +704,14 @@ def add_step(
             previous_step = self.steps[previous_step_index]
             end_line = previous_step.ast.range.end.line
             end_char = previous_step.ast.range.end.character
-            # FIXME use slice line
             lines[end_line] = (
-                lines[end_line][: end_char + 1]
+                self.__slice_line(
+                    lines[end_line], stop=end_char, range=previous_step.ast.range
+                )
                 + step_text
-                + lines[end_line][end_char + 1 :]
+                + self.__slice_line(
+                    lines[end_line], start=end_char + 1, range=previous_step.ast.range
+                )
             )
             text = "\n".join(lines)
             f.write(text)

coqlspclient/proof_file.py

@@ -176,7 +176,7 @@ def get_context(file_path: str, timeout: int):
                 # FIXME: we ignore the usage of Local from imported files to
                 # simplify the implementation. However, they can be used:
                 # https://coq.inria.fr/refman/language/core/modules.html?highlight=local#coq:attr.local
-                for term in aux_context.terms.keys():
+                for term in list(aux_context.terms.keys()):
                     if aux_context.terms[term].text.startswith("Local"):
                         aux_context.terms.pop(term)
                 context.update(**vars(aux_context))
@@ -189,10 +189,6 @@ class ProofFile(CoqFile):
     ProofState will run the file from its current state, i.e., if the file
     has finished its execution, ProofState won't return anything. The Coq file
     will be fully checked after the creation of a ProofState.
-
-    FIXME
-    Attributes:
-        coq_file (CoqFile): Coq file to interact with
     """
 
     def __init__(
@@ -216,7 +212,8 @@ def __init__(
         self.__aux_file = _AuxFile(timeout=self.timeout)
 
         try:
-            self.context = _AuxFile.get_context(self.path, self.timeout)
+            # We need to update the context already defined in the CoqFile
+            self.context.update(_AuxFile.get_context(self.path, self.timeout).terms)
             self.__program_context: Dict[str, Tuple[Term, List]] = {}
             self.__proofs = self.__get_proofs()
         except Exception as e: