1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.xml.handler.module;
17
18 import org.qedeq.kernel.se.base.module.Reason;
19 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
20 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
21 import org.qedeq.kernel.xml.common.XmlSyntaxException;
22 import org.qedeq.kernel.xml.handler.common.AbstractSimpleHandler;
23 import org.qedeq.kernel.xml.handler.common.SimpleAttributes;
24
25
26
27
28
29
30
31 public class FormalProofLineListHandler extends AbstractSimpleHandler {
32
33
34 private FormalProofLineListVo list;
35
36
37 private final FormulaHandler formulaHandler;
38
39
40 private final ModusPonensHandler modusPonensHandler;
41
42
43 private final AddHandler addHandler;
44
45
46 private final RenameHandler renameHandler;
47
48
49 private final SubstPredvarHandler substPredvarHandler;
50
51
52 private final SubstFreevarHandler substFreevarHandler;
53
54
55 private final SubstFuncvarHandler substFuncvarHandler;
56
57
58 private final ExistentialHandler existentialHandler;
59
60
61 private final UniversalHandler universalHandler;
62
63
64 private final ConditionalProofHandler conditionalProofHandler;
65
66
67 private String label;
68
69
70 private Reason reason;
71
72
73
74
75
76
77
78 public FormalProofLineListHandler(final AbstractSimpleHandler handler) {
79 super(handler, "LINES");
80 formulaHandler = new FormulaHandler(this);
81 modusPonensHandler = new ModusPonensHandler(this);
82 addHandler = new AddHandler(this);
83 substPredvarHandler = new SubstPredvarHandler(this);
84 renameHandler = new RenameHandler(this);
85 substFreevarHandler = new SubstFreevarHandler(this);
86 substFuncvarHandler = new SubstFuncvarHandler(this);
87 existentialHandler = new ExistentialHandler(this);
88 universalHandler = new UniversalHandler(this);
89 conditionalProofHandler = new ConditionalProofHandler(this);
90 }
91
92 public final void init() {
93 list = null;
94 reason = null;
95 label = null;
96 }
97
98
99
100
101
102
103 public final FormalProofLineListVo getFormalProofLineList() {
104 return list;
105 }
106
107 public final void startElement(final String name, final SimpleAttributes attributes)
108 throws XmlSyntaxException {
109 if (getStartTag().equals(name)) {
110 list = new FormalProofLineListVo();
111 } else if ("L".equals(name)) {
112 label = attributes.getString("label");
113 reason = null;
114 } else if (formulaHandler.getStartTag().equals(name)) {
115 changeHandler(formulaHandler, name, attributes);
116 } else if (modusPonensHandler.getStartTag().equals(name)) {
117 changeHandler(modusPonensHandler, name, attributes);
118 } else if (addHandler.getStartTag().equals(name)) {
119 changeHandler(addHandler, name, attributes);
120 } else if (substPredvarHandler.getStartTag().equals(name)) {
121 changeHandler(substPredvarHandler, name, attributes);
122 } else if (renameHandler.getStartTag().equals(name)) {
123 changeHandler(renameHandler, name, attributes);
124 } else if (substFreevarHandler.getStartTag().equals(name)) {
125 changeHandler(substFreevarHandler, name, attributes);
126 } else if (substFuncvarHandler.getStartTag().equals(name)) {
127 changeHandler(substFuncvarHandler, name, attributes);
128 } else if (existentialHandler.getStartTag().equals(name)) {
129 changeHandler(existentialHandler, name, attributes);
130 } else if (universalHandler.getStartTag().equals(name)) {
131 changeHandler(universalHandler, name, attributes);
132 } else if (conditionalProofHandler.getStartTag().equals(name)) {
133 changeHandler(conditionalProofHandler, name, attributes);
134 } else {
135 throw XmlSyntaxException.createUnexpectedTagException(name);
136 }
137 }
138
139 public final void endElement(final String name) throws XmlSyntaxException {
140 if (getStartTag().equals(name)) {
141
142 } else if (formulaHandler.getStartTag().equals(name)) {
143
144 } else if ("L".equals(name)) {
145 list.add(new FormalProofLineVo(label, formulaHandler.getFormula(), reason));
146 } else if (modusPonensHandler.getStartTag().equals(name)) {
147 reason = modusPonensHandler.getModusPonensVo();
148 } else if (addHandler.getStartTag().equals(name)) {
149 reason = addHandler.getAddVo();
150 } else if (substPredvarHandler.getStartTag().equals(name)) {
151 reason = substPredvarHandler.getSubstPredVo();
152 } else if (renameHandler.getStartTag().equals(name)) {
153 reason = renameHandler.getRenameVo();
154 } else if (substFreevarHandler.getStartTag().equals(name)) {
155 reason = substFreevarHandler.getSubstFreeVo();
156 } else if (substFuncvarHandler.getStartTag().equals(name)) {
157 reason = substFuncvarHandler.getSubstFuncVo();
158 } else if (existentialHandler.getStartTag().equals(name)) {
159 reason = existentialHandler.getExistentialVo();
160 } else if (universalHandler.getStartTag().equals(name)) {
161 reason = universalHandler.getUniversalVo();
162 } else if (conditionalProofHandler.getStartTag().equals(name)) {
163 list.add(conditionalProofHandler.getConditionalProofVo());
164 } else {
165 throw XmlSyntaxException.createUnexpectedTagException(name);
166 }
167 }
168 }