package start;

import model.Proof;

import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.HashMap;

public class ExportLatex {
    private static final HashMap<Character, String> unicodeToLaTeX;

    static {
        unicodeToLaTeX = new HashMap<Character, String>();
        unicodeToLaTeX.put('∧', "\\land ");
        unicodeToLaTeX.put('∨', "\\lor ");
        unicodeToLaTeX.put('¬', "\\neg ");
        unicodeToLaTeX.put('→', "\\to ");
        unicodeToLaTeX.put('∃', "\\exists ");
        unicodeToLaTeX.put('∀', "\\forall ");
        unicodeToLaTeX.put('⊥', "\\bot ");
        unicodeToLaTeX.put('₀', "_0");
        unicodeToLaTeX.put('₁', "_1");
        unicodeToLaTeX.put('₂', "_2");
        unicodeToLaTeX.put('₃', "_3");
        unicodeToLaTeX.put('₄', "_4");
        unicodeToLaTeX.put('₅', "_5");
        unicodeToLaTeX.put('₆', "_6");
        unicodeToLaTeX.put('₇', "_7");
        unicodeToLaTeX.put('₈', "_8");
        unicodeToLaTeX.put('₉', "_9");
    }

    public static void export(Proof proof, String file) throws IOException {
        String[] lines = proof.getProofString().split("\\r?\\n");
        String output = "% For use with https://www.ctan.org/pkg/logicproof\n";
        output += "% Note that ending a box in a box is not valid and will not give the desired results.\n";
        int maxDepth = -1;
        int curDepth = 1;
        for (String line : lines) {
            String[] info = line.split("::");
            int depth = Integer.parseInt(info[0]);
            if (maxDepth < depth) {
                maxDepth = depth;
            }
            if (curDepth == depth && Integer.parseInt(info[4])==1) { // Edge case same depth box after box
                // Need to remove backslashes and both end and start a new environment
                output = trimEnd(output);
                output += "\\end{subproof}\n";
                output += "\\begin{subproof}\n";

            } else if (curDepth < depth) { // Regular depth increase
                output += "\\begin{subproof}\n";
                ++curDepth;
            } else while (curDepth > depth) {
                output = trimEnd(output);
                output += "\\end{subproof}\n";
                --curDepth;
            }
            output += replaceAllUnicode(info[1]).replaceAll("null","");
            // Everything before the &, is in a math environment.
            output += "&";
            // We surround the crucial part in $ in the rule and references.
            output += replaceAllUnicode(info[2]).replaceAll(
                    "(\\\\land |\\\\lor |\\\\to |\\\\forall |\\\\exists |\\\\bot |\\\\neg )(i|e)(_\\{(\\d)\\})?","\\$$1\\\\mathrm\\{$2\\}$3\\$").replaceAll("null", "");
            output += "\\\\\n";

        }
        while (curDepth > 1) {
            output = trimEnd(output);
            output += "\\end{subproof}\n";
            --curDepth;
        }
        output = trimEnd(output);
        output = "\\begin{logicproof}{" + maxDepth + "}\n" + output + "\\end{logicproof}";
        Files.write(Paths.get(file), output.getBytes());
    }

    private static String replaceAllUnicode(String s) {
        String ret = "";
        for (int i = 0; i < s.length(); i++) {
            String next = unicodeToLaTeX.getOrDefault(s.charAt(i), null);
            if (next == null)
                ret += s.charAt(i);
            else
                ret += next;
        }
        return ret;
    }

    private static String trimEnd(String s) {
        if (s.endsWith("\\\\\n")) // Might need \r for cross platform
            return s.substring(0, s.length() - 3) + '\n';
        return s;

    }
}

@@ -649,17 +649,16 @@
 t('%E2%82%80', %22
-_
 0%22);%0A   
@@ -687,17 +687,16 @@
 t('%E2%82%81', %22
-_
 1%22);%0A   
@@ -725,17 +725,16 @@
 t('%E2%82%82', %22
-_
 2%22);%0A   
@@ -763,17 +763,16 @@
 t('%E2%82%83', %22
-_
 3%22);%0A   
@@ -801,17 +801,16 @@
 t('%E2%82%84', %22
-_
 4%22);%0A   
@@ -839,17 +839,16 @@
 t('%E2%82%85', %22
-_
 5%22);%0A   
@@ -877,17 +877,16 @@
 t('%E2%82%86', %22
-_
 6%22);%0A   
@@ -915,17 +915,16 @@
 t('%E2%82%87', %22
-_
 7%22);%0A   
@@ -953,17 +953,16 @@
 t('%E2%82%88', %22
-_
 8%22);%0A   
@@ -990,14 +990,13 @@
 ut('
-%E2%82%89
+%E2%82%88
 ', %22
-_
 9%22);
@@ -2275,32 +2275,44 @@
       output += 
+attachIndex(
 replaceAllUnicod
@@ -2321,16 +2321,17 @@
 info%5B1%5D)
+)
 .replace
@@ -2341,16 +2341,17 @@
 (%22null%22,
+ 
 %22%22);%0A   
@@ -3117,32 +3117,139 @@
 ytes());%0A    %7D%0A%0A
+    private static String attachIndex(String s) %7B%0A        return s.replaceAll(%22(%5C%5Cd+)%22,%22_%5C%5C%7B$1%5C%5C%7D%22);%0A    %7D%0A
     private stat

Support for numbered items added for export latex