1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.se.dto.module; |
17 | |
18 | import org.qedeq.base.utility.EqualsUtility; |
19 | import org.qedeq.kernel.se.base.module.FormalProof; |
20 | import org.qedeq.kernel.se.base.module.FormalProofLineList; |
21 | import org.qedeq.kernel.se.base.module.LatexList; |
22 | |
23 | |
24 | /** |
25 | * Contains a formal proof for a proposition. |
26 | * |
27 | * @author Michael Meyling |
28 | */ |
29 | public class FormalProofVo implements FormalProof { |
30 | |
31 | /** Preceding LaTeX text. This text comes before the formal proof. */ |
32 | private LatexList precedingText; |
33 | |
34 | /** Proof lines. */ |
35 | private FormalProofLineList formalProofLineList; |
36 | |
37 | /** Succeeding LaTeX text. This text comes after the formal proof. */ |
38 | private LatexList succeedingText; |
39 | |
40 | /** |
41 | * Constructs an empty proof. |
42 | */ |
43 | public FormalProofVo() { |
44 | // nothing to do |
45 | } |
46 | |
47 | /** |
48 | * Constructs a proof. |
49 | * |
50 | * @param formalProofLines The proof lines. |
51 | */ |
52 | public FormalProofVo(final FormalProofLineList formalProofLines) { |
53 | this.formalProofLineList = formalProofLines; |
54 | } |
55 | |
56 | /** |
57 | * Set preceding LaTeX text. This text comes before a formal proof. |
58 | * |
59 | * @param precedingText Preceding LaTeX text. |
60 | */ |
61 | public final void setPrecedingText(final LatexListVo precedingText) { |
62 | this.precedingText = precedingText; |
63 | } |
64 | |
65 | public final LatexList getPrecedingText() { |
66 | return precedingText; |
67 | } |
68 | |
69 | /** |
70 | * Set proof lines for formal proof. |
71 | * |
72 | * @param formalProofLines The proof lines. |
73 | */ |
74 | public final void setFormalProofLineList(final FormalProofLineList formalProofLines) { |
75 | this.formalProofLineList = formalProofLines; |
76 | } |
77 | |
78 | public final FormalProofLineList getFormalProofLineList() { |
79 | return formalProofLineList; |
80 | } |
81 | |
82 | /** |
83 | * Set succeeding LaTeX text. This text comes after a formal proof. |
84 | * |
85 | * @param succeedingText Succeeding LaTeX text. |
86 | */ |
87 | public final void setSucceedingText(final LatexListVo succeedingText) { |
88 | this.succeedingText = succeedingText; |
89 | } |
90 | |
91 | public final LatexList getSucceedingText() { |
92 | return succeedingText; |
93 | } |
94 | |
95 | public boolean equals(final Object obj) { |
96 | if (!(obj instanceof FormalProofVo)) { |
97 | return false; |
98 | } |
99 | final FormalProofVo other = (FormalProofVo) obj; |
100 | return EqualsUtility.equals(getPrecedingText(), other.getPrecedingText()) |
101 | && EqualsUtility.equals(getFormalProofLineList(), other.getFormalProofLineList()) |
102 | && EqualsUtility.equals(getSucceedingText(), other.getSucceedingText()); |
103 | } |
104 | |
105 | public int hashCode() { |
106 | return (getPrecedingText() != null ? getPrecedingText().hashCode() : 0) |
107 | ^ (getFormalProofLineList() != null ? 2 ^ getFormalProofLineList().hashCode() : 0) |
108 | ^ (getSucceedingText() != null ? 3 ^ getSucceedingText().hashCode() : 0); |
109 | } |
110 | |
111 | public String toString() { |
112 | final StringBuffer result = new StringBuffer(); |
113 | if (getPrecedingText() != null) { |
114 | result.append(getPrecedingText()); |
115 | } |
116 | if (getFormalProofLineList() != null) { |
117 | result.append("Formal Proof: " + getFormalProofLineList()); |
118 | } |
119 | if (getSucceedingText() != null) { |
120 | result.append(getSucceedingText()); |
121 | } |
122 | return result.toString(); |
123 | } |
124 | |
125 | |
126 | } |