From 0c50c6d2b21f90a487b562eebadb8dd715a55257 Mon Sep 17 00:00:00 2001
From: Abhishek Chugh <achugh89@gmail.com>
Date: Tue, 14 Jul 2020 10:21:31 +0530
Subject: [PATCH] Make renumbering of proof derivation steps optional

Sophize is using this function to get proofs in a format that can imported. Thus, renumbering  needs to be avoided for this case.
---
 src/mmj/pa/ProofAsst.java        |  2 +-
 src/mmj/verify/VerifyProofs.java | 10 ++++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/mmj/pa/ProofAsst.java b/src/mmj/pa/ProofAsst.java
index fe112cf3..07747760 100644
--- a/src/mmj/pa/ProofAsst.java
+++ b/src/mmj/pa/ProofAsst.java
@@ -1667,7 +1667,7 @@ private ProofWorksheet getExportedProofWorksheet(final Theorem theorem,
         try {
             proofDerivationStepList = verifyProofs.getProofDerivationSteps(
                 theorem, exportFormatUnified, hypsOrder,
-                getProvableLogicStmtTyp());
+                getProvableLogicStmtTyp(), true);
 
             proofWorksheet = new ProofWorksheet(theorem,
                 proofDerivationStepList, deriveFormulas, proofAsstPreferences,
diff --git a/src/mmj/verify/VerifyProofs.java b/src/mmj/verify/VerifyProofs.java
index c2f1b26f..1187a935 100644
--- a/src/mmj/verify/VerifyProofs.java
+++ b/src/mmj/verify/VerifyProofs.java
@@ -472,20 +472,22 @@ public VerifyException verifyDerivStepDjVars(final String derivStepNbr,
      */
     public List<ProofDerivationStepEntry> getProofDerivationSteps(
         final Theorem theorem, final boolean exportFormatUnified,
-        final HypsOrder hypsOrder, final Cnst provableLogicStmtTyp)
+        final HypsOrder hypsOrder, final Cnst provableLogicStmtTyp,
+        final boolean renumberSteps)
         throws VerifyException
     {
 
         final LogHyp[] theoremLogHypArray = theorem.getLogHypArray();
         final List<ProofDerivationStepEntry> derivStepList = new ArrayList<>(
             theoremLogHypArray.length);
-
-        int renumberStep = PaConstants.PROOF_STEP_RENUMBER_START;
+        
+        int renumberStep = renumberSteps ? PaConstants.PROOF_STEP_RENUMBER_START : 0;
+        int renumberInterval =  renumberSteps ? PaConstants.PROOF_STEP_RENUMBER_INTERVAL : 1;
         for (final LogHyp element : theoremLogHypArray) {
             final ProofDerivationStepEntry e = new ProofDerivationStepEntry();
             e.isHyp = true;
             e.step = Integer.toString(renumberStep);
-            renumberStep += PaConstants.PROOF_STEP_RENUMBER_INTERVAL;
+            renumberStep += renumberInterval;
             e.hypStep = new String[0];
             e.refLabel = element.getLabel();
             e.formula = element.getFormula();