001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.unicode;
017
018
019 /**
020 * Contains printing data for a formal proof line.
021 *
022 * @author Michael Meyling
023 */
024 public class ProofLineData {
025
026 /** Current Label of formal proof line. */
027 private String lineLabel;
028
029 /** String representation of formal proof line formula. */
030 private String[] formula;
031
032 /** String representation of formal proof line reason. */
033 private String[] reason;
034
035 /**
036 * Constructs empty container.
037 */
038 public ProofLineData() {
039 init();
040 }
041
042 /**
043 * Construct new proof line data.
044 *
045 * @param lineLabel Proof line label.
046 * @param formula Formula strings.
047 * @param reason Reason strings.
048 */
049 public ProofLineData(final String lineLabel, final String[] formula, final String[] reason) {
050 this.lineLabel = lineLabel;
051 this.formula = formula;
052 this.reason = reason;
053 }
054
055 /**
056 * Copy constructor.
057 *
058 * @param lineData Existing object.
059 */
060 public ProofLineData(final ProofLineData lineData) {
061 this.lineLabel = lineData.lineLabel;
062 this.formula = new String[lineData.formula.length];
063 System.arraycopy(lineData.formula, 0, this.formula, 0, lineData.formula.length);
064 this.reason = new String[lineData.reason.length];
065 System.arraycopy(lineData.reason, 0, this.reason, 0, lineData.reason.length);
066 }
067
068 /**
069 * Empty data.
070 */
071 public void init() {
072 this.lineLabel = "";
073 this.formula = new String[0];
074 this.reason = new String[0];
075 }
076
077 /**
078 * Exists formula data or reason data?
079 *
080 * @return Is there any reason or formula data?
081 */
082 public boolean containsData() {
083 return (0 != lines());
084 }
085
086 /**
087 * How many lines do we have? This is maximum of formula lines and reason lines.
088 *
089 * @return Number of lines.
090 */
091 public int lines() {
092 return Math.max(getFormula().length, getReason().length);
093 }
094
095 /**
096 * Get label for proof line.
097 *
098 * @return Proof line label.
099 */
100 public String getLineLabel() {
101 return lineLabel;
102 }
103
104 /**
105 * Set label for proof line.
106 *
107 * @param lineLabel Proof line label.
108 */
109 public void setLineLabel(final String lineLabel) {
110 this.lineLabel = lineLabel;
111 }
112
113 /**
114 * Get proof line formula.
115 *
116 * @return Proof line formula.
117 */
118 public String[] getFormula() {
119 return formula;
120 }
121
122 /**
123 * Set proof line formula.
124 *
125 * @param formula Proof line formula.
126 */
127 public void setFormula(final String[] formula) {
128 this.formula = formula;
129 }
130
131 /**
132 * Get derive reason for proof line. Already formatted in several lines.
133 *
134 * @return Reason for getting this proof line.
135 */
136 public String[] getReason() {
137 return reason;
138 }
139
140 /**
141 * Set derive reason for proof line.
142 *
143 * @param reason Reason for getting this proof line. Must be already formatted in serveral
144 * lines.
145 */
146 public void setReason(final String[] reason) {
147 this.reason = reason;
148 }
149
150 }
|