Fix the indenting of imports in the printer

src/main/scala/lisa/kernel/Printer.scala

@@ -180,6 +180,17 @@ object Printer {
         Seq(prettyFormulas(sequent.left), "⊢", prettyFormulas(sequent.right)).filter(_.nonEmpty).mkString(spaceSeparator(compact))
     }
 
+    /**
+     * Returns a string representation of the line number in a proof.
+     * Example output:
+     * <pre>
+     * 0:2:1
+     * </pre>
+     * @param line the line number
+     * @return the string representation of this line number
+     */
+    def prettyLineNumber(line: Seq[Int]): String = line.mkString(":")
+
     /**
      * Returns a string representation of this proof.
      * @param proof the proof
@@ -187,14 +198,13 @@ object Printer {
      *                  (`->`) as an error. The proof is considered to be valid by default
      * @return a string where each indented line corresponds to a step in the proof
      */
-    def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof): String = {
-        def computeMaxNumbering(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
-            val resultWithCurrent = result.updated(level, Math.max(proof.steps.size - 1, result(level)))
-            proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumbering(sp.sp, level + 1, if(acc.size <= level + 1) acc :+ 0 else acc))
+    def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof, forceDisplaySubproofs: Boolean = false): String = {
+        def computeMaxNumberingLengths(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
+          val resultWithCurrent = result.updated(level, (Seq((proof.steps.size - 1).toString.length, result(level)) ++ (if(proof.imports.nonEmpty) Seq((-proof.imports.size).toString.length) else Seq.empty)).max)
+          proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumberingLengths(sp.sp, level + 1, if(acc.size <= level + 1) acc :+ 0 else acc))
         }
-        val maxNumbering = computeMaxNumbering(proof, 0, IndexedSeq(0)) // The maximum value for each number column
-        val maxNumberingLengths = maxNumbering.map(_.toString.length)
-        val maxLevel = maxNumbering.size - 1
+        val maxNumberingLengths = computeMaxNumberingLengths(proof, 0, IndexedSeq(0)) // The maximum value for each number column
+        val maxLevel = maxNumberingLengths.size - 1
 
         def leftPadSpaces(v: Any, n: Int): String = {
             val s = String.valueOf(v)
@@ -239,7 +249,8 @@ object Printer {
                         prettySequent(step.bot)
                     )
                 step match {
-                    case sp @ SCSubproof(_, _, true) => pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if(i == 0) topMostIndices else IndexedSeq.empty) :+ i)
+                    case sp @ SCSubproof(_, _, display) if display || forceDisplaySubproofs =>
+                        pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if(i == 0) topMostIndices else IndexedSeq.empty) :+ i)
                     case other =>
                         val line = other match {
                             case Rewrite(_, t1) => pretty("Rewrite", t1)
@@ -268,7 +279,7 @@ object Printer {
                             case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
                             case InstFunSchema(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
                             case InstPredSchema(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
-                            case SCSubproof(_, _, false) => pretty("SCSubproof (hidden)")
+                            case SCSubproof(_, _, false) => pretty("Subproof (hidden)")
                             case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
                         }
                         Seq(line)
@@ -288,7 +299,7 @@ object Printer {
                 full.mkString(" ")
         }.mkString("\n") + (judgement match {
             case SCValidProof => ""
-            case SCInvalidProof(path, message) => s"\nProof checker has reported error at line ${path.mkString(".")}: $message"
+            case SCInvalidProof(path, message) => s"\nProof checker has reported an error at line ${path.mkString(".")}: $message"
         })
     }