1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
package org.qedeq.kernel.bo.service.latex; |
17 |
|
|
18 |
|
import java.io.File; |
19 |
|
import java.io.FileInputStream; |
20 |
|
import java.io.FileOutputStream; |
21 |
|
import java.io.IOException; |
22 |
|
import java.io.InputStream; |
23 |
|
import java.util.Locale; |
24 |
|
|
25 |
|
import org.qedeq.base.io.IoUtility; |
26 |
|
import org.qedeq.base.io.Parameters; |
27 |
|
import org.qedeq.base.io.SourcePosition; |
28 |
|
import org.qedeq.base.io.TextInput; |
29 |
|
import org.qedeq.base.io.TextOutput; |
30 |
|
import org.qedeq.base.trace.Trace; |
31 |
|
import org.qedeq.base.utility.DateUtility; |
32 |
|
import org.qedeq.base.utility.EqualsUtility; |
33 |
|
import org.qedeq.base.utility.StringUtility; |
34 |
|
import org.qedeq.kernel.bo.log.QedeqLog; |
35 |
|
import org.qedeq.kernel.bo.module.ControlVisitor; |
36 |
|
import org.qedeq.kernel.bo.module.InternalServiceCall; |
37 |
|
import org.qedeq.kernel.bo.module.KernelNodeBo; |
38 |
|
import org.qedeq.kernel.bo.module.KernelQedeqBo; |
39 |
|
import org.qedeq.kernel.bo.module.PluginExecutor; |
40 |
|
import org.qedeq.kernel.bo.module.Reference; |
41 |
|
import org.qedeq.kernel.se.base.list.Element; |
42 |
|
import org.qedeq.kernel.se.base.list.ElementList; |
43 |
|
import org.qedeq.kernel.se.base.module.Add; |
44 |
|
import org.qedeq.kernel.se.base.module.Author; |
45 |
|
import org.qedeq.kernel.se.base.module.AuthorList; |
46 |
|
import org.qedeq.kernel.se.base.module.Axiom; |
47 |
|
import org.qedeq.kernel.se.base.module.ChangedRule; |
48 |
|
import org.qedeq.kernel.se.base.module.ChangedRuleList; |
49 |
|
import org.qedeq.kernel.se.base.module.Chapter; |
50 |
|
import org.qedeq.kernel.se.base.module.Conclusion; |
51 |
|
import org.qedeq.kernel.se.base.module.ConditionalProof; |
52 |
|
import org.qedeq.kernel.se.base.module.Existential; |
53 |
|
import org.qedeq.kernel.se.base.module.FormalProof; |
54 |
|
import org.qedeq.kernel.se.base.module.FormalProofLine; |
55 |
|
import org.qedeq.kernel.se.base.module.FormalProofLineList; |
56 |
|
import org.qedeq.kernel.se.base.module.FunctionDefinition; |
57 |
|
import org.qedeq.kernel.se.base.module.Header; |
58 |
|
import org.qedeq.kernel.se.base.module.Hypothesis; |
59 |
|
import org.qedeq.kernel.se.base.module.Import; |
60 |
|
import org.qedeq.kernel.se.base.module.ImportList; |
61 |
|
import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
62 |
|
import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
63 |
|
import org.qedeq.kernel.se.base.module.Latex; |
64 |
|
import org.qedeq.kernel.se.base.module.LatexList; |
65 |
|
import org.qedeq.kernel.se.base.module.LinkList; |
66 |
|
import org.qedeq.kernel.se.base.module.LiteratureItem; |
67 |
|
import org.qedeq.kernel.se.base.module.LiteratureItemList; |
68 |
|
import org.qedeq.kernel.se.base.module.LocationList; |
69 |
|
import org.qedeq.kernel.se.base.module.ModusPonens; |
70 |
|
import org.qedeq.kernel.se.base.module.Node; |
71 |
|
import org.qedeq.kernel.se.base.module.PredicateDefinition; |
72 |
|
import org.qedeq.kernel.se.base.module.Proof; |
73 |
|
import org.qedeq.kernel.se.base.module.Proposition; |
74 |
|
import org.qedeq.kernel.se.base.module.Qedeq; |
75 |
|
import org.qedeq.kernel.se.base.module.Rename; |
76 |
|
import org.qedeq.kernel.se.base.module.Rule; |
77 |
|
import org.qedeq.kernel.se.base.module.Section; |
78 |
|
import org.qedeq.kernel.se.base.module.SectionList; |
79 |
|
import org.qedeq.kernel.se.base.module.Specification; |
80 |
|
import org.qedeq.kernel.se.base.module.Subsection; |
81 |
|
import org.qedeq.kernel.se.base.module.SubsectionList; |
82 |
|
import org.qedeq.kernel.se.base.module.SubsectionType; |
83 |
|
import org.qedeq.kernel.se.base.module.SubstFree; |
84 |
|
import org.qedeq.kernel.se.base.module.SubstFunc; |
85 |
|
import org.qedeq.kernel.se.base.module.SubstPred; |
86 |
|
import org.qedeq.kernel.se.base.module.Universal; |
87 |
|
import org.qedeq.kernel.se.base.module.UsedByList; |
88 |
|
import org.qedeq.kernel.se.common.ModuleAddress; |
89 |
|
import org.qedeq.kernel.se.common.ModuleContext; |
90 |
|
import org.qedeq.kernel.se.common.ModuleDataException; |
91 |
|
import org.qedeq.kernel.se.common.Plugin; |
92 |
|
import org.qedeq.kernel.se.common.RuleKey; |
93 |
|
import org.qedeq.kernel.se.common.SourceFileExceptionList; |
94 |
|
|
95 |
|
|
96 |
|
|
97 |
|
|
98 |
|
|
99 |
|
|
100 |
|
|
101 |
|
|
102 |
|
|
103 |
|
@author |
104 |
|
|
|
|
| 80.2% |
Uncovered Elements: 248 (1,253) |
Complexity: 309 |
Complexity Density: 0.39 |
|
105 |
|
public final class Qedeq2LatexExecutor extends ControlVisitor implements PluginExecutor { |
106 |
|
|
107 |
|
|
108 |
|
private static final Class CLASS = Qedeq2LatexExecutor.class; |
109 |
|
|
110 |
|
|
111 |
|
|
112 |
|
|
113 |
|
|
114 |
|
private TextOutput printer; |
115 |
|
|
116 |
|
|
117 |
|
private String language; |
118 |
|
|
119 |
|
|
120 |
|
|
121 |
|
|
122 |
|
|
123 |
|
private final boolean info; |
124 |
|
|
125 |
|
|
126 |
|
private final boolean brief; |
127 |
|
|
128 |
|
|
129 |
|
private String id; |
130 |
|
|
131 |
|
|
132 |
|
private String title; |
133 |
|
|
134 |
|
|
135 |
|
private String subContext = ""; |
136 |
|
|
137 |
|
|
138 |
|
private String label = ""; |
139 |
|
|
140 |
|
|
141 |
|
private String formula = ""; |
142 |
|
|
143 |
|
|
144 |
|
private String reason = ""; |
145 |
|
|
146 |
|
|
147 |
|
private int tabLevel = 0; |
148 |
|
|
149 |
|
|
150 |
|
private static final String ALPHABET = "abcdefghijklmnopqrstuvwxyz"; |
151 |
|
|
152 |
|
|
153 |
|
|
154 |
|
|
155 |
|
@param |
156 |
|
@param |
157 |
|
@param |
158 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0.33 |
|
159 |
42
|
public Qedeq2LatexExecutor(final Plugin plugin, final KernelQedeqBo prop, final Parameters parameters) {... |
160 |
42
|
super(plugin, prop); |
161 |
42
|
info = parameters.getBoolean("info"); |
162 |
42
|
brief = parameters.getBoolean("brief"); |
163 |
|
} |
164 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
165 |
46
|
private Plugin getPlugin() {... |
166 |
46
|
return (Plugin) getService(); |
167 |
|
} |
168 |
|
|
|
|
| 48.4% |
Uncovered Elements: 16 (31) |
Complexity: 8 |
Complexity Density: 0.35 |
|
169 |
4
|
public Object executePlugin(final InternalServiceCall call, final Object data) {... |
170 |
4
|
final String method = "executePlugin(QedeqBo, Map)"; |
171 |
4
|
try { |
172 |
4
|
QedeqLog.getInstance().logRequest("Generate LaTeX", getQedeqBo().getUrl()); |
173 |
4
|
final String[] languages = getQedeqBo().getSupportedLanguages(); |
174 |
12
|
for (int j = 0; j < languages.length; j++) { |
175 |
8
|
language = languages[j]; |
176 |
|
|
177 |
8
|
final String result = generateLatex(call, languages[j], "1").toString(); |
178 |
8
|
if (languages[j] != null) { |
179 |
8
|
QedeqLog.getInstance().logSuccessfulReply( |
180 |
|
"LaTeX for language \"" + languages[j] |
181 |
|
+ "\" was generated from into \"" + result + "\"", getQedeqBo().getUrl()); |
182 |
|
} else { |
183 |
0
|
QedeqLog.getInstance().logSuccessfulReply( |
184 |
|
"LaTeX for default language " |
185 |
|
+ "was generated into \"" + result + "\"", getQedeqBo().getUrl()); |
186 |
|
} |
187 |
|
} |
188 |
4
|
if (languages.length == 0) { |
189 |
0
|
QedeqLog.getInstance().logMessage("no supported language found, assuming 'en'"); |
190 |
0
|
final String result = generateLatex(call, "en", "1").toString(); |
191 |
0
|
QedeqLog.getInstance().logSuccessfulReply( |
192 |
|
"LaTeX for language \"en" |
193 |
|
+ "\" was generated into \"" + result + "\"", getQedeqBo().getUrl()); |
194 |
|
} |
195 |
|
} catch (final SourceFileExceptionList e) { |
196 |
0
|
final String msg = "Generation failed"; |
197 |
0
|
Trace.fatal(CLASS, this, method, msg, e); |
198 |
0
|
QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage()); |
199 |
|
} catch (IOException e) { |
200 |
0
|
final String msg = "Generation failed"; |
201 |
0
|
Trace.fatal(CLASS, this, method, msg, e); |
202 |
0
|
QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage()); |
203 |
|
} catch (final RuntimeException e) { |
204 |
0
|
Trace.fatal(CLASS, this, method, "unexpected problem", e); |
205 |
0
|
QedeqLog.getInstance().logFailureReply( |
206 |
|
"Generation failed", getQedeqBo().getUrl(), "unexpected problem: " |
207 |
0
|
+ (e.getMessage() != null ? e.getMessage() : e.toString())); |
208 |
|
} |
209 |
4
|
return null; |
210 |
|
} |
211 |
|
|
212 |
|
|
213 |
|
|
214 |
|
|
215 |
|
@param |
216 |
|
@param |
217 |
|
@param |
218 |
|
|
219 |
|
@return |
220 |
|
@throws |
221 |
|
@throws |
222 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
223 |
38
|
public InputStream createLatex(final InternalServiceCall call, final String language, final String level)... |
224 |
|
throws SourceFileExceptionList, IOException { |
225 |
38
|
return new FileInputStream(generateLatex(call, language, level)); |
226 |
|
} |
227 |
|
|
228 |
|
|
229 |
|
|
230 |
|
|
231 |
|
@param |
232 |
|
@param |
233 |
|
|
234 |
|
@param |
235 |
|
|
236 |
|
@return |
237 |
|
@throws |
238 |
|
@throws |
239 |
|
|
|
|
| 81.6% |
Uncovered Elements: 7 (38) |
Complexity: 10 |
Complexity Density: 0.36 |
|
240 |
46
|
public File generateLatex(final InternalServiceCall call, final String language, final String level)... |
241 |
|
throws SourceFileExceptionList, IOException { |
242 |
46
|
final String method = "generateLatex(String, String)"; |
243 |
46
|
this.language = language; |
244 |
|
|
245 |
|
|
246 |
46
|
try { |
247 |
46
|
getServices().loadRequiredModules(call.getInternalServiceProcess(), getQedeqBo()); |
248 |
46
|
getServices().checkWellFormedness(call.getInternalServiceProcess(), getQedeqBo()); |
249 |
|
} catch (Exception e) { |
250 |
|
|
251 |
0
|
Trace.trace(CLASS, method, e); |
252 |
|
} |
253 |
46
|
String tex = getQedeqBo().getModuleAddress().getFileName(); |
254 |
46
|
if (tex.toLowerCase(Locale.US).endsWith(".xml")) { |
255 |
46
|
tex = tex.substring(0, tex.length() - 4); |
256 |
|
} |
257 |
46
|
if (language != null && language.length() > 0) { |
258 |
46
|
tex = tex + "_" + language; |
259 |
|
} |
260 |
|
|
261 |
|
|
262 |
46
|
File destination = new File(getServices().getConfig() |
263 |
|
.getGenerationDirectory(), tex + ".tex").getCanonicalFile(); |
264 |
|
|
265 |
46
|
init(); |
266 |
|
|
267 |
46
|
try { |
268 |
|
|
269 |
46
|
if ("de".equals(language)) { |
270 |
18
|
printer = new TextOutput(getQedeqBo().getName(), new FileOutputStream(destination), |
271 |
|
"ISO-8859-1") { |
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
272 |
227172
|
public void append(final String txt) {... |
273 |
227172
|
super.append(escapeUmlauts(txt)); |
274 |
|
} |
275 |
|
}; |
276 |
|
} else { |
277 |
28
|
printer = new TextOutput(getQedeqBo().getName(), new FileOutputStream(destination), |
278 |
|
"UTF-8") { |
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
279 |
306048
|
public void append(final String txt) {... |
280 |
306048
|
super.append(escapeUmlauts(txt)); |
281 |
|
} |
282 |
|
}; |
283 |
|
} |
284 |
46
|
traverse(call.getInternalServiceProcess()); |
285 |
|
} finally { |
286 |
46
|
getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList()); |
287 |
46
|
if (printer != null) { |
288 |
46
|
printer.flush(); |
289 |
46
|
printer.close(); |
290 |
|
} |
291 |
|
} |
292 |
46
|
if (printer != null && printer.checkError()) { |
293 |
0
|
throw printer.getError(); |
294 |
|
} |
295 |
46
|
try { |
296 |
46
|
QedeqBoDuplicateLanguageChecker.check(call); |
297 |
|
} catch (SourceFileExceptionList warnings) { |
298 |
0
|
getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), null, warnings); |
299 |
|
} |
300 |
46
|
return destination.getCanonicalFile(); |
301 |
|
} |
302 |
|
|
303 |
|
|
304 |
|
@link |
305 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0.33 |
|
306 |
46
|
protected void init() {... |
307 |
46
|
id = null; |
308 |
46
|
title = null; |
309 |
46
|
subContext = ""; |
310 |
|
} |
311 |
|
|
|
|
| 94% |
Uncovered Elements: 5 (84) |
Complexity: 6 |
Complexity Density: 0.08 |
|
312 |
46
|
public final void visitEnter(final Qedeq qedeq) {... |
313 |
46
|
printer.println("% -*- TeX" |
314 |
46
|
+ (language != null ? ":" + language.toUpperCase(Locale.US) : "") + " -*-"); |
315 |
46
|
printer.println("%%% ===================================================================="); |
316 |
46
|
printer.println("%%% @LaTeX-file " + printer.getName()); |
317 |
46
|
printer.println("%%% Generated from " + getQedeqBo().getModuleAddress()); |
318 |
46
|
printer.println("%%% Generated at " + DateUtility.getTimestamp()); |
319 |
46
|
printer.println("%%% ===================================================================="); |
320 |
46
|
printer.println(); |
321 |
46
|
printer.println( |
322 |
|
"%%% Permission is granted to copy, distribute and/or modify this document"); |
323 |
46
|
printer.println("%%% under the terms of the GNU Free Documentation License, Version 1.2"); |
324 |
46
|
printer.println("%%% or any later version published by the Free Software Foundation;"); |
325 |
46
|
printer.println( |
326 |
|
"%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts."); |
327 |
46
|
printer.println(); |
328 |
46
|
printer.println("\\documentclass[a4paper,german,10pt,twoside]{book}"); |
329 |
46
|
if ("de".equals(language)) { |
330 |
18
|
printer.println("\\usepackage[german]{babel}"); |
331 |
|
} else { |
332 |
28
|
if (!"en".equals(language)) { |
333 |
0
|
printer.println("%%% TODO unknown language: " + language); |
334 |
|
} |
335 |
28
|
printer.println("\\usepackage[english]{babel}"); |
336 |
|
} |
337 |
46
|
printer.println("\\usepackage{makeidx}"); |
338 |
46
|
printer.println("\\usepackage{amsmath,amsthm,amssymb}"); |
339 |
46
|
printer.println("\\usepackage{color}"); |
340 |
46
|
printer.println("\\usepackage{xr}"); |
341 |
46
|
printer.println("\\usepackage{tabularx}"); |
342 |
|
|
343 |
|
|
344 |
46
|
printer.println("\\usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen,"); |
345 |
46
|
printer.println(" unicode=true,colorlinks=true,linkcolor=webgreen,"); |
346 |
46
|
printer.println(" pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref}"); |
347 |
46
|
printer.println("\\definecolor{webgreen}{rgb}{0,.5,0}"); |
348 |
46
|
printer.println("\\usepackage{epsfig,longtable}"); |
349 |
46
|
printer.println("\\usepackage{graphicx}"); |
350 |
46
|
printer.println("\\usepackage[all]{hypcap}"); |
351 |
46
|
printer.println(); |
352 |
46
|
if ("de".equals(language)) { |
353 |
|
|
354 |
|
|
355 |
18
|
printer.println("\\newtheorem{thm}{Theorem}"); |
356 |
18
|
printer.println("\\newtheorem{cor}[thm]{Korollar}"); |
357 |
18
|
printer.println("\\newtheorem{lem}[thm]{Lemma}"); |
358 |
18
|
printer.println("\\newtheorem{prop}[thm]{Proposition}"); |
359 |
18
|
printer.println("\\newtheorem{ax}{Axiom}"); |
360 |
18
|
printer.println("\\newtheorem{rul}{Regel}"); |
361 |
18
|
printer.println(); |
362 |
18
|
printer.println("\\theoremstyle{definition}"); |
363 |
18
|
printer.println("\\newtheorem{defn}{Definition}"); |
364 |
18
|
printer.println("\\newtheorem{idefn}[defn]{Initiale Definition}"); |
365 |
18
|
printer.println(); |
366 |
18
|
printer.println("\\theoremstyle{remark}"); |
367 |
18
|
printer.println("\\newtheorem{rem}[thm]{Bemerkung}"); |
368 |
18
|
printer.println("\\newtheorem*{notation}{Notation}"); |
369 |
|
} else { |
370 |
28
|
if (!"en".equals(language)) { |
371 |
0
|
printer.println("%%% TODO unknown language: " + language); |
372 |
|
} |
373 |
|
|
374 |
|
|
375 |
28
|
printer.println("\\newtheorem{thm}{Theorem}"); |
376 |
28
|
printer.println("\\newtheorem{cor}[thm]{Corollary}"); |
377 |
28
|
printer.println("\\newtheorem{lem}[thm]{Lemma}"); |
378 |
28
|
printer.println("\\newtheorem{prop}[thm]{Proposition}"); |
379 |
28
|
printer.println("\\newtheorem{ax}{Axiom}"); |
380 |
28
|
printer.println("\\newtheorem{rul}{Rule}"); |
381 |
28
|
printer.println(); |
382 |
28
|
printer.println("\\theoremstyle{definition}"); |
383 |
28
|
printer.println("\\newtheorem{defn}{Definition}"); |
384 |
28
|
printer.println("\\newtheorem{idefn}[defn]{Initial Definition}"); |
385 |
28
|
printer.println(); |
386 |
28
|
printer.println("\\theoremstyle{remark}"); |
387 |
28
|
printer.println("\\newtheorem{rem}[thm]{Remark}"); |
388 |
28
|
printer.println("\\newtheorem*{notation}{Notation}"); |
389 |
|
} |
390 |
46
|
printer.println(); |
391 |
46
|
printer.println(); |
392 |
46
|
printer.println("\\addtolength{\\textheight}{7\\baselineskip}"); |
393 |
46
|
printer.println("\\addtolength{\\topmargin}{-5\\baselineskip}"); |
394 |
46
|
printer.println(); |
395 |
46
|
printer.println("\\setlength{\\parindent}{0pt}"); |
396 |
46
|
printer.println(); |
397 |
46
|
printer.println("\\frenchspacing \\sloppy"); |
398 |
46
|
printer.println(); |
399 |
46
|
printer.println("\\makeindex"); |
400 |
46
|
printer.println(); |
401 |
46
|
printer.println(); |
402 |
|
} |
403 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0.25 |
|
404 |
46
|
public final void visitLeave(final Qedeq qedeq) {... |
405 |
46
|
printer.println("\\addcontentsline{toc}{chapter}{\\indexname} \\printindex"); |
406 |
46
|
printer.println(); |
407 |
46
|
printer.println("\\end{document}"); |
408 |
46
|
printer.println(); |
409 |
|
} |
410 |
|
|
|
|
| 86% |
Uncovered Elements: 12 (86) |
Complexity: 15 |
Complexity Density: 0.23 |
|
411 |
46
|
public void visitEnter(final Header header) {... |
412 |
46
|
final LatexList tit = header.getTitle(); |
413 |
46
|
printer.print("\\title{"); |
414 |
46
|
printer.print(getLatexListEntry("getTitle()", tit)); |
415 |
46
|
printer.println("}"); |
416 |
46
|
printer.println("\\author{"); |
417 |
46
|
final AuthorList authors = getQedeqBo().getQedeq().getHeader().getAuthorList(); |
418 |
46
|
final StringBuffer authorList = new StringBuffer(); |
419 |
92
|
for (int i = 0; i < authors.size(); i++) { |
420 |
46
|
if (i > 0) { |
421 |
0
|
authorList.append(", "); |
422 |
0
|
printer.println(", "); |
423 |
|
} |
424 |
46
|
final Author author = authors.get(i); |
425 |
46
|
final String name = author.getName().getLatex().trim(); |
426 |
46
|
printer.print(name); |
427 |
46
|
authorList.append(name); |
428 |
46
|
String email = author.getEmail(); |
429 |
46
|
if (email != null && email.trim().length() > 0) { |
430 |
46
|
authorList.append(" \\href{mailto:" + email + "}{" + email + "}"); |
431 |
|
} |
432 |
|
} |
433 |
46
|
printer.println(); |
434 |
46
|
printer.println("}"); |
435 |
46
|
printer.println(); |
436 |
46
|
printer.println("\\begin{document}"); |
437 |
46
|
printer.println(); |
438 |
46
|
printer.println("\\maketitle"); |
439 |
46
|
printer.println(); |
440 |
46
|
printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}"); |
441 |
46
|
printer.println("\\mbox{}"); |
442 |
46
|
printer.println("\\vfill"); |
443 |
46
|
printer.println(); |
444 |
46
|
final String url = getQedeqBo().getUrl(); |
445 |
46
|
if (url != null && url.length() > 0) { |
446 |
46
|
printer.println("\\par"); |
447 |
46
|
if ("de".equals(language)) { |
448 |
18
|
printer.println("Die Quelle f{\"ur} dieses Dokument ist hier zu finden:"); |
449 |
|
} else { |
450 |
28
|
if (!"en".equals(language)) { |
451 |
0
|
printer.println("%%% TODO unknown language: " + language); |
452 |
|
} |
453 |
28
|
printer.println("The source for this document can be found here:"); |
454 |
|
} |
455 |
46
|
printer.println("\\par"); |
456 |
46
|
printer.println("\\url{" + url + "}"); |
457 |
46
|
printer.println(); |
458 |
|
} |
459 |
|
{ |
460 |
46
|
printer.println("\\par"); |
461 |
46
|
if ("de".equals(language)) { |
462 |
18
|
printer.println("Die vorliegende Publikation ist urheberrechtlich gesch{\"u}tzt."); |
463 |
|
} else { |
464 |
28
|
if (!"en".equals(language)) { |
465 |
0
|
printer.println("%%% TODO unknown language: " + language); |
466 |
|
} |
467 |
28
|
printer.println("Copyright by the authors. All rights reserved."); |
468 |
|
} |
469 |
|
} |
470 |
46
|
final String email = header.getEmail(); |
471 |
46
|
if (email != null && email.length() > 0) { |
472 |
46
|
final String emailUrl = "\\href{mailto:" + email + "}{" + email + "}"; |
473 |
46
|
printer.println("\\par"); |
474 |
46
|
if ("de".equals(language)) { |
475 |
18
|
printer.println("Bei Fragen, Anregungen oder Bitte um Aufnahme in die Liste der" |
476 |
|
+ " abh\u00e4ngigen Module schicken Sie bitte eine EMail an die Adresse " |
477 |
|
+ emailUrl); |
478 |
18
|
printer.println(); |
479 |
18
|
printer.println("\\par"); |
480 |
18
|
printer.println("Die Autoren dieses Dokuments sind:"); |
481 |
18
|
printer.println(authorList); |
482 |
|
} else { |
483 |
28
|
if (!"en".equals(language)) { |
484 |
0
|
printer.println("%%% TODO unknown language: " + language); |
485 |
|
} |
486 |
28
|
printer.println("If you have any questions, suggestions or want to add something" |
487 |
|
+ " to the list of modules that use this one, please send an email to the" |
488 |
|
+ " address " + emailUrl); |
489 |
28
|
printer.println(); |
490 |
28
|
printer.println("\\par"); |
491 |
28
|
printer.println("The authors of this document are:"); |
492 |
28
|
printer.println(authorList); |
493 |
|
} |
494 |
46
|
printer.println(); |
495 |
|
} |
496 |
|
} |
497 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (7) |
Complexity: 1 |
Complexity Density: 0.14 |
|
498 |
46
|
public void visitLeave(final Header header) {... |
499 |
46
|
printer.println(); |
500 |
46
|
printer.println(); |
501 |
46
|
printer.println("\\setlength{\\parskip}{0pt}"); |
502 |
46
|
printer.println("\\tableofcontents"); |
503 |
46
|
printer.println(); |
504 |
46
|
printer.println("\\setlength{\\parskip}{5pt plus 2pt minus 1pt}"); |
505 |
46
|
printer.println(); |
506 |
|
} |
507 |
|
|
|
|
| 86.7% |
Uncovered Elements: 2 (15) |
Complexity: 3 |
Complexity Density: 0.27 |
|
508 |
22
|
public void visitEnter(final ImportList imports) throws ModuleDataException {... |
509 |
22
|
printer.println(); |
510 |
22
|
printer.println(); |
511 |
22
|
printer.println("\\par"); |
512 |
22
|
if ("de".equals(language)) { |
513 |
10
|
printer.println("Benutzte QEDEQ module:"); |
514 |
|
} else { |
515 |
12
|
if (!"en".equals(language)) { |
516 |
0
|
printer.println("%%% TODO unknown language: " + language); |
517 |
|
} |
518 |
12
|
printer.println("Used other QEDEQ modules:"); |
519 |
|
} |
520 |
22
|
printer.println(); |
521 |
22
|
printer.println("\\par"); |
522 |
22
|
printer.println(); |
523 |
|
} |
524 |
|
|
|
|
| 90.9% |
Uncovered Elements: 1 (11) |
Complexity: 4 |
Complexity Density: 0.44 |
|
525 |
32
|
public void visitEnter(final Import imp) throws ModuleDataException {... |
526 |
32
|
printer.println(); |
527 |
32
|
printer.println("\\par"); |
528 |
32
|
printer.print("\\textbf{" + imp.getLabel() + "} "); |
529 |
32
|
final Specification spec = imp.getSpecification(); |
530 |
32
|
printer.print(getLatex(spec.getName())); |
531 |
32
|
if (spec.getLocationList() != null && spec.getLocationList().size() > 0 |
532 |
|
&& spec.getLocationList().get(0).getLocation().length() > 0) { |
533 |
32
|
printer.print(" "); |
534 |
32
|
printer.print("\\url{" + getPdfLink((KernelQedeqBo) getQedeqBo() |
535 |
|
.getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}"); |
536 |
|
} |
537 |
32
|
printer.println(); |
538 |
|
} |
539 |
|
|
540 |
|
|
541 |
|
|
542 |
|
|
543 |
|
@param |
544 |
|
@param |
545 |
|
@return |
546 |
|
|
|
|
| 62.5% |
Uncovered Elements: 3 (8) |
Complexity: 4 |
Complexity Density: 0.67 |
|
547 |
8
|
private String getUrl(final ModuleAddress address, final Specification specification) {... |
548 |
8
|
final LocationList list = specification.getLocationList(); |
549 |
8
|
if (list == null || list.size() <= 0) { |
550 |
0
|
return ""; |
551 |
|
} |
552 |
8
|
try { |
553 |
8
|
return address.getModulePaths(specification)[0].getUrl(); |
554 |
|
} catch (IOException e) { |
555 |
0
|
return ""; |
556 |
|
} |
557 |
|
} |
558 |
|
|
|
|
| 35.7% |
Uncovered Elements: 36 (56) |
Complexity: 16 |
Complexity Density: 0.47 |
|
559 |
146
|
public void visitEnter(final Chapter chapter) {... |
560 |
|
|
561 |
146
|
if (brief) { |
562 |
0
|
boolean hasFormalContent = false; |
563 |
0
|
do { |
564 |
0
|
final SectionList sections = chapter.getSectionList(); |
565 |
0
|
if (sections == null) { |
566 |
0
|
break; |
567 |
|
} |
568 |
0
|
for (int i = 0; i < sections.size() && !hasFormalContent; i++) { |
569 |
0
|
final Section section = sections.get(i); |
570 |
0
|
if (section == null) { |
571 |
0
|
continue; |
572 |
|
} |
573 |
0
|
final SubsectionList subSections = section.getSubsectionList(); |
574 |
0
|
if (subSections == null) { |
575 |
0
|
continue; |
576 |
|
} |
577 |
0
|
for (int j = 0; j < subSections.size(); j++) { |
578 |
0
|
final SubsectionType subSection = subSections.get(j); |
579 |
0
|
if (!(subSection instanceof Subsection)) { |
580 |
0
|
hasFormalContent = true; |
581 |
0
|
break; |
582 |
|
} |
583 |
|
} |
584 |
|
} |
585 |
|
} while (false); |
586 |
0
|
if (!hasFormalContent) { |
587 |
0
|
setBlocked(true); |
588 |
0
|
return; |
589 |
|
} |
590 |
|
} |
591 |
146
|
printer.print("\\chapter"); |
592 |
146
|
if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) { |
593 |
34
|
printer.print("*"); |
594 |
|
} |
595 |
146
|
printer.print("{"); |
596 |
146
|
printer.print(getLatexListEntry("getTitle()", chapter.getTitle())); |
597 |
146
|
final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber(); |
598 |
146
|
printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}"); |
599 |
146
|
if (chapter.getNoNumber() != null && chapter.getNoNumber().booleanValue()) { |
600 |
34
|
printer.println("\\addcontentsline{toc}{chapter}{" |
601 |
|
+ getLatexListEntry("getTitle()", chapter.getTitle()) + "}"); |
602 |
|
} |
603 |
146
|
printer.println(); |
604 |
146
|
if (chapter.getIntroduction() != null && !brief) { |
605 |
146
|
printer.println(getLatexListEntry("getIntroduction()", chapter.getIntroduction())); |
606 |
146
|
printer.println(); |
607 |
|
} |
608 |
|
} |
609 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0.33 |
|
610 |
146
|
public void visitLeave(final Chapter chapter) {... |
611 |
146
|
printer.println("%% end of chapter " + getLatexListEntry("getTitle()", chapter.getTitle())); |
612 |
146
|
printer.println(); |
613 |
146
|
setBlocked(false); |
614 |
|
} |
615 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
616 |
104
|
public void visitLeave(final SectionList list) {... |
617 |
104
|
printer.println(); |
618 |
|
} |
619 |
|
|
|
|
| 34.2% |
Uncovered Elements: 25 (38) |
Complexity: 10 |
Complexity Density: 0.42 |
|
620 |
280
|
public void visitEnter(final Section section) {... |
621 |
|
|
622 |
280
|
if (brief) { |
623 |
0
|
boolean hasFormalContent = false; |
624 |
0
|
do { |
625 |
0
|
final SubsectionList subSections = section.getSubsectionList(); |
626 |
0
|
if (subSections == null) { |
627 |
0
|
break; |
628 |
|
} |
629 |
0
|
for (int j = 0; j < subSections.size(); j++) { |
630 |
0
|
final SubsectionType subSection = subSections.get(j); |
631 |
0
|
if (!(subSection instanceof Subsection)) { |
632 |
0
|
hasFormalContent = true; |
633 |
0
|
break; |
634 |
|
} |
635 |
|
} |
636 |
|
} while (false); |
637 |
0
|
if (!hasFormalContent) { |
638 |
0
|
setBlocked(true); |
639 |
0
|
return; |
640 |
|
} |
641 |
|
} |
642 |
280
|
printer.print("\\section"); |
643 |
280
|
if (section.getNoNumber() != null && section.getNoNumber().booleanValue()) { |
644 |
0
|
printer.print("*"); |
645 |
|
} |
646 |
280
|
printer.print("{"); |
647 |
280
|
printer.print(getLatexListEntry("getTitle()", section.getTitle())); |
648 |
280
|
final String chapterLabel = "chapter" + getCurrentNumbers().getAbsoluteChapterNumber() |
649 |
|
+ "_section" + getCurrentNumbers().getAbsoluteSectionNumber(); |
650 |
280
|
printer.println("} \\label{" + chapterLabel + "} \\hypertarget{" + chapterLabel + "}{}"); |
651 |
280
|
if (section.getIntroduction() != null && !brief) { |
652 |
280
|
printer.println(getLatexListEntry("getIntroduction()", section.getIntroduction())); |
653 |
280
|
printer.println(); |
654 |
|
} |
655 |
|
} |
656 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
657 |
280
|
public void visitLeave(final Section section) {... |
658 |
280
|
setBlocked(false); |
659 |
|
} |
660 |
|
|
|
|
| 86.7% |
Uncovered Elements: 2 (15) |
Complexity: 4 |
Complexity Density: 0.44 |
|
661 |
108
|
public void visitEnter(final Subsection subsection) {... |
662 |
|
|
663 |
|
|
664 |
|
|
665 |
|
|
666 |
|
|
667 |
|
|
668 |
|
|
669 |
|
|
670 |
108
|
if (brief) { |
671 |
0
|
return; |
672 |
|
} |
673 |
108
|
if (subsection.getTitle() != null) { |
674 |
68
|
printer.print("\\subsection{"); |
675 |
68
|
printer.println(getLatexListEntry("getTitle()", subsection.getTitle())); |
676 |
68
|
printer.println("}"); |
677 |
|
} |
678 |
108
|
if (subsection.getId() != null) { |
679 |
4
|
printer.println("\\label{" + subsection.getId() + "} \\hypertarget{" |
680 |
|
+ subsection.getId() + "}{}"); |
681 |
|
} |
682 |
108
|
printer.println(getLatexListEntry("getLatex()", subsection.getLatex())); |
683 |
|
} |
684 |
|
|
|
|
| 66.7% |
Uncovered Elements: 2 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
685 |
108
|
public void visitLeave(final Subsection subsection) {... |
686 |
108
|
if (brief) { |
687 |
0
|
return; |
688 |
|
} |
689 |
108
|
printer.println(); |
690 |
108
|
printer.println(); |
691 |
|
} |
692 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (12) |
Complexity: 4 |
Complexity Density: 0.5 |
|
693 |
992
|
public void visitEnter(final Node node) {... |
694 |
|
|
695 |
|
|
696 |
|
|
697 |
|
|
698 |
|
|
699 |
992
|
if (node.getPrecedingText() != null && !brief) { |
700 |
502
|
printer.println("\\par"); |
701 |
502
|
printer.println(getLatexListEntry("getPrecedingText()", node.getPrecedingText())); |
702 |
502
|
printer.println(); |
703 |
|
} |
704 |
992
|
id = node.getId(); |
705 |
992
|
title = null; |
706 |
992
|
if (node.getTitle() != null) { |
707 |
552
|
title = getLatexListEntry("getTitle()", node.getTitle()); |
708 |
|
} |
709 |
|
} |
710 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (7) |
Complexity: 3 |
Complexity Density: 0.6 |
|
711 |
992
|
public void visitLeave(final Node node) {... |
712 |
992
|
printer.println(); |
713 |
992
|
if (node.getSucceedingText() != null && !brief) { |
714 |
144
|
printer.println(getLatexListEntry("getSucceedingText()", node.getSucceedingText())); |
715 |
144
|
printer.println(); |
716 |
|
} |
717 |
992
|
printer.println(); |
718 |
|
} |
719 |
|
|
|
|
| 81.8% |
Uncovered Elements: 2 (11) |
Complexity: 3 |
Complexity Density: 0.43 |
|
720 |
236
|
public void visitEnter(final Axiom axiom) {... |
721 |
236
|
printer.println("\\begin{ax}" + (title != null ? "[" + title + "]" : "")); |
722 |
236
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
723 |
236
|
if (info) { |
724 |
236
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
725 |
|
} |
726 |
236
|
printFormula(axiom.getFormula().getElement()); |
727 |
236
|
printer.println(getLatexListEntry("getDescription()", axiom.getDescription())); |
728 |
236
|
printer.println("\\end{ax}"); |
729 |
|
} |
730 |
|
|
|
|
| 90.9% |
Uncovered Elements: 1 (11) |
Complexity: 3 |
Complexity Density: 0.43 |
|
731 |
444
|
public void visitEnter(final Proposition proposition) {... |
732 |
444
|
printer.println("\\begin{prop}" + (title != null ? "[" + title + "]" : "")); |
733 |
444
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
734 |
444
|
if (info) { |
735 |
444
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
736 |
|
} |
737 |
444
|
printTopFormula(proposition.getFormula().getElement(), id); |
738 |
444
|
printer.println(getLatexListEntry("getDescription()", proposition.getDescription())); |
739 |
444
|
printer.println("\\end{prop}"); |
740 |
|
} |
741 |
|
|
|
|
| 62.5% |
Uncovered Elements: 3 (8) |
Complexity: 2 |
Complexity Density: 0.33 |
|
742 |
88
|
public void visitEnter(final Proof proof) {... |
743 |
|
|
744 |
|
|
745 |
|
|
746 |
|
|
747 |
|
|
748 |
|
|
749 |
|
|
750 |
|
|
751 |
88
|
if (brief) { |
752 |
0
|
setBlocked(true); |
753 |
0
|
return; |
754 |
|
} |
755 |
88
|
printer.println("\\begin{proof}"); |
756 |
88
|
printer.println(getLatexListEntry("getNonFormalProof()", proof.getNonFormalProof())); |
757 |
88
|
printer.println("\\end{proof}"); |
758 |
|
} |
759 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
760 |
88
|
public void visitLeave(final Proof proof) {... |
761 |
88
|
setBlocked(false); |
762 |
|
} |
763 |
|
|
|
|
| 57.1% |
Uncovered Elements: 3 (7) |
Complexity: 2 |
Complexity Density: 0.4 |
|
764 |
196
|
public void visitEnter(final FormalProof proof) {... |
765 |
196
|
if (brief) { |
766 |
0
|
setBlocked(true); |
767 |
0
|
return; |
768 |
|
} |
769 |
196
|
tabLevel = 0; |
770 |
196
|
printer.println("\\begin{proof}"); |
771 |
|
|
772 |
|
|
773 |
|
|
774 |
|
|
775 |
|
|
776 |
|
} |
777 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
778 |
396
|
public void visitEnter(final FormalProofLineList lines) {... |
779 |
396
|
if (tabLevel == 0) { |
780 |
196
|
printer.println("\\mbox{}\\\\"); |
781 |
196
|
printer.println("\\begin{longtable}[h!]{r@{\\extracolsep{\\fill}}p{9cm}@{\\extracolsep{\\fill}}p{4cm}}"); |
782 |
|
} |
783 |
|
} |
784 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
785 |
396
|
public void visitLeave(final FormalProofLineList lines) {... |
786 |
396
|
if (tabLevel == 0) { |
787 |
196
|
printer.println(" & & \\qedhere"); |
788 |
196
|
printer.println("\\end{longtable}"); |
789 |
|
} |
790 |
|
} |
791 |
|
|
|
|
| 73.3% |
Uncovered Elements: 4 (15) |
Complexity: 4 |
Complexity Density: 0.44 |
|
792 |
2026
|
public void visitEnter(final FormalProofLine line) {... |
793 |
2026
|
if (line.getLabel() != null) { |
794 |
2022
|
label = line.getLabel(); |
795 |
|
} else { |
796 |
4
|
label = ""; |
797 |
|
} |
798 |
2026
|
if (line.getFormula() != null) { |
799 |
2026
|
formula = "$" + getQedeqBo().getElement2Latex().getLatex(line.getFormula().getElement()) + "$"; |
800 |
|
} else { |
801 |
0
|
formula = ""; |
802 |
|
} |
803 |
2026
|
if (line.getReason() != null) { |
804 |
2026
|
reason = line.getReason().toString(); |
805 |
|
} else { |
806 |
0
|
reason = ""; |
807 |
|
} |
808 |
|
} |
809 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
810 |
2026
|
public void visitLeave(final FormalProofLine line) {... |
811 |
2026
|
if (brief) { |
812 |
0
|
return; |
813 |
|
} |
814 |
2026
|
linePrintln(); |
815 |
|
} |
816 |
|
|
817 |
|
|
818 |
|
|
819 |
|
|
|
|
| 86.2% |
Uncovered Elements: 4 (29) |
Complexity: 7 |
Complexity Density: 0.37 |
|
820 |
2426
|
private void linePrintln() {... |
821 |
2426
|
if (formula.length() == 0 && reason.length() == 0) { |
822 |
0
|
return; |
823 |
|
} |
824 |
2426
|
if (label.length() > 0) { |
825 |
2422
|
String display = getNodeBo().getNodeVo().getId() + "!" + label; |
826 |
2422
|
printer.print("\\label{" + display + "} \\hypertarget{" + display |
827 |
|
+ "}{\\mbox{(" + label + ")}} "); |
828 |
|
} |
829 |
2426
|
printer.print(" \\ & \\ "); |
830 |
3494
|
for (int i = 0; i < tabLevel; i++) { |
831 |
1068
|
printer.print("\\mbox{\\qquad}"); |
832 |
|
} |
833 |
2426
|
if (formula.length() > 0) { |
834 |
2426
|
printer.print(formula); |
835 |
|
} |
836 |
2426
|
printer.print(" \\ & \\ "); |
837 |
2426
|
if (reason.length() > 0) { |
838 |
2426
|
printer.print("{\\tiny "); |
839 |
2426
|
printer.print(reason); |
840 |
2426
|
printer.print("}"); |
841 |
|
} |
842 |
2426
|
printer.println(" \\\\ "); |
843 |
2426
|
reason = ""; |
844 |
2426
|
formula = ""; |
845 |
2426
|
label = ""; |
846 |
|
} |
847 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
848 |
1374
|
private String getReference(final String reference) {... |
849 |
1374
|
return getReference(reference, "getReference()"); |
850 |
|
} |
851 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0.2 |
|
852 |
2538
|
private String getReference(final String reference, final String subContext) {... |
853 |
2538
|
final String context = getCurrentContext().getLocationWithinModule(); |
854 |
2538
|
try { |
855 |
2538
|
getCurrentContext().setLocationWithinModule(context + "." + subContext); |
856 |
2538
|
return (getReference(reference, null, null)); |
857 |
|
} finally { |
858 |
2538
|
getCurrentContext().setLocationWithinModule(context); |
859 |
|
} |
860 |
|
} |
861 |
|
|
|
|
| 84.2% |
Uncovered Elements: 3 (19) |
Complexity: 5 |
Complexity Density: 0.45 |
|
862 |
592
|
public void visitEnter(final ModusPonens r) throws ModuleDataException {... |
863 |
592
|
if (brief) { |
864 |
0
|
return; |
865 |
|
} |
866 |
592
|
reason = getRuleReference(r.getName()); |
867 |
592
|
boolean one = false; |
868 |
592
|
if (r.getReference1() != null) { |
869 |
576
|
reason += " " + getReference(r.getReference1(), "getReference1()"); |
870 |
576
|
one = true; |
871 |
|
} |
872 |
592
|
if (r.getReference1() != null) { |
873 |
576
|
if (one) { |
874 |
576
|
reason += ","; |
875 |
|
} |
876 |
576
|
reason += " " + getReference(r.getReference2(), "getReference2()"); |
877 |
|
} |
878 |
|
} |
879 |
|
|
|
|
| 77.8% |
Uncovered Elements: 2 (9) |
Complexity: 3 |
Complexity Density: 0.6 |
|
880 |
454
|
public void visitEnter(final Add r) throws ModuleDataException {... |
881 |
454
|
if (brief) { |
882 |
0
|
return; |
883 |
|
} |
884 |
454
|
reason = getRuleReference(r.getName()); |
885 |
454
|
if (r.getReference() != null) { |
886 |
450
|
reason += " " + getReference(r.getReference()); |
887 |
|
} |
888 |
|
} |
889 |
|
|
|
|
| 88.2% |
Uncovered Elements: 2 (17) |
Complexity: 5 |
Complexity Density: 0.56 |
|
890 |
86
|
public void visitEnter(final Rename r) throws ModuleDataException {... |
891 |
86
|
if (brief) { |
892 |
0
|
return; |
893 |
|
} |
894 |
86
|
reason = getRuleReference(r.getName()); |
895 |
86
|
if (r.getOriginalSubjectVariable() != null) { |
896 |
74
|
reason += " $" + getQedeqBo().getElement2Latex().getLatex( |
897 |
|
r.getOriginalSubjectVariable()) + "$"; |
898 |
|
} |
899 |
86
|
if (r.getReplacementSubjectVariable() != null) { |
900 |
66
|
reason += " by $" + getQedeqBo().getElement2Latex().getLatex( |
901 |
|
r.getReplacementSubjectVariable()) + "$"; |
902 |
|
} |
903 |
86
|
if (r.getReference() != null) { |
904 |
74
|
reason += " in " + getReference(r.getReference()); |
905 |
|
} |
906 |
|
} |
907 |
|
|
|
|
| 88.2% |
Uncovered Elements: 2 (17) |
Complexity: 5 |
Complexity Density: 0.56 |
|
908 |
50
|
public void visitEnter(final SubstFree r) throws ModuleDataException {... |
909 |
50
|
if (brief) { |
910 |
0
|
return; |
911 |
|
} |
912 |
50
|
reason = getRuleReference(r.getName()); |
913 |
50
|
if (r.getSubjectVariable() != null) { |
914 |
34
|
reason += " $" + getQedeqBo().getElement2Latex().getLatex( |
915 |
|
r.getSubjectVariable()) + "$"; |
916 |
|
} |
917 |
50
|
if (r.getSubstituteTerm() != null) { |
918 |
46
|
reason += " by $" + getQedeqBo().getElement2Latex().getLatex( |
919 |
|
r.getSubstituteTerm()) + "$"; |
920 |
|
} |
921 |
50
|
if (r.getReference() != null) { |
922 |
46
|
reason += " in " + getReference(r.getReference()); |
923 |
|
} |
924 |
|
} |
925 |
|
|
|
|
| 88.2% |
Uncovered Elements: 2 (17) |
Complexity: 5 |
Complexity Density: 0.56 |
|
926 |
16
|
public void visitEnter(final SubstFunc r) throws ModuleDataException {... |
927 |
16
|
if (brief) { |
928 |
0
|
return; |
929 |
|
} |
930 |
16
|
reason = getRuleReference(r.getName()); |
931 |
16
|
if (r.getFunctionVariable() != null) { |
932 |
8
|
reason += " $" + getQedeqBo().getElement2Latex().getLatex( |
933 |
|
r.getFunctionVariable()) + "$"; |
934 |
|
} |
935 |
16
|
if (r.getSubstituteTerm() != null) { |
936 |
12
|
reason += " by $" + getQedeqBo().getElement2Latex().getLatex( |
937 |
|
r.getSubstituteTerm()) + "$"; |
938 |
|
} |
939 |
16
|
if (r.getReference() != null) { |
940 |
12
|
reason += " in " + getReference(r.getReference()); |
941 |
|
} |
942 |
|
} |
943 |
|
|
|
|
| 88.2% |
Uncovered Elements: 2 (17) |
Complexity: 5 |
Complexity Density: 0.56 |
|
944 |
778
|
public void visitEnter(final SubstPred r) throws ModuleDataException {... |
945 |
778
|
if (brief) { |
946 |
0
|
return; |
947 |
|
} |
948 |
778
|
reason = getRuleReference(r.getName()); |
949 |
778
|
if (r.getPredicateVariable() != null) { |
950 |
742
|
reason += " $" + getQedeqBo().getElement2Latex().getLatex( |
951 |
|
r.getPredicateVariable()) + "$"; |
952 |
|
} |
953 |
778
|
if (r.getSubstituteFormula() != null) { |
954 |
742
|
reason += " by $" + getQedeqBo().getElement2Latex().getLatex( |
955 |
|
r.getSubstituteFormula()) + "$"; |
956 |
|
} |
957 |
778
|
if (r.getReference() != null) { |
958 |
746
|
reason += " in " + getReference(r.getReference()); |
959 |
|
} |
960 |
|
} |
961 |
|
|
|
|
| 76.9% |
Uncovered Elements: 3 (13) |
Complexity: 4 |
Complexity Density: 0.57 |
|
962 |
10
|
public void visitEnter(final Existential r) throws ModuleDataException {... |
963 |
10
|
if (brief) { |
964 |
0
|
return; |
965 |
|
} |
966 |
10
|
reason = getRuleReference(r.getName()); |
967 |
10
|
if (r.getSubjectVariable() != null) { |
968 |
6
|
reason += " with $" + getQedeqBo().getElement2Latex().getLatex( |
969 |
|
r.getSubjectVariable()) + "$"; |
970 |
|
} |
971 |
10
|
if (r.getReference() != null) { |
972 |
10
|
reason += " in " + getReference(r.getReference()); |
973 |
|
} |
974 |
|
} |
975 |
|
|
|
|
| 84.6% |
Uncovered Elements: 2 (13) |
Complexity: 4 |
Complexity Density: 0.57 |
|
976 |
40
|
public void visitEnter(final Universal r) throws ModuleDataException {... |
977 |
40
|
if (brief) { |
978 |
0
|
return; |
979 |
|
} |
980 |
40
|
reason = getRuleReference(r.getName()); |
981 |
40
|
if (r.getSubjectVariable() != null) { |
982 |
28
|
reason += " with $" + getQedeqBo().getElement2Latex().getLatex( |
983 |
|
r.getSubjectVariable()) + "$"; |
984 |
|
} |
985 |
40
|
if (r.getReference() != null) { |
986 |
36
|
reason += " in " + getReference(r.getReference()); |
987 |
|
} |
988 |
|
} |
989 |
|
|
|
|
| 85.7% |
Uncovered Elements: 2 (14) |
Complexity: 3 |
Complexity Density: 0.3 |
|
990 |
200
|
public void visitEnter(final ConditionalProof r) throws ModuleDataException {... |
991 |
200
|
if (brief) { |
992 |
0
|
return; |
993 |
|
} |
994 |
200
|
reason = getRuleReference(r.getName()); |
995 |
200
|
printer.print(" \\ & \\ "); |
996 |
304
|
for (int i = 0; i < tabLevel; i++) { |
997 |
104
|
printer.print("\\mbox{\\qquad}"); |
998 |
|
} |
999 |
200
|
printer.println("Conditional Proof"); |
1000 |
200
|
printer.print(" \\ & \\ "); |
1001 |
200
|
printer.println(" \\\\ "); |
1002 |
200
|
tabLevel++; |
1003 |
|
} |
1004 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1005 |
200
|
public void visitLeave(final ConditionalProof proof) {... |
1006 |
200
|
if (brief) { |
1007 |
0
|
return; |
1008 |
|
} |
1009 |
200
|
tabLevel--; |
1010 |
|
} |
1011 |
|
|
|
|
| 69.2% |
Uncovered Elements: 4 (13) |
Complexity: 4 |
Complexity Density: 0.57 |
|
1012 |
200
|
public void visitEnter(final Hypothesis hypothesis) {... |
1013 |
200
|
if (brief) { |
1014 |
0
|
return; |
1015 |
|
} |
1016 |
200
|
reason = "Hypothesis"; |
1017 |
200
|
if (hypothesis.getLabel() != null) { |
1018 |
200
|
label = hypothesis.getLabel(); |
1019 |
|
} |
1020 |
200
|
if (hypothesis.getFormula() != null) { |
1021 |
200
|
formula = "$" + getQedeqBo().getElement2Latex().getLatex( |
1022 |
|
hypothesis.getFormula().getElement()) + "$"; |
1023 |
|
} |
1024 |
|
} |
1025 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1026 |
200
|
public void visitLeave(final Hypothesis hypothesis) {... |
1027 |
200
|
if (brief) { |
1028 |
0
|
return; |
1029 |
|
} |
1030 |
200
|
linePrintln(); |
1031 |
|
} |
1032 |
|
|
|
|
| 71.4% |
Uncovered Elements: 4 (14) |
Complexity: 4 |
Complexity Density: 0.5 |
|
1033 |
200
|
public void visitEnter(final Conclusion conclusion) {... |
1034 |
200
|
if (brief) { |
1035 |
0
|
return; |
1036 |
|
} |
1037 |
200
|
tabLevel--; |
1038 |
200
|
reason = "Conclusion"; |
1039 |
200
|
if (conclusion.getLabel() != null) { |
1040 |
200
|
label = conclusion.getLabel(); |
1041 |
|
} |
1042 |
200
|
if (conclusion.getFormula() != null) { |
1043 |
200
|
formula = "$" + getQedeqBo().getElement2Latex().getLatex( |
1044 |
|
conclusion.getFormula().getElement()) + "$"; |
1045 |
|
} |
1046 |
|
} |
1047 |
|
|
|
|
| 66.7% |
Uncovered Elements: 2 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
1048 |
200
|
public void visitLeave(final Conclusion conclusion) {... |
1049 |
200
|
if (brief) { |
1050 |
0
|
return; |
1051 |
|
} |
1052 |
200
|
linePrintln(); |
1053 |
200
|
tabLevel++; |
1054 |
|
} |
1055 |
|
|
|
|
| 80% |
Uncovered Elements: 1 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1056 |
196
|
public void visitLeave(final FormalProof proof) {... |
1057 |
196
|
if (!getBlocked()) { |
1058 |
196
|
printer.println("\\end{proof}"); |
1059 |
|
} |
1060 |
196
|
setBlocked(false); |
1061 |
|
} |
1062 |
|
|
|
|
| 84.6% |
Uncovered Elements: 2 (13) |
Complexity: 3 |
Complexity Density: 0.33 |
|
1063 |
20
|
public void visitEnter(final InitialPredicateDefinition definition) {... |
1064 |
20
|
printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : "")); |
1065 |
20
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1066 |
20
|
if (info) { |
1067 |
20
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1068 |
|
} |
1069 |
20
|
printer.print("$$"); |
1070 |
20
|
printer.println(getLatex(definition.getPredCon())); |
1071 |
20
|
printer.println("$$"); |
1072 |
20
|
printer.println(getLatexListEntry("getDescription()", definition.getDescription())); |
1073 |
20
|
printer.println("\\end{idefn}"); |
1074 |
|
} |
1075 |
|
|
|
|
| 84.6% |
Uncovered Elements: 2 (13) |
Complexity: 3 |
Complexity Density: 0.33 |
|
1076 |
48
|
public void visitEnter(final PredicateDefinition definition) {... |
1077 |
48
|
printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : "")); |
1078 |
48
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1079 |
48
|
if (info) { |
1080 |
48
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1081 |
|
} |
1082 |
48
|
printer.print("$$"); |
1083 |
48
|
printer.print(getLatex(definition.getFormula().getElement())); |
1084 |
48
|
printer.println("$$"); |
1085 |
48
|
printer.println(getLatexListEntry("getDescription()", definition.getDescription())); |
1086 |
48
|
printer.println("\\end{defn}"); |
1087 |
|
} |
1088 |
|
|
|
|
| 0% |
Uncovered Elements: 13 (13) |
Complexity: 3 |
Complexity Density: 0.33 |
|
1089 |
0
|
public void visitEnter(final InitialFunctionDefinition definition) {... |
1090 |
0
|
printer.println("\\begin{idefn}" + (title != null ? "[" + title + "]" : "")); |
1091 |
0
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1092 |
0
|
if (info) { |
1093 |
0
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1094 |
|
} |
1095 |
0
|
printer.print("$$"); |
1096 |
0
|
printer.print(getLatex(definition.getFunCon())); |
1097 |
0
|
printer.println("$$"); |
1098 |
0
|
printer.println(getLatexListEntry("getDescription()", definition.getDescription())); |
1099 |
0
|
printer.println("\\end{defn}"); |
1100 |
|
} |
1101 |
|
|
|
|
| 83.3% |
Uncovered Elements: 2 (12) |
Complexity: 3 |
Complexity Density: 0.38 |
|
1102 |
64
|
public void visitEnter(final FunctionDefinition definition) {... |
1103 |
64
|
printer.println("\\begin{defn}" + (title != null ? "[" + title + "]" : "")); |
1104 |
64
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1105 |
64
|
if (info) { |
1106 |
64
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1107 |
|
} |
1108 |
64
|
printer.print("$$"); |
1109 |
64
|
printer.print(getLatex(definition.getFormula().getElement())); |
1110 |
64
|
printer.println("$$"); |
1111 |
64
|
printer.println("\\end{defn}"); |
1112 |
|
} |
1113 |
|
|
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
1114 |
64
|
public void visitLeave(final FunctionDefinition definition) {... |
1115 |
|
|
1116 |
|
} |
1117 |
|
|
|
|
| 84.2% |
Uncovered Elements: 3 (19) |
Complexity: 5 |
Complexity Density: 0.45 |
|
1118 |
180
|
public void visitEnter(final Rule rule) {... |
1119 |
180
|
printer.println("\\begin{rul}" + (title != null ? "[" + title + "]" : "")); |
1120 |
180
|
printer.println("\\label{" + id + "} \\hypertarget{" + id + "}{}"); |
1121 |
180
|
if (info) { |
1122 |
180
|
printer.println("{\\tt \\tiny [\\verb]" + id + "]]}"); |
1123 |
|
} |
1124 |
180
|
printer.println(); |
1125 |
180
|
printer.println("\\par"); |
1126 |
180
|
printer.println("{\\em " |
1127 |
180
|
+ (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "") |
1128 |
180
|
+ (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : "") |
1129 |
|
+ "}"); |
1130 |
180
|
printer.println(); |
1131 |
180
|
printer.println(); |
1132 |
180
|
printer.println(getLatexListEntry("getDescription()", rule.getDescription())); |
1133 |
180
|
printer.println("\\end{rul}"); |
1134 |
|
} |
1135 |
|
|
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
1136 |
180
|
public void visitLeave(final Rule rule) {... |
1137 |
|
|
1138 |
|
} |
1139 |
|
|
|
|
| 77.3% |
Uncovered Elements: 5 (22) |
Complexity: 6 |
Complexity Density: 0.5 |
|
1140 |
8
|
public void visitEnter(final LinkList linkList) {... |
1141 |
8
|
if (linkList.size() <= 0) { |
1142 |
0
|
return; |
1143 |
|
} |
1144 |
8
|
if ("de".equals(language)) { |
1145 |
4
|
printer.println("Basierend auf: "); |
1146 |
|
} else { |
1147 |
4
|
if (!"en".equals(language)) { |
1148 |
0
|
printer.println("%%% TODO unknown language: " + language); |
1149 |
|
} |
1150 |
4
|
printer.println("Based on: "); |
1151 |
|
} |
1152 |
20
|
for (int i = 0; i < linkList.size(); i++) { |
1153 |
12
|
if (linkList.get(i) != null) { |
1154 |
12
|
printer.print(" " + getReference(linkList.get(i), "get(" + i + ")")); |
1155 |
|
} |
1156 |
8
|
}; |
1157 |
8
|
printer.println(); |
1158 |
|
} |
1159 |
|
|
|
|
| 71.4% |
Uncovered Elements: 4 (14) |
Complexity: 4 |
Complexity Density: 0.5 |
|
1160 |
4
|
public void visitEnter(final ChangedRuleList list) {... |
1161 |
4
|
if (list.size() <= 0) { |
1162 |
0
|
return; |
1163 |
|
} |
1164 |
4
|
if ("de".equals(language)) { |
1165 |
2
|
printer.println("Die folgenden Regeln m\u00fcssen erweitert werden."); |
1166 |
|
} else { |
1167 |
2
|
if (!"en".equals(language)) { |
1168 |
0
|
printer.println("%%% TODO unknown language: " + language); |
1169 |
|
} |
1170 |
2
|
printer.println("The following rules have to be extended."); |
1171 |
|
} |
1172 |
4
|
printer.println(); |
1173 |
|
} |
1174 |
|
|
|
|
| 76% |
Uncovered Elements: 6 (25) |
Complexity: 7 |
Complexity Density: 0.47 |
|
1175 |
32
|
public void visitEnter(final ChangedRule rule) {... |
1176 |
32
|
printer.println("\\par"); |
1177 |
32
|
printer.println("\\label{" + id + "!" + rule.getName() + "} \\hypertarget{" + id + "!" |
1178 |
|
+ rule.getName() + "}{}"); |
1179 |
32
|
printer.print("{\\em " |
1180 |
32
|
+ (rule.getName() != null ? " Name: \\verb]" + rule.getName() + "]" : "") |
1181 |
32
|
+ (rule.getVersion() != null ? " - Version: \\verb]" + rule.getVersion() + "]" : "")); |
1182 |
32
|
RuleKey old = getLocalRuleKey(rule.getName()); |
1183 |
32
|
if (old == null && getQedeqBo().getExistenceChecker() != null) { |
1184 |
0
|
old = getQedeqBo().getExistenceChecker().getParentRuleKey(rule.getName()); |
1185 |
|
} |
1186 |
32
|
if (old != null) { |
1187 |
32
|
printer.print(" - Old Version: " |
1188 |
|
+ getRuleReference(rule.getName(), old.getVersion())); |
1189 |
|
} |
1190 |
32
|
printer.println("}"); |
1191 |
32
|
rule.getName(); |
1192 |
32
|
printer.println(); |
1193 |
32
|
if (rule.getDescription() != null) { |
1194 |
32
|
printer.println(getLatexListEntry("getDescription()", rule.getDescription())); |
1195 |
32
|
printer.println(); |
1196 |
32
|
printer.println(); |
1197 |
|
} |
1198 |
|
} |
1199 |
|
|
1200 |
|
|
|
|
| 91.7% |
Uncovered Elements: 3 (36) |
Complexity: 9 |
Complexity Density: 0.35 |
|
1201 |
14
|
public void visitEnter(final LiteratureItemList list) {... |
1202 |
14
|
printer.println("\\backmatter"); |
1203 |
14
|
printer.println(); |
1204 |
14
|
printer.println("\\begin{thebibliography}{99}"); |
1205 |
14
|
if ("de".equals(language)) { |
1206 |
6
|
printer.println("\\addcontentsline{toc}{chapter}{Literaturverzeichnis}"); |
1207 |
|
} else { |
1208 |
8
|
if (!"en".equals(language)) { |
1209 |
0
|
printer.println("%%% TODO unknown language: " + language); |
1210 |
|
} |
1211 |
8
|
printer.println("\\addcontentsline{toc}{chapter}{Bibliography}"); |
1212 |
|
} |
1213 |
14
|
final ImportList imports = getQedeqBo().getQedeq().getHeader().getImportList(); |
1214 |
14
|
if (imports != null && imports.size() > 0) { |
1215 |
6
|
printer.println(); |
1216 |
6
|
printer.println(); |
1217 |
6
|
printer.println("%% Used other QEDEQ modules:"); |
1218 |
14
|
for (int i = 0; i < imports.size(); i++) { |
1219 |
8
|
final Import imp = imports.get(i); |
1220 |
8
|
printer.print("\\bibitem{" + imp.getLabel() + "} "); |
1221 |
8
|
final Specification spec = imp.getSpecification(); |
1222 |
8
|
printer.print(getLatex(spec.getName())); |
1223 |
8
|
if (spec.getLocationList() != null && spec.getLocationList().size() > 0 |
1224 |
|
&& spec.getLocationList().get(0).getLocation().length() > 0) { |
1225 |
8
|
printer.print(" "); |
1226 |
|
|
1227 |
|
|
1228 |
|
|
1229 |
|
|
1230 |
|
|
1231 |
8
|
printer.print("\\url{" + getPdfLink((KernelQedeqBo) getQedeqBo() |
1232 |
|
.getLabels().getReferences().getQedeqBo(imp.getLabel())) + "}"); |
1233 |
|
} |
1234 |
8
|
printer.println(); |
1235 |
|
} |
1236 |
6
|
printer.println(); |
1237 |
6
|
printer.println(); |
1238 |
6
|
printer.println("%% Other references:"); |
1239 |
6
|
printer.println(); |
1240 |
|
} |
1241 |
|
} |
1242 |
|
|
|
|
| 95.7% |
Uncovered Elements: 1 (23) |
Complexity: 6 |
Complexity Density: 0.35 |
|
1243 |
14
|
public void visitLeave(final LiteratureItemList list) {... |
1244 |
14
|
final UsedByList usedby = getQedeqBo().getQedeq().getHeader().getUsedByList(); |
1245 |
14
|
if (usedby != null && usedby.size() > 0) { |
1246 |
8
|
printer.println(); |
1247 |
8
|
printer.println(); |
1248 |
8
|
printer.println("%% QEDEQ modules that use this one:"); |
1249 |
16
|
for (int i = 0; i < usedby.size(); i++) { |
1250 |
8
|
final Specification spec = usedby.get(i); |
1251 |
8
|
printer.print("\\bibitem{" + spec.getName() + "} "); |
1252 |
8
|
printer.print(getLatex(spec.getName())); |
1253 |
8
|
final String url = getUrl(getQedeqBo().getModuleAddress(), spec); |
1254 |
8
|
if (url != null && url.length() > 0) { |
1255 |
8
|
printer.print(" "); |
1256 |
8
|
printer.print("\\url{" + url + "}"); |
1257 |
|
} |
1258 |
8
|
printer.println(); |
1259 |
|
} |
1260 |
8
|
printer.println(); |
1261 |
8
|
printer.println(); |
1262 |
|
} |
1263 |
14
|
printer.println("\\end{thebibliography}"); |
1264 |
|
} |
1265 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0.33 |
|
1266 |
56
|
public void visitEnter(final LiteratureItem item) {... |
1267 |
56
|
printer.print("\\bibitem{" + item.getLabel() + "} "); |
1268 |
56
|
printer.println(getLatexListEntry("getItem()", item.getItem())); |
1269 |
56
|
printer.println(); |
1270 |
|
} |
1271 |
|
|
1272 |
|
|
1273 |
|
|
1274 |
|
|
1275 |
|
|
1276 |
|
@param |
1277 |
|
@param |
1278 |
|
|
|
|
| 92.3% |
Uncovered Elements: 2 (26) |
Complexity: 7 |
Complexity Density: 0.44 |
|
1279 |
444
|
private void printTopFormula(final Element element, final String mainLabel) {... |
1280 |
444
|
if (!element.isList() || !element.getList().getOperator().equals("AND")) { |
1281 |
372
|
printFormula(element); |
1282 |
372
|
return; |
1283 |
|
} |
1284 |
72
|
final ElementList list = element.getList(); |
1285 |
72
|
printer.println("\\mbox{}"); |
1286 |
72
|
printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{0.9\\linewidth}l}}"); |
1287 |
608
|
for (int i = 0; i < list.size(); i++) { |
1288 |
536
|
String newLabel = ""; |
1289 |
536
|
if (list.size() >= ALPHABET.length() * ALPHABET.length()) { |
1290 |
0
|
newLabel = "" + (i + 1); |
1291 |
|
} else { |
1292 |
|
|
1293 |
536
|
if (list.size() > ALPHABET.length()) { |
1294 |
160
|
final int div = (i / ALPHABET.length()); |
1295 |
160
|
newLabel = "" + ALPHABET.charAt(div); |
1296 |
|
} |
1297 |
536
|
newLabel += ALPHABET.charAt(i % ALPHABET.length()); |
1298 |
|
} |
1299 |
|
|
1300 |
536
|
printer.println("\\centering $" + getLatex(list.getElement(i)) + "$" |
1301 |
|
+ " & \\label{" + mainLabel + "/" + newLabel + "} \\hypertarget{" + mainLabel + "/" |
1302 |
|
+ newLabel + "}{} \\mbox{\\emph{(" + newLabel + ")}} " |
1303 |
536
|
+ (i + 1 < list.size() ? "\\\\" : "")); |
1304 |
|
} |
1305 |
72
|
printer.println("\\end{longtable}"); |
1306 |
|
} |
1307 |
|
|
1308 |
|
|
1309 |
|
|
1310 |
|
|
1311 |
|
@param |
1312 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0.25 |
|
1313 |
608
|
private void printFormula(final Element element) {... |
1314 |
608
|
printer.println("\\mbox{}"); |
1315 |
608
|
printer.println("\\begin{longtable}{{@{\\extracolsep{\\fill}}p{\\linewidth}}}"); |
1316 |
608
|
printer.println("\\centering $" + getLatex(element) + "$"); |
1317 |
608
|
printer.println("\\end{longtable}"); |
1318 |
|
} |
1319 |
|
|
1320 |
|
|
1321 |
|
|
1322 |
|
|
1323 |
|
@param |
1324 |
|
@return |
1325 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1326 |
1276
|
private String getLatex(final Element element) {... |
1327 |
1276
|
return getQedeqBo().getElement2Latex().getLatex(element); |
1328 |
|
} |
1329 |
|
|
1330 |
|
|
1331 |
|
|
1332 |
|
|
1333 |
|
|
1334 |
|
|
1335 |
|
@param |
1336 |
|
|
1337 |
|
|
1338 |
|
@param |
1339 |
|
@return |
1340 |
|
|
|
|
| 89.6% |
Uncovered Elements: 5 (48) |
Complexity: 16 |
Complexity Density: 0.67 |
|
1341 |
3556
|
private String getLatexListEntry(final String method, final LatexList list) {... |
1342 |
3556
|
if (list == null) { |
1343 |
744
|
return ""; |
1344 |
|
} |
1345 |
2812
|
if (method.length() > 0) { |
1346 |
2812
|
subContext = method; |
1347 |
|
} |
1348 |
2812
|
try { |
1349 |
4024
|
for (int i = 0; language != null && i < list.size(); i++) { |
1350 |
3812
|
if (language.equals(list.get(i).getLanguage())) { |
1351 |
2600
|
if (method.length() > 0) { |
1352 |
2600
|
subContext = method + ".get(" + i + ")"; |
1353 |
|
} |
1354 |
2600
|
return getLatex(list.get(i)); |
1355 |
|
} |
1356 |
|
} |
1357 |
|
|
1358 |
212
|
final String def = getQedeqBo().getOriginalLanguage(); |
1359 |
232
|
for (int i = 0; i < list.size(); i++) { |
1360 |
212
|
if (EqualsUtility.equals(def, list.get(i).getLanguage())) { |
1361 |
192
|
if (method.length() > 0) { |
1362 |
192
|
subContext = method + ".get(" + i + ")"; |
1363 |
|
} |
1364 |
192
|
return "MISSING! OTHER: " + getLatex(list.get(i)); |
1365 |
|
} |
1366 |
|
} |
1367 |
|
|
1368 |
22
|
for (int i = 0; i < list.size(); i++) { |
1369 |
20
|
if (method.length() > 0) { |
1370 |
20
|
subContext = method + ".get(" + i + ")"; |
1371 |
|
} |
1372 |
20
|
if (null != list.get(i) && null != list.get(i).getLatex() |
1373 |
|
&& list.get(i).getLatex().trim().length() > 0) { |
1374 |
18
|
return "MISSING! OTHER: " + getLatex(list.get(i)); |
1375 |
|
} |
1376 |
|
} |
1377 |
2
|
return "MISSING!"; |
1378 |
|
} finally { |
1379 |
2812
|
if (method.length() > 0) { |
1380 |
2812
|
subContext = ""; |
1381 |
|
} |
1382 |
|
} |
1383 |
|
} |
1384 |
|
|
1385 |
|
|
1386 |
|
|
1387 |
|
|
1388 |
|
|
1389 |
|
@param |
1390 |
|
@return |
1391 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (7) |
Complexity: 3 |
Complexity Density: 0.6 |
|
1392 |
2810
|
private String getLatex(final Latex latex) {... |
1393 |
2810
|
if (latex == null || latex.getLatex() == null) { |
1394 |
6
|
return ""; |
1395 |
|
} |
1396 |
2804
|
StringBuffer result = new StringBuffer(latex.getLatex()); |
1397 |
|
|
1398 |
|
|
1399 |
|
|
1400 |
2804
|
transformQref(result); |
1401 |
|
|
1402 |
2804
|
return deleteLineLeadingWhitespace(result.toString()); |
1403 |
|
} |
1404 |
|
|
1405 |
|
|
1406 |
|
|
1407 |
|
|
1408 |
|
|
1409 |
|
|
1410 |
|
|
1411 |
|
@param |
1412 |
|
|
|
|
| 84.1% |
Uncovered Elements: 7 (44) |
Complexity: 7 |
Complexity Density: 0.22 |
|
1413 |
2804
|
private void transformQref(final StringBuffer result) {... |
1414 |
2804
|
final String method = "transformQref(StringBuffer)"; |
1415 |
2804
|
final StringBuffer buffer = new StringBuffer(result.toString()); |
1416 |
2804
|
final TextInput input = new TextInput(buffer); |
1417 |
2804
|
int last = 0; |
1418 |
2804
|
try { |
1419 |
2804
|
result.setLength(0); |
1420 |
3273
|
while (input.forward("\\qref{")) { |
1421 |
469
|
final SourcePosition startPosition = input.getSourcePosition(); |
1422 |
469
|
final int start = input.getPosition(); |
1423 |
469
|
if (!input.forward("}")) { |
1424 |
0
|
addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE, |
1425 |
|
LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition, |
1426 |
|
input.getSourcePosition()); |
1427 |
0
|
continue; |
1428 |
|
} |
1429 |
469
|
String ref = input.getSubstring(start + "\\qref{".length(), input.getPosition()).trim(); |
1430 |
469
|
input.read(); |
1431 |
469
|
Trace.param(CLASS, this, method, "1 ref", ref); |
1432 |
469
|
if (ref.length() == 0) { |
1433 |
1
|
addWarning(LatexErrorCodes.QREF_EMPTY_CODE, LatexErrorCodes.QREF_EMPTY_TEXT, |
1434 |
|
startPosition, input.getSourcePosition()); |
1435 |
1
|
continue; |
1436 |
|
} |
1437 |
468
|
if (ref.length() > 1024) { |
1438 |
0
|
addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE, |
1439 |
|
LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition, |
1440 |
|
input.getSourcePosition()); |
1441 |
0
|
continue; |
1442 |
|
} |
1443 |
468
|
if (ref.indexOf("{") >= 0) { |
1444 |
1
|
addWarning(LatexErrorCodes.QREF_END_NOT_FOUND_CODE, |
1445 |
|
LatexErrorCodes.QREF_END_NOT_FOUND_TEXT, startPosition, |
1446 |
|
input.getSourcePosition()); |
1447 |
1
|
continue; |
1448 |
|
} |
1449 |
467
|
final int end = input.getPosition(); |
1450 |
467
|
final SourcePosition endPosition = input.getSourcePosition(); |
1451 |
467
|
result.append(buffer.substring(last, start)); |
1452 |
467
|
result.append(getReference(ref, startPosition, endPosition)); |
1453 |
467
|
last = end; |
1454 |
|
} |
1455 |
|
} finally { |
1456 |
2804
|
IoUtility.close(input); |
1457 |
2804
|
if (last < buffer.length()) { |
1458 |
2804
|
result.append(buffer.substring(last)); |
1459 |
|
} |
1460 |
|
} |
1461 |
|
} |
1462 |
|
|
|
|
| 80.5% |
Uncovered Elements: 8 (41) |
Complexity: 16 |
Complexity Density: 1.07 |
|
1463 |
3005
|
private String getReference(final String reference, final SourcePosition start, final SourcePosition end) {... |
1464 |
3005
|
final String method = "getReference(String, String)"; |
1465 |
3005
|
Trace.param(CLASS, this, method, "2 reference", reference); |
1466 |
|
|
1467 |
3005
|
final Reference ref = getReference(reference, getCurrentContext(start, end), true, false); |
1468 |
3005
|
if (ref.isNodeLocalReference() && ref.isSubReference()) { |
1469 |
0
|
return "\\hyperlink{" + ref.getNodeLabel() + "/" + ref.getSubLabel() + "}{" + "(" |
1470 |
|
+ ref.getSubLabel() + ")" + "}"; |
1471 |
|
} |
1472 |
|
|
1473 |
3005
|
if (ref.isNodeLocalReference() && ref.isProofLineReference()) { |
1474 |
2052
|
return "\\hyperlink{" + ref.getNodeLabel() + "!" + ref.getProofLineLabel() + "}{" + "(" |
1475 |
|
+ ref.getProofLineLabel() + ")" + "}"; |
1476 |
|
} |
1477 |
|
|
1478 |
953
|
if (!ref.isExternal()) { |
1479 |
804
|
return "\\hyperlink{" + ref.getNodeLabel() |
1480 |
804
|
+ (ref.isSubReference() ? "/" + ref.getSubLabel() : "") |
1481 |
804
|
+ (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "") |
1482 |
|
+ "}{" |
1483 |
|
+ getNodeDisplay(ref.getNodeLabel(), ref.getNode()) |
1484 |
804
|
+ (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "") |
1485 |
804
|
+ (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "") |
1486 |
|
+ "}"; |
1487 |
|
} |
1488 |
|
|
1489 |
|
|
1490 |
149
|
if (ref.isExternalModuleReference()) { |
1491 |
8
|
return "\\url{" + getPdfLink(ref.getExternalQedeq()) + "}~\\cite{" |
1492 |
|
+ ref.getExternalQedeqLabel() + "}"; |
1493 |
|
|
1494 |
|
} |
1495 |
|
|
1496 |
141
|
String external = getPdfLink(ref.getExternalQedeq()); |
1497 |
141
|
if (external.startsWith("file://")) { |
1498 |
1
|
external = "file:" + external.substring("file://".length()); |
1499 |
|
} |
1500 |
141
|
return "\\hyperref{" + external + "}{}{" |
1501 |
|
+ ref.getNodeLabel() |
1502 |
141
|
+ (ref.isSubReference() ? "/" + ref.getSubLabel() : "") |
1503 |
141
|
+ (ref.isProofLineReference() ? "!" + ref.getProofLineLabel() : "") |
1504 |
|
+ "}{" + getNodeDisplay(ref.getNodeLabel(), ref.getNode()) |
1505 |
141
|
+ (ref.isSubReference() ? " (" + ref.getSubLabel() + ")" : "") |
1506 |
141
|
+ (ref.isProofLineReference() ? " (" + ref.getProofLineLabel() + ")" : "") |
1507 |
|
+ "}~\\cite{" + ref.getExternalQedeqLabel() + "}"; |
1508 |
|
} |
1509 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1510 |
945
|
private String getNodeDisplay(final String label, final KernelNodeBo kNode) {... |
1511 |
945
|
return StringUtility.replace(getNodeDisplay(label, kNode, language), " ", "~"); |
1512 |
|
} |
1513 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1514 |
2226
|
private String getRuleReference(final String ruleName) {... |
1515 |
2226
|
return getRuleReference(ruleName, ruleName); |
1516 |
|
} |
1517 |
|
|
|
|
| 64.7% |
Uncovered Elements: 12 (34) |
Complexity: 8 |
Complexity Density: 0.36 |
|
1518 |
2258
|
private String getRuleReference(final String ruleName, final String caption) {... |
1519 |
2258
|
final String method = "getRuleReference(String, String)"; |
1520 |
2258
|
Trace.param(CLASS, this, method, "ruleName", ruleName); |
1521 |
2258
|
RuleKey key = getLocalRuleKey(ruleName); |
1522 |
2258
|
if (key == null && getQedeqBo().getExistenceChecker() != null) { |
1523 |
0
|
key = getQedeqBo().getExistenceChecker().getParentRuleKey(ruleName); |
1524 |
|
} |
1525 |
2258
|
if (key == null) { |
1526 |
0
|
key = getQedeqBo().getLabels().getRuleKey(ruleName); |
1527 |
|
} |
1528 |
2258
|
KernelQedeqBo qedeq = getQedeqBo(); |
1529 |
2258
|
if (getQedeqBo().getExistenceChecker() != null) { |
1530 |
2258
|
qedeq = getQedeqBo().getExistenceChecker().getQedeq(key); |
1531 |
|
} |
1532 |
2258
|
String localRef = getQedeqBo().getLabels().getRuleLabel(key); |
1533 |
2258
|
final String refRuleName = qedeq.getLabels().getRule(key).getName(); |
1534 |
2258
|
if (!ruleName.equals(refRuleName)) { |
1535 |
1256
|
localRef += "!" + ruleName; |
1536 |
|
} |
1537 |
2258
|
qedeq.getLabels().getRule(key).getName(); |
1538 |
2258
|
boolean local = getQedeqBo().equals(qedeq); |
1539 |
2258
|
if (local) { |
1540 |
2258
|
return "\\hyperlink{" + localRef + "}{" + caption + "}"; |
1541 |
|
} |
1542 |
0
|
String external = getPdfLink(qedeq); |
1543 |
0
|
if (external.startsWith("file://")) { |
1544 |
0
|
external = "file:" + external.substring("file://".length()); |
1545 |
|
} |
1546 |
0
|
return "\\hyperref{" + external + "}{}{" + caption + "}{" |
1547 |
|
+ localRef + "}"; |
1548 |
|
} |
1549 |
|
|
1550 |
|
|
1551 |
|
|
1552 |
|
|
1553 |
|
@param |
1554 |
|
|
1555 |
|
@param |
1556 |
|
|
1557 |
|
@return |
1558 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
1559 |
3007
|
public ModuleContext getCurrentContext(final SourcePosition startDelta,... |
1560 |
|
final SourcePosition endDelta) { |
1561 |
3007
|
if (subContext.length() == 0) { |
1562 |
2538
|
return super.getCurrentContext(); |
1563 |
|
} |
1564 |
469
|
final ModuleContext c = new ModuleContext(super.getCurrentContext().getModuleLocation(), |
1565 |
|
super.getCurrentContext().getLocationWithinModule() + "." + subContext, |
1566 |
|
startDelta, endDelta); |
1567 |
469
|
return c; |
1568 |
|
} |
1569 |
|
|
1570 |
|
|
1571 |
|
|
1572 |
|
|
1573 |
|
|
1574 |
|
|
1575 |
|
|
1576 |
|
|
1577 |
|
|
1578 |
|
|
1579 |
|
@param |
1580 |
|
@param |
1581 |
|
@param |
1582 |
|
|
1583 |
|
@param |
1584 |
|
|
1585 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0.5 |
|
1586 |
2
|
private void addWarning(final int code, final String msg, final SourcePosition startDelta,... |
1587 |
|
final SourcePosition endDelta) { |
1588 |
2
|
Trace.param(CLASS, this, "addWarning", "msg", msg); |
1589 |
2
|
addWarning(new LatexContentException(code, msg, getCurrentContext(startDelta, endDelta))); |
1590 |
|
} |
1591 |
|
|
1592 |
|
|
1593 |
|
|
1594 |
|
|
1595 |
|
|
1596 |
|
@param |
1597 |
|
@return |
1598 |
|
|
|
|
| 64.3% |
Uncovered Elements: 5 (14) |
Complexity: 4 |
Complexity Density: 0.5 |
|
1599 |
189
|
private String getPdfLink(final KernelQedeqBo prop) {... |
1600 |
189
|
if (prop == null) { |
1601 |
4
|
return ""; |
1602 |
|
} |
1603 |
185
|
final String url = prop.getUrl(); |
1604 |
185
|
final int dot = url.lastIndexOf("."); |
1605 |
185
|
if (prop.isSupportedLanguage(language)) { |
1606 |
185
|
return url.substring(0, dot) + "_" + language + ".pdf"; |
1607 |
|
} |
1608 |
0
|
final String a = prop.getOriginalLanguage(); |
1609 |
0
|
return url.substring(0, dot) + (a.length() > 0 ? "_" + a : "") + ".pdf"; |
1610 |
|
} |
1611 |
|
|
1612 |
|
|
1613 |
|
|
1614 |
|
|
1615 |
|
|
1616 |
|
@param |
1617 |
|
@return |
1618 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (15) |
Complexity: 1 |
Complexity Density: 0.07 |
|
1619 |
48
|
private String getLatex(final String text) {... |
1620 |
48
|
final StringBuffer buffer = new StringBuffer(text); |
1621 |
48
|
StringUtility.replace(buffer, "\\", "\\textbackslash"); |
1622 |
48
|
StringUtility.replace(buffer, "$", "\\$"); |
1623 |
48
|
StringUtility.replace(buffer, "&", "\\&"); |
1624 |
48
|
StringUtility.replace(buffer, "%", "\\%"); |
1625 |
48
|
StringUtility.replace(buffer, "#", "\\#"); |
1626 |
48
|
StringUtility.replace(buffer, "_", "\\_"); |
1627 |
48
|
StringUtility.replace(buffer, "{", "\\{"); |
1628 |
48
|
StringUtility.replace(buffer, "}", "\\}"); |
1629 |
48
|
StringUtility.replace(buffer, "~", "\\textasciitilde"); |
1630 |
48
|
StringUtility.replace(buffer, "^", "\\textasciicircum"); |
1631 |
48
|
StringUtility.replace(buffer, "<", "\\textless"); |
1632 |
48
|
StringUtility.replace(buffer, ">", "\\textgreater"); |
1633 |
48
|
StringUtility.deleteLineLeadingWhitespace(buffer); |
1634 |
48
|
return buffer.toString().trim(); |
1635 |
|
} |
1636 |
|
|
1637 |
|
|
1638 |
|
|
1639 |
|
|
1640 |
|
@param |
1641 |
|
@return |
1642 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0.33 |
|
1643 |
2804
|
private String deleteLineLeadingWhitespace(final String text) {... |
1644 |
2804
|
final StringBuffer buffer = new StringBuffer(text); |
1645 |
2804
|
StringUtility.deleteLineLeadingWhitespace(buffer); |
1646 |
2804
|
return buffer.toString().trim(); |
1647 |
|
} |
1648 |
|
|
1649 |
|
|
1650 |
|
|
1651 |
|
|
1652 |
|
|
1653 |
|
@param |
1654 |
|
@return |
1655 |
|
|
|
|
| 84.6% |
Uncovered Elements: 2 (13) |
Complexity: 2 |
Complexity Density: 0.18 |
|
1656 |
533220
|
private String escapeUmlauts(final String nearlyLatex) {... |
1657 |
533220
|
if (nearlyLatex == null) { |
1658 |
0
|
return ""; |
1659 |
|
} |
1660 |
533220
|
final StringBuffer buffer = new StringBuffer(nearlyLatex); |
1661 |
|
|
1662 |
|
|
1663 |
|
|
1664 |
|
|
1665 |
|
|
1666 |
|
|
1667 |
533220
|
StringUtility.replace(buffer, "\u00fc", "{\\\"u}"); |
1668 |
533220
|
StringUtility.replace(buffer, "\u00f6", "{\\\"o}"); |
1669 |
533220
|
StringUtility.replace(buffer, "\u00e4", "{\\\"a}"); |
1670 |
533220
|
StringUtility.replace(buffer, "\u00dc", "{\\\"U}"); |
1671 |
533220
|
StringUtility.replace(buffer, "\u00d6", "{\\\"O}"); |
1672 |
533220
|
StringUtility.replace(buffer, "\u00c4", "{\\\"A}"); |
1673 |
533220
|
StringUtility.replace(buffer, "\u00df", "{\\ss}"); |
1674 |
533220
|
return buffer.toString(); |
1675 |
|
} |
1676 |
|
|
1677 |
|
} |