1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
|
|
18 |
|
package org.qedeq.kernel.bo.service.latex; |
19 |
|
|
20 |
|
import java.io.File; |
21 |
|
import java.io.FileOutputStream; |
22 |
|
import java.io.IOException; |
23 |
|
import java.io.OutputStream; |
24 |
|
import java.io.PrintStream; |
25 |
|
|
26 |
|
import org.qedeq.base.trace.Trace; |
27 |
|
import org.qedeq.base.utility.StringUtility; |
28 |
|
import org.qedeq.kernel.base.list.Element; |
29 |
|
import org.qedeq.kernel.base.list.ElementList; |
30 |
|
import org.qedeq.kernel.base.module.Axiom; |
31 |
|
import org.qedeq.kernel.base.module.Chapter; |
32 |
|
import org.qedeq.kernel.base.module.ChapterList; |
33 |
|
import org.qedeq.kernel.base.module.FunctionDefinition; |
34 |
|
import org.qedeq.kernel.base.module.Latex; |
35 |
|
import org.qedeq.kernel.base.module.LatexList; |
36 |
|
import org.qedeq.kernel.base.module.LiteratureItem; |
37 |
|
import org.qedeq.kernel.base.module.LiteratureItemList; |
38 |
|
import org.qedeq.kernel.base.module.Node; |
39 |
|
import org.qedeq.kernel.base.module.NodeType; |
40 |
|
import org.qedeq.kernel.base.module.PredicateDefinition; |
41 |
|
import org.qedeq.kernel.base.module.Proposition; |
42 |
|
import org.qedeq.kernel.base.module.Rule; |
43 |
|
import org.qedeq.kernel.base.module.Section; |
44 |
|
import org.qedeq.kernel.base.module.SectionList; |
45 |
|
import org.qedeq.kernel.base.module.Subsection; |
46 |
|
import org.qedeq.kernel.base.module.SubsectionList; |
47 |
|
import org.qedeq.kernel.base.module.SubsectionType; |
48 |
|
import org.qedeq.kernel.base.module.VariableList; |
49 |
|
import org.qedeq.kernel.bo.QedeqBo; |
50 |
|
|
51 |
|
|
52 |
|
|
53 |
|
|
54 |
|
|
55 |
|
|
56 |
|
|
57 |
|
|
58 |
|
|
59 |
|
|
60 |
|
|
61 |
|
|
62 |
|
@version |
63 |
|
@author |
64 |
|
|
|
|
| 0% |
Uncovered Elements: 304 (304) |
Complexity: 60 |
Complexity Density: 0,33 |
|
65 |
|
public class Qedeq2Wiki { |
66 |
|
|
67 |
|
|
68 |
|
private static final Class CLASS = Qedeq2Wiki.class; |
69 |
|
|
70 |
|
|
71 |
|
private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz"; |
72 |
|
|
73 |
|
|
74 |
|
private final QedeqBo prop; |
75 |
|
|
76 |
|
|
77 |
|
private PrintStream printer; |
78 |
|
|
79 |
|
|
80 |
|
private String language; |
81 |
|
|
82 |
|
@link |
83 |
|
private final Element2Latex elementConverter; |
84 |
|
|
85 |
|
|
86 |
|
private File outputDirectory; |
87 |
|
|
88 |
|
|
89 |
|
|
90 |
|
|
91 |
|
@param |
92 |
|
|
|
|
| 0% |
Uncovered Elements: 4 (4) |
Complexity: 1 |
Complexity Density: 0,5 |
|
93 |
0
|
public Qedeq2Wiki(final QedeqBo prop) {... |
94 |
0
|
this.prop = prop; |
95 |
0
|
this.elementConverter = new Element2Latex((prop.hasLoadedRequiredModules() |
96 |
|
? prop.getRequiredModules() : null)); |
97 |
|
} |
98 |
|
|
99 |
|
|
100 |
|
|
101 |
|
|
102 |
|
@param |
103 |
|
@param |
104 |
|
|
105 |
|
@param |
106 |
|
@throws |
107 |
|
|
|
|
| 0% |
Uncovered Elements: 12 (12) |
Complexity: 3 |
Complexity Density: 0,38 |
|
108 |
0
|
public final synchronized void printWiki(final String language, final String level,... |
109 |
|
final File outputDirectory) throws IOException { |
110 |
0
|
if (language == null) { |
111 |
0
|
this.language = "en"; |
112 |
|
} else { |
113 |
0
|
this.language = language; |
114 |
|
} |
115 |
0
|
this.outputDirectory = outputDirectory; |
116 |
0
|
printQedeqChapters(); |
117 |
0
|
printQedeqBibliography(); |
118 |
0
|
if (printer.checkError()) { |
119 |
0
|
throw new IOException("TODO mime: better use another OutputStream"); |
120 |
|
} |
121 |
|
} |
122 |
|
|
123 |
|
|
124 |
|
|
125 |
|
|
126 |
|
@throws |
127 |
|
|
|
|
| 0% |
Uncovered Elements: 30 (30) |
Complexity: 6 |
Complexity Density: 0,27 |
|
128 |
0
|
private void printQedeqChapters() throws IOException {... |
129 |
0
|
final ChapterList chapters = prop.getQedeq().getChapterList(); |
130 |
0
|
for (int i = 0; i < chapters.size(); i++) { |
131 |
0
|
final String label = prop.getQedeq().getHeader().getSpecification() |
132 |
|
.getName() + "_ch_" + i; |
133 |
0
|
final OutputStream outputStream = new FileOutputStream(new File(outputDirectory, |
134 |
|
label + "_" + language + ".wiki")); |
135 |
0
|
this.printer = new PrintStream(outputStream); |
136 |
0
|
final Chapter chapter = chapters.get(i); |
137 |
0
|
printer.print("\\chapter"); |
138 |
0
|
if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) { |
139 |
0
|
printer.print("*"); |
140 |
|
} |
141 |
0
|
printer.println("== " + getLatexListEntry(chapter.getTitle()) + " =="); |
142 |
0
|
printer.println(); |
143 |
0
|
printer.println("<div id=\"" + label + "\"></div>"); |
144 |
|
|
145 |
0
|
printer.println(); |
146 |
0
|
if (chapter.getIntroduction() != null) { |
147 |
0
|
printer.println(getLatexListEntry(chapter.getIntroduction())); |
148 |
0
|
printer.println(); |
149 |
|
} |
150 |
0
|
final SectionList sections = chapter.getSectionList(); |
151 |
0
|
if (sections != null) { |
152 |
0
|
printSections(i, sections); |
153 |
0
|
printer.println(); |
154 |
|
} |
155 |
0
|
printer.println("%% end of chapter " + getLatexListEntry(chapter.getTitle())); |
156 |
0
|
printer.println(); |
157 |
|
} |
158 |
|
} |
159 |
|
|
160 |
|
|
161 |
|
|
162 |
|
|
|
|
| 0% |
Uncovered Elements: 15 (15) |
Complexity: 3 |
Complexity Density: 0,27 |
|
163 |
0
|
private void printQedeqBibliography() {... |
164 |
0
|
final LiteratureItemList items = prop.getQedeq().getLiteratureItemList(); |
165 |
0
|
if (items == null) { |
166 |
0
|
return; |
167 |
|
} |
168 |
0
|
printer.println("\\begin{thebibliography}{99}"); |
169 |
0
|
for (int i = 0; i < items.size(); i++) { |
170 |
0
|
final LiteratureItem item = items.get(i); |
171 |
0
|
printer.print("\\bibitem{" + item.getLabel() + "} "); |
172 |
0
|
printer.println(getLatexListEntry(item.getItem())); |
173 |
0
|
printer.println(); |
174 |
|
} |
175 |
0
|
printer.println("\\end{thebibliography}"); |
176 |
0
|
printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}"); |
177 |
|
} |
178 |
|
|
179 |
|
|
180 |
|
|
181 |
|
|
182 |
|
@param |
183 |
|
@param |
184 |
|
|
|
|
| 0% |
Uncovered Elements: 15 (15) |
Complexity: 3 |
Complexity Density: 0,27 |
|
185 |
0
|
private void printSections(final int chapter, final SectionList sections) {... |
186 |
0
|
if (sections == null) { |
187 |
0
|
return; |
188 |
|
} |
189 |
0
|
for (int i = 0; i < sections.size(); i++) { |
190 |
0
|
final Section section = sections.get(i); |
191 |
0
|
printer.print("\\section{"); |
192 |
0
|
printer.print(getLatexListEntry(section.getTitle())); |
193 |
0
|
final String label = "chapter" + chapter + "_section" + i; |
194 |
0
|
printer.println("} \\label{" + label + "} \\hypertarget{" + label + "}{}"); |
195 |
0
|
printer.println(getLatexListEntry(section.getIntroduction())); |
196 |
0
|
printer.println(); |
197 |
0
|
printSubsections(section.getSubsectionList()); |
198 |
|
} |
199 |
|
} |
200 |
|
|
201 |
|
|
202 |
|
|
203 |
|
|
204 |
|
@param |
205 |
|
|
|
|
| 0% |
Uncovered Elements: 57 (57) |
Complexity: 11 |
Complexity Density: 0,31 |
|
206 |
0
|
private void printSubsections(final SubsectionList nodes) {... |
207 |
0
|
if (nodes == null) { |
208 |
0
|
return; |
209 |
|
} |
210 |
0
|
for (int i = 0; i < nodes.size(); i++) { |
211 |
0
|
final SubsectionType subsectionType = nodes.get(i); |
212 |
0
|
if (subsectionType instanceof Node) { |
213 |
0
|
final Node node = (Node) subsectionType; |
214 |
0
|
printer.println(getLatexListEntry(node.getPrecedingText())); |
215 |
0
|
printer.println(); |
216 |
0
|
printer.println("\\par"); |
217 |
0
|
final String id = node.getId(); |
218 |
0
|
final NodeType type = node.getNodeType(); |
219 |
0
|
String title = null; |
220 |
0
|
if (node.getTitle() != null) { |
221 |
0
|
title = getLatexListEntry(node.getTitle()); |
222 |
|
} |
223 |
0
|
if (type instanceof Axiom) { |
224 |
0
|
printAxiom((Axiom) type, title, id); |
225 |
0
|
} else if (type instanceof PredicateDefinition) { |
226 |
0
|
printPredicateDefinition((PredicateDefinition) type, title, id); |
227 |
0
|
} else if (type instanceof FunctionDefinition) { |
228 |
0
|
printFunctionDefinition((FunctionDefinition) type, title, id); |
229 |
0
|
} else if (type instanceof Proposition) { |
230 |
0
|
printProposition((Proposition) type, title, id); |
231 |
0
|
} else if (type instanceof Rule) { |
232 |
0
|
printRule((Rule) type, title, id); |
233 |
|
} else { |
234 |
0
|
throw new RuntimeException((type != null ? "unknown type: " |
235 |
|
+ type.getClass().getName() : "node type empty")); |
236 |
|
} |
237 |
0
|
printer.println(); |
238 |
0
|
printer.println(getLatexListEntry(node.getSucceedingText())); |
239 |
|
} else { |
240 |
0
|
final Subsection subsection = (Subsection) subsectionType; |
241 |
0
|
if (subsection.getTitle() != null) { |
242 |
0
|
printer.print("\\subsection{"); |
243 |
0
|
printer.println(getLatexListEntry(subsection.getTitle())); |
244 |
0
|
printer.println("}"); |
245 |
|
} |
246 |
0
|
printer.println(getLatexListEntry(subsection.getLatex())); |
247 |
|
} |
248 |
0
|
printer.println(); |
249 |
0
|
printer.println(); |
250 |
|
} |
251 |
|
} |
252 |
|
|
253 |
|
|
254 |
|
|
255 |
|
|
256 |
|
@param |
257 |
|
@param |
258 |
|
@param |
259 |
|
|
|
|
| 0% |
Uncovered Elements: 7 (7) |
Complexity: 1 |
Complexity Density: 0,2 |
|
260 |
0
|
private void printAxiom(final Axiom axiom, final String title, final String id) {... |
261 |
0
|
printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : "")); |
262 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
263 |
0
|
printFormula(axiom.getFormula().getElement()); |
264 |
0
|
printer.println(getLatexListEntry(axiom.getDescription())); |
265 |
0
|
printer.println("\\end{ax}"); |
266 |
|
} |
267 |
|
|
268 |
|
|
269 |
|
|
270 |
|
|
271 |
|
|
272 |
|
@param |
273 |
|
@param |
274 |
|
|
|
|
| 0% |
Uncovered Elements: 18 (18) |
Complexity: 4 |
Complexity Density: 0,4 |
|
275 |
0
|
private void printTopFormula(final Element element, final String mainLabel) {... |
276 |
0
|
if (!element.isList() || !element.getList().getOperator().equals("AND")) { |
277 |
0
|
printFormula(element); |
278 |
0
|
return; |
279 |
|
} |
280 |
0
|
final ElementList list = element.getList(); |
281 |
0
|
printer.println("\\mbox{}"); |
282 |
0
|
printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}"); |
283 |
0
|
for (int i = 0; i < list.size(); i++) { |
284 |
0
|
final String label = (i < ALPHABET.length() ? "" + ALPHABET .charAt(i) : "" + i); |
285 |
0
|
printer.println("\\centering $" + getLatex(list.getElement(i)) + "$" |
286 |
|
+ " & \\label{" + mainLabel + ":" + label + "} \\hypertarget{" + mainLabel + ":" |
287 |
|
+ label + "}{} \\mbox{\\emph{(" + label + ")}} " |
288 |
0
|
+ (i + 1 < list.size() ? "\\\\" : "")); |
289 |
|
} |
290 |
0
|
printer.println("\\end{longtable}"); |
291 |
|
} |
292 |
|
|
293 |
|
|
294 |
|
|
295 |
|
|
296 |
|
@param |
297 |
|
|
|
|
| 0% |
Uncovered Elements: 4 (4) |
Complexity: 1 |
Complexity Density: 0,25 |
|
298 |
0
|
private void printFormula(final Element element) {... |
299 |
0
|
printer.println("\\mbox{}"); |
300 |
0
|
printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}"); |
301 |
0
|
printer.println("\\centering $" + getLatex(element) + "$"); |
302 |
0
|
printer.println("\\end{longtable}"); |
303 |
|
} |
304 |
|
|
305 |
|
|
306 |
|
|
307 |
|
|
308 |
|
@param |
309 |
|
@param |
310 |
|
@param |
311 |
|
|
|
|
| 0% |
Uncovered Elements: 33 (33) |
Complexity: 5 |
Complexity Density: 0,24 |
|
312 |
0
|
private void printPredicateDefinition(final PredicateDefinition definition, final String title,... |
313 |
|
final String id) { |
314 |
0
|
final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern()); |
315 |
0
|
final VariableList list = definition.getVariableList(); |
316 |
0
|
if (list != null) { |
317 |
0
|
for (int i = list.size() - 1; i >= 0; i--) { |
318 |
0
|
Trace.trace(CLASS, this, "printDefinition", "replacing!"); |
319 |
0
|
StringUtility.replace(define, "#" + (i + 1), getLatex(list.get(i))); |
320 |
|
} |
321 |
|
} |
322 |
0
|
if (definition.getFormula() != null) { |
323 |
0
|
printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : "")); |
324 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
325 |
0
|
define.append("\\ :\\leftrightarrow \\ "); |
326 |
0
|
define.append(getLatex(definition.getFormula().getElement())); |
327 |
|
} else { |
328 |
0
|
printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : "")); |
329 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
330 |
|
} |
331 |
0
|
define.append("$$"); |
332 |
0
|
elementConverter.addPredicate(definition); |
333 |
0
|
Trace.param(CLASS, this, "printDefinition", "define", define); |
334 |
0
|
printer.println(define); |
335 |
0
|
printer.println(getLatexListEntry(definition.getDescription())); |
336 |
0
|
if (definition.getFormula() != null) { |
337 |
0
|
printer.println("\\end{defn}"); |
338 |
|
} else { |
339 |
0
|
printer.println("\\end{idefn}"); |
340 |
|
} |
341 |
|
} |
342 |
|
|
343 |
|
|
344 |
|
|
345 |
|
|
346 |
|
@param |
347 |
|
@param |
348 |
|
@param |
349 |
|
|
|
|
| 0% |
Uncovered Elements: 33 (33) |
Complexity: 5 |
Complexity Density: 0,24 |
|
350 |
0
|
private void printFunctionDefinition(final FunctionDefinition definition, final String title,... |
351 |
|
final String id) { |
352 |
0
|
final StringBuffer define = new StringBuffer("$$" + definition.getLatexPattern()); |
353 |
0
|
final VariableList list = definition.getVariableList(); |
354 |
0
|
if (list != null) { |
355 |
0
|
for (int i = list.size() - 1; i >= 0; i--) { |
356 |
0
|
Trace.trace(CLASS, this, "printDefinition", "replacing!"); |
357 |
0
|
StringUtility.replace(define, "#" + (i + 1), getLatex(list.get(i))); |
358 |
|
} |
359 |
|
} |
360 |
0
|
if (definition.getTerm() != null) { |
361 |
0
|
printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : "")); |
362 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
363 |
0
|
define.append("\\ := \\ "); |
364 |
0
|
define.append(getLatex(definition.getTerm().getElement())); |
365 |
|
} else { |
366 |
0
|
printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : "")); |
367 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
368 |
|
} |
369 |
0
|
define.append("$$"); |
370 |
0
|
elementConverter.addFunction(definition); |
371 |
0
|
Trace.param(CLASS, this, "printDefinition", "define", define); |
372 |
0
|
printer.println(define); |
373 |
0
|
printer.println(getLatexListEntry(definition.getDescription())); |
374 |
0
|
if (definition.getTerm() != null) { |
375 |
0
|
printer.println("\\end{defn}"); |
376 |
|
} else { |
377 |
0
|
printer.println("\\end{idefn}"); |
378 |
|
} |
379 |
|
} |
380 |
|
|
381 |
|
|
382 |
|
|
383 |
|
|
384 |
|
@param |
385 |
|
@param |
386 |
|
@param |
387 |
|
|
|
|
| 0% |
Uncovered Elements: 16 (16) |
Complexity: 3 |
Complexity Density: 0,3 |
|
388 |
0
|
private void printProposition(final Proposition proposition, final String title,... |
389 |
|
final String id) { |
390 |
0
|
printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : "")); |
391 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
392 |
0
|
printTopFormula(proposition.getFormula().getElement(), id); |
393 |
0
|
printer.println(getLatexListEntry(proposition.getDescription())); |
394 |
0
|
printer.println("\\end{prop}"); |
395 |
0
|
if (proposition.getProofList() != null) { |
396 |
0
|
for (int i = 0; i < proposition.getProofList().size(); i++) { |
397 |
0
|
printer.println("\\begin{proof}"); |
398 |
0
|
printer.println(getLatexListEntry(proposition.getProofList().get(i) |
399 |
|
.getNonFormalProof())); |
400 |
0
|
printer.println("\\end{proof}"); |
401 |
|
} |
402 |
|
} |
403 |
|
} |
404 |
|
|
405 |
|
|
406 |
|
|
407 |
|
|
408 |
|
@param |
409 |
|
@param |
410 |
|
@param |
411 |
|
|
|
|
| 0% |
Uncovered Elements: 15 (15) |
Complexity: 3 |
Complexity Density: 0,33 |
|
412 |
0
|
private void printRule(final Rule rule, final String title,... |
413 |
|
final String id) { |
414 |
0
|
printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : "")); |
415 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
416 |
0
|
printer.println(getLatexListEntry(rule.getDescription())); |
417 |
0
|
printer.println("\\end{rul}"); |
418 |
|
|
419 |
|
|
420 |
|
|
421 |
|
|
422 |
|
|
423 |
|
|
424 |
|
|
425 |
|
|
426 |
|
|
427 |
|
|
428 |
|
|
429 |
|
|
430 |
|
|
431 |
|
|
432 |
0
|
if (rule.getProofList() != null) { |
433 |
0
|
for (int i = 0; i < rule.getProofList().size(); i++) { |
434 |
0
|
printer.println("\\begin{proof}"); |
435 |
0
|
printer.println(getLatexListEntry(rule.getProofList().get(i) |
436 |
|
.getNonFormalProof())); |
437 |
0
|
printer.println("\\end{proof}"); |
438 |
|
} |
439 |
|
} |
440 |
|
} |
441 |
|
|
442 |
|
|
443 |
|
|
444 |
|
|
445 |
|
@param |
446 |
|
@return |
447 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
448 |
0
|
private String getLatex(final Element element) {... |
449 |
0
|
return elementConverter.getLatex(element); |
450 |
|
} |
451 |
|
|
452 |
|
|
453 |
|
|
454 |
|
|
455 |
|
|
456 |
|
|
457 |
|
@param |
458 |
|
@return |
459 |
|
|
|
|
| 0% |
Uncovered Elements: 23 (23) |
Complexity: 7 |
Complexity Density: 0,64 |
|
460 |
0
|
private String getLatexListEntry(final LatexList list) {... |
461 |
0
|
if (list == null) { |
462 |
0
|
return ""; |
463 |
|
} |
464 |
0
|
for (int i = 0; i < list.size(); i++) { |
465 |
0
|
if (language.equals(list.get(i).getLanguage())) { |
466 |
0
|
return getLatex(list.get(i)); |
467 |
|
} |
468 |
|
} |
469 |
|
|
470 |
0
|
for (int i = 0; i < list.size(); i++) { |
471 |
0
|
if (list.get(i).getLanguage() == null) { |
472 |
0
|
return getLatex(list.get(i)); |
473 |
|
} |
474 |
|
} |
475 |
0
|
for (int i = 0; i < list.size(); i++) { |
476 |
0
|
return "MISSING! OTHER: " + getLatex(list.get(i)); |
477 |
|
} |
478 |
0
|
return "MISSING!"; |
479 |
|
} |
480 |
|
|
481 |
|
|
482 |
|
|
483 |
|
|
484 |
|
|
485 |
|
@param |
486 |
|
@return |
487 |
|
|
|
|
| 0% |
Uncovered Elements: 5 (5) |
Complexity: 3 |
Complexity Density: 1 |
|
488 |
0
|
private String getLatex(final Latex latex) {... |
489 |
0
|
if (latex == null || latex.getLatex() == null) { |
490 |
0
|
return ""; |
491 |
|
} |
492 |
0
|
return LatexTextParser.transform(latex.getLatex()); |
493 |
|
} |
494 |
|
|
495 |
|
} |