Fix proof using parse error

See ProofGeneral/PG#715 for a description of the same issue in Proof General
UCSD-PL · Nov 8, 2023 · d9becac · d9becac
1 parent 0f0a82e
commit d9becac
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/add_proof_using.py b/src/add_proof_using.py
@@ -61,6 +61,8 @@ def add_proof_using_with_running_instance(coq: coq_serapy.CoqAgent, commands: It
                                            cur_proof_commands[0].strip())
                 if proof_cmd_match:
                     proof_cmd_suffix = proof_cmd_match.group(1)
+                    if len(suggested_deps.strip().split()) > 1 and proof_cmd_suffix.strip() != "":
+                        suggested_deps = "(" + suggested_deps + ")"
                     cur_proof_commands[0] = "Proof using " + suggested_deps + proof_cmd_suffix + ".\n"
                 else:
                     cur_proof_commands.insert(0, "Proof using " + suggested_deps + ".\n")