1 | /* This file is part of the project "Hilbert II" - http://www.qedeq.org |
2 | * |
3 | * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>. |
4 | * |
5 | * "Hilbert II" is free software; you can redistribute |
6 | * it and/or modify it under the terms of the GNU General Public |
7 | * License as published by the Free Software Foundation; either |
8 | * version 2 of the License, or (at your option) any later version. |
9 | * |
10 | * This program is distributed in the hope that it will be useful, |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
13 | * GNU General Public License for more details. |
14 | */ |
15 | |
16 | package org.qedeq.kernel.xml.dao; |
17 | |
18 | import java.io.IOException; |
19 | |
20 | import org.qedeq.base.io.TextOutput; |
21 | import org.qedeq.base.utility.StringUtility; |
22 | import org.qedeq.kernel.bo.KernelContext; |
23 | import org.qedeq.kernel.bo.module.InternalServiceJob; |
24 | import org.qedeq.kernel.bo.module.KernelQedeqBo; |
25 | import org.qedeq.kernel.bo.service.basis.ControlVisitor; |
26 | import org.qedeq.kernel.se.base.list.ElementList; |
27 | import org.qedeq.kernel.se.base.module.Add; |
28 | import org.qedeq.kernel.se.base.module.Author; |
29 | import org.qedeq.kernel.se.base.module.AuthorList; |
30 | import org.qedeq.kernel.se.base.module.Axiom; |
31 | import org.qedeq.kernel.se.base.module.ChangedRule; |
32 | import org.qedeq.kernel.se.base.module.Chapter; |
33 | import org.qedeq.kernel.se.base.module.Conclusion; |
34 | import org.qedeq.kernel.se.base.module.ConditionalProof; |
35 | import org.qedeq.kernel.se.base.module.Existential; |
36 | import org.qedeq.kernel.se.base.module.FormalProof; |
37 | import org.qedeq.kernel.se.base.module.FormalProofLine; |
38 | import org.qedeq.kernel.se.base.module.FormalProofLineList; |
39 | import org.qedeq.kernel.se.base.module.Formula; |
40 | import org.qedeq.kernel.se.base.module.FunctionDefinition; |
41 | import org.qedeq.kernel.se.base.module.Header; |
42 | import org.qedeq.kernel.se.base.module.Hypothesis; |
43 | import org.qedeq.kernel.se.base.module.Import; |
44 | import org.qedeq.kernel.se.base.module.ImportList; |
45 | import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
46 | import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
47 | import org.qedeq.kernel.se.base.module.Latex; |
48 | import org.qedeq.kernel.se.base.module.LatexList; |
49 | import org.qedeq.kernel.se.base.module.LinkList; |
50 | import org.qedeq.kernel.se.base.module.LiteratureItem; |
51 | import org.qedeq.kernel.se.base.module.LiteratureItemList; |
52 | import org.qedeq.kernel.se.base.module.Location; |
53 | import org.qedeq.kernel.se.base.module.LocationList; |
54 | import org.qedeq.kernel.se.base.module.ModusPonens; |
55 | import org.qedeq.kernel.se.base.module.Node; |
56 | import org.qedeq.kernel.se.base.module.PredicateDefinition; |
57 | import org.qedeq.kernel.se.base.module.Proof; |
58 | import org.qedeq.kernel.se.base.module.Proposition; |
59 | import org.qedeq.kernel.se.base.module.Qedeq; |
60 | import org.qedeq.kernel.se.base.module.Rename; |
61 | import org.qedeq.kernel.se.base.module.Rule; |
62 | import org.qedeq.kernel.se.base.module.Section; |
63 | import org.qedeq.kernel.se.base.module.Specification; |
64 | import org.qedeq.kernel.se.base.module.Subsection; |
65 | import org.qedeq.kernel.se.base.module.SubsectionList; |
66 | import org.qedeq.kernel.se.base.module.SubstFree; |
67 | import org.qedeq.kernel.se.base.module.SubstFunc; |
68 | import org.qedeq.kernel.se.base.module.SubstPred; |
69 | import org.qedeq.kernel.se.base.module.Term; |
70 | import org.qedeq.kernel.se.base.module.Universal; |
71 | import org.qedeq.kernel.se.base.module.UsedByList; |
72 | import org.qedeq.kernel.se.common.ModuleService; |
73 | import org.qedeq.kernel.se.common.SourceFileExceptionList; |
74 | |
75 | |
76 | /** |
77 | * This class prints a QEDEQ module in XML format in an output stream. |
78 | * |
79 | * @author Michael Meyling |
80 | */ |
81 | public final class Qedeq2Xml extends ControlVisitor implements ModuleService { |
82 | |
83 | /** Output goes here. */ |
84 | private TextOutput printer; |
85 | |
86 | /** |
87 | * Constructor. |
88 | * |
89 | * @param plugin This plugin we work for. |
90 | * @param bo QEDEQ BO. |
91 | * @param printer Print herein. |
92 | */ |
93 | public Qedeq2Xml(final ModuleService plugin, final KernelQedeqBo bo, final TextOutput printer) { |
94 | super(plugin, bo); |
95 | this.printer = printer; |
96 | } |
97 | |
98 | /** |
99 | * Prints a XML representation of given QEDEQ module into a given output stream. |
100 | * |
101 | * @param process Service process we work for. |
102 | * @param plugin Plugin we work for. |
103 | * @param bo BO QEDEQ module object. |
104 | * @param printer Print herein. |
105 | * @throws SourceFileExceptionList Major problem occurred. |
106 | * @throws IOException Writing failed. |
107 | */ |
108 | public static void print(final InternalServiceJob process, |
109 | final ModuleService plugin, final KernelQedeqBo bo, final TextOutput printer) throws |
110 | SourceFileExceptionList, IOException { |
111 | final Qedeq2Xml converter = new Qedeq2Xml(plugin, bo, printer); |
112 | try { |
113 | converter.traverse(process); |
114 | } finally { |
115 | printer.flush(); |
116 | } |
117 | if (printer.checkError()) { |
118 | throw printer.getError(); |
119 | } |
120 | } |
121 | |
122 | public final void visitEnter(final Qedeq qedeq) { |
123 | printer.println("<?xml version=\"1.0\" encoding=\"UTF-8\"?>"); |
124 | printer.println("<QEDEQ"); |
125 | printer.println(" xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\""); |
126 | printer.println(" xsi:noNamespaceSchemaLocation=\"http://www.qedeq.org/" |
127 | + KernelContext.getInstance().getKernelVersionDirectory() + "/xml/qedeq.xsd\">"); |
128 | printer.pushLevel(); |
129 | } |
130 | |
131 | public final void visitLeave(final Qedeq qedeq) { |
132 | printer.popLevel(); |
133 | printer.println("</QEDEQ>"); |
134 | } |
135 | |
136 | public void visitEnter(final Header header) { |
137 | printer.print("<HEADER"); |
138 | if (header.getEmail() != null) { |
139 | printer.print(" email=\"" + StringUtility.escapeXml(header.getEmail()) + "\""); |
140 | } |
141 | printer.println(">"); |
142 | printer.pushLevel(); |
143 | } |
144 | |
145 | public void visitLeave(final Header header) { |
146 | printer.popLevel(); |
147 | printer.println("</HEADER>"); |
148 | } |
149 | |
150 | public void visitEnter(final Specification specification) { |
151 | printer.print("<SPECIFICATION"); |
152 | if (specification.getName() != null) { |
153 | printer.print(" name=\"" + StringUtility.escapeXml(specification.getName()) + "\""); |
154 | } |
155 | if (specification.getName() != null) { |
156 | printer.print(" ruleVersion=\"" + StringUtility.escapeXml(specification.getRuleVersion()) + "\""); |
157 | } |
158 | printer.println(">"); |
159 | printer.pushLevel(); |
160 | } |
161 | |
162 | public void visitLeave(final Specification specification) { |
163 | printer.popLevel(); |
164 | printer.println("</SPECIFICATION>"); |
165 | } |
166 | |
167 | public void visitEnter(final LatexList latexList) { |
168 | final String last = getCurrentContext().getLocationWithinModule(); |
169 | if (last.endsWith(".getTitle()")) { |
170 | printer.println("<TITLE>"); |
171 | } else if (last.endsWith(".getSummary()")) { |
172 | printer.println("<ABSTRACT>"); |
173 | } else if (last.endsWith(".getIntroduction()")) { |
174 | printer.println("<INTRODUCTION>"); |
175 | } else if (last.endsWith(".getName()")) { |
176 | printer.println("<NAME>"); |
177 | } else if (last.endsWith(".getPrecedingText()")) { |
178 | printer.println("<PRECEDING>"); |
179 | } else if (last.endsWith(".getSucceedingText()")) { |
180 | printer.println("<SUCCEEDING>"); |
181 | } else if (last.endsWith(".getLatex()")) { |
182 | printer.println("<TEXT>"); |
183 | } else if (last.endsWith(".getDescription()")) { |
184 | if (last.indexOf(".getChangedRuleList().get(") < 0) { |
185 | printer.println("<DESCRIPTION>"); |
186 | } |
187 | } |
188 | printer.pushLevel(); |
189 | } |
190 | |
191 | public void visitLeave(final LatexList latexList) { |
192 | printer.popLevel(); |
193 | final String last = getCurrentContext().getLocationWithinModule(); |
194 | if (last.endsWith(".getTitle()")) { |
195 | printer.println("</TITLE>"); |
196 | } else if (last.endsWith(".getSummary()")) { |
197 | printer.println("</ABSTRACT>"); |
198 | } else if (last.endsWith(".getIntroduction()")) { |
199 | printer.println("</INTRODUCTION>"); |
200 | } else if (last.endsWith(".getName()")) { |
201 | printer.println("</NAME>"); |
202 | } else if (last.endsWith(".getPrecedingText()")) { |
203 | printer.println("</PRECEDING>"); |
204 | } else if (last.endsWith(".getSucceedingText()")) { |
205 | printer.println("</SUCCEEDING>"); |
206 | } else if (last.endsWith(".getLatex()")) { |
207 | printer.println("</TEXT>"); |
208 | } else if (last.endsWith(".getDescription()")) { |
209 | if (last.indexOf(".getChangedRuleList().get(") < 0) { |
210 | printer.println("</DESCRIPTION>"); |
211 | } |
212 | } |
213 | } |
214 | |
215 | public void visitEnter(final Latex latex) { |
216 | printer.print("<LATEX"); |
217 | if (latex.getLanguage() != null) { |
218 | printer.print(" language=\"" + latex.getLanguage() + "\""); |
219 | } |
220 | printer.println(">"); |
221 | if (latex.getLatex() != null) { |
222 | printer.pushLevel(); |
223 | printer.println("<![CDATA["); |
224 | printer.addToken(" "); // we must fool the printer, this is token not whitespace! |
225 | final String tabs = printer.getLevel(); |
226 | printer.clearLevel(); |
227 | // escape ]]> |
228 | final String data = StringUtility.replace(latex.getLatex(), |
229 | "]]>", "]]]]><![CDATA[>"); |
230 | printer.println(StringUtility.useSystemLineSeparator(data).trim()); |
231 | printer.pushLevel(tabs); |
232 | } |
233 | } |
234 | |
235 | public void visitLeave(final Latex latex) { |
236 | if (latex.getLatex() != null) { |
237 | printer.println("]]>"); |
238 | printer.popLevel(); |
239 | } |
240 | printer.println("</LATEX>"); |
241 | } |
242 | |
243 | public void visitEnter(final LocationList locationList) { |
244 | printer.println("<LOCATIONS>"); |
245 | printer.pushLevel(); |
246 | } |
247 | |
248 | public void visitLeave(final LocationList locationList) { |
249 | printer.popLevel(); |
250 | printer.println("</LOCATIONS>"); |
251 | } |
252 | |
253 | public void visitEnter(final Location location) { |
254 | printer.print("<LOCATION"); |
255 | if (location.getLocation() != null) { |
256 | printer.print(" value=\"" + location.getLocation() + "\""); |
257 | } |
258 | printer.println(" />"); |
259 | } |
260 | |
261 | public void visitEnter(final AuthorList authorList) { |
262 | printer.println("<AUTHORS>"); |
263 | printer.pushLevel(); |
264 | } |
265 | |
266 | public void visitLeave(final AuthorList authorList) { |
267 | printer.popLevel(); |
268 | printer.println("</AUTHORS>"); |
269 | } |
270 | |
271 | public void visitEnter(final Author author) { |
272 | printer.print("<AUTHOR"); |
273 | if (author.getEmail() != null) { |
274 | printer.print(" email=\"" + StringUtility.escapeXml(author.getEmail()) + "\""); |
275 | } |
276 | printer.println(">"); |
277 | printer.pushLevel(); |
278 | if (author.getName() != null) { |
279 | printer.println("<NAME>"); |
280 | } |
281 | printer.pushLevel(); |
282 | } |
283 | |
284 | public void visitLeave(final Author author) { |
285 | printer.popLevel(); |
286 | if (author.getName() != null) { |
287 | printer.println("</NAME>"); |
288 | } |
289 | printer.popLevel(); |
290 | printer.println("</AUTHOR>"); |
291 | } |
292 | |
293 | public void visitEnter(final ImportList importList) { |
294 | printer.println("<IMPORTS>"); |
295 | printer.pushLevel(); |
296 | } |
297 | |
298 | public void visitLeave(final ImportList importList) { |
299 | printer.popLevel(); |
300 | printer.println("</IMPORTS>"); |
301 | } |
302 | |
303 | public void visitEnter(final Import imp) { |
304 | printer.print("<IMPORT"); |
305 | if (imp.getLabel() != null) { |
306 | printer.print(" label=\"" + StringUtility.escapeXml(imp.getLabel()) + "\""); |
307 | } |
308 | printer.println(">"); |
309 | printer.pushLevel(); |
310 | } |
311 | |
312 | public void visitLeave(final Import imp) { |
313 | printer.popLevel(); |
314 | printer.println("</IMPORT>"); |
315 | } |
316 | |
317 | public void visitEnter(final UsedByList usedByList) { |
318 | printer.println("<USEDBY>"); |
319 | printer.pushLevel(); |
320 | } |
321 | |
322 | public void visitLeave(final UsedByList usedByList) { |
323 | printer.popLevel(); |
324 | printer.println("</USEDBY>"); |
325 | } |
326 | |
327 | public void visitEnter(final Chapter chapter) { |
328 | printer.print("<CHAPTER"); |
329 | if (chapter.getNoNumber() != null) { |
330 | printer.print(" noNumber=\"" + chapter.getNoNumber().booleanValue() + "\""); |
331 | } |
332 | printer.println(">"); |
333 | printer.pushLevel(); |
334 | } |
335 | |
336 | public void visitLeave(final Chapter chapter) { |
337 | printer.popLevel(); |
338 | printer.println("</CHAPTER>"); |
339 | } |
340 | |
341 | public void visitEnter(final Section section) { |
342 | printer.print("<SECTION"); |
343 | if (section.getNoNumber() != null) { |
344 | printer.print(" noNumber=\"" + section.getNoNumber().booleanValue() + "\""); |
345 | } |
346 | printer.println(">"); |
347 | printer.pushLevel(); |
348 | } |
349 | |
350 | public void visitLeave(final Section section) { |
351 | printer.popLevel(); |
352 | printer.println("</SECTION>"); |
353 | } |
354 | |
355 | public void visitEnter(final SubsectionList subsectionList) { |
356 | printer.println("<SUBSECTIONS>"); |
357 | printer.pushLevel(); |
358 | } |
359 | |
360 | public void visitLeave(final SubsectionList subsectionList) { |
361 | printer.popLevel(); |
362 | printer.println("</SUBSECTIONS>"); |
363 | } |
364 | |
365 | public void visitEnter(final Subsection subsection) { |
366 | printer.print("<SUBSECTION"); |
367 | if (subsection.getId() != null) { |
368 | printer.print(" id=\"" + StringUtility.escapeXml(subsection.getId()) + "\""); |
369 | } |
370 | if (subsection.getLevel() != null) { |
371 | printer.print(" level=\"" + StringUtility.escapeXml(subsection.getLevel()) + "\""); |
372 | } |
373 | printer.println(">"); |
374 | printer.pushLevel(); |
375 | } |
376 | |
377 | public void visitLeave(final Subsection subsection) { |
378 | printer.popLevel(); |
379 | printer.println("</SUBSECTION>"); |
380 | } |
381 | |
382 | public void visitEnter(final Node node) { |
383 | printer.print("<NODE"); |
384 | if (node.getId() != null) { |
385 | printer.print(" id=\"" + StringUtility.escapeXml(node.getId()) + "\""); |
386 | } |
387 | if (node.getLevel() != null) { |
388 | printer.print(" level=\"" + StringUtility.escapeXml(node.getLevel()) + "\""); |
389 | } |
390 | printer.println(">"); |
391 | printer.pushLevel(); |
392 | } |
393 | |
394 | public void visitLeave(final Node node) { |
395 | printer.popLevel(); |
396 | printer.println("</NODE>"); |
397 | } |
398 | |
399 | public void visitEnter(final Axiom axiom) { |
400 | printer.print("<AXIOM"); |
401 | if (axiom.getDefinedOperator() != null) { |
402 | printer.print(" definedOperator=\"" + StringUtility.escapeXml(axiom.getDefinedOperator()) + "\""); |
403 | } |
404 | printer.println(">"); |
405 | printer.pushLevel(); |
406 | } |
407 | |
408 | public void visitLeave(final Axiom axiom) { |
409 | printer.popLevel(); |
410 | printer.println("</AXIOM>"); |
411 | } |
412 | |
413 | public void visitEnter(final Proposition proposition) { |
414 | printer.println("<THEOREM>"); |
415 | printer.pushLevel(); |
416 | } |
417 | |
418 | public void visitLeave(final Proposition proposition) { |
419 | printer.popLevel(); |
420 | printer.println("</THEOREM>"); |
421 | } |
422 | |
423 | public void visitEnter(final Proof proof) { |
424 | printer.print("<PROOF"); |
425 | if (proof.getKind() != null) { |
426 | printer.print(" kind=\"" + StringUtility.escapeXml(proof.getKind()) + "\""); |
427 | } |
428 | if (proof.getLevel() != null) { |
429 | printer.print(" level=\"" + StringUtility.escapeXml(proof.getLevel()) + "\""); |
430 | } |
431 | printer.println(">"); |
432 | } |
433 | |
434 | public void visitLeave(final Proof proof) { |
435 | printer.println("</PROOF>"); |
436 | } |
437 | |
438 | public void visitEnter(final FormalProof proof) { |
439 | printer.println("<FORMAL_PROOF>"); |
440 | printer.pushLevel(); |
441 | } |
442 | |
443 | public void visitLeave(final FormalProof proof) { |
444 | printer.popLevel(); |
445 | printer.println("</FORMAL_PROOF>"); |
446 | } |
447 | |
448 | public void visitEnter(final FormalProofLineList proof) { |
449 | printer.println("<LINES>"); |
450 | printer.pushLevel(); |
451 | } |
452 | |
453 | public void visitLeave(final FormalProofLineList proof) { |
454 | printer.popLevel(); |
455 | printer.println("</LINES>"); |
456 | } |
457 | |
458 | public void visitEnter(final FormalProofLine line) { |
459 | printer.print("<L"); |
460 | if (line.getLabel() != null) { |
461 | printer.print(" label=\"" + StringUtility.escapeXml(line.getLabel()) + "\""); |
462 | } |
463 | printer.println(">"); |
464 | printer.pushLevel(); |
465 | } |
466 | |
467 | public void visitLeave(final FormalProofLine line) { |
468 | printer.popLevel(); |
469 | printer.println("</L>"); |
470 | } |
471 | |
472 | public void visitEnter(final ModusPonens reason) { |
473 | printer.print("<MP"); |
474 | if (reason.getReference1() != null) { |
475 | printer.print(" ref1=\"" + StringUtility.escapeXml(reason.getReference1()) + "\""); |
476 | } |
477 | if (reason.getReference2() != null) { |
478 | printer.print(" ref2=\"" + StringUtility.escapeXml(reason.getReference2()) + "\""); |
479 | } |
480 | } |
481 | |
482 | public void visitLeave(final ModusPonens reason) { |
483 | printer.println("/>"); |
484 | } |
485 | |
486 | public void visitEnter(final Add reason) { |
487 | printer.print("<ADD"); |
488 | if (reason.getReference() != null) { |
489 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
490 | } |
491 | } |
492 | |
493 | public void visitLeave(final Add reason) { |
494 | printer.println("/>"); |
495 | } |
496 | |
497 | public void visitEnter(final Rename reason) { |
498 | printer.print("<RENAME"); |
499 | if (reason.getReference() != null) { |
500 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
501 | } |
502 | if (reason.getOccurrence() != 0) { |
503 | printer.print(" occurrence=\"" + StringUtility.escapeXml("" + reason.getOccurrence()) + "\""); |
504 | } |
505 | printer.println(">"); |
506 | printer.pushLevel(); |
507 | } |
508 | |
509 | public void visitLeave(final Rename reason) { |
510 | printer.popLevel(); |
511 | printer.println("</RENAME>"); |
512 | } |
513 | |
514 | public void visitEnter(final SubstFree reason) { |
515 | printer.print("<SUBST_FREE"); |
516 | if (reason.getReference() != null) { |
517 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
518 | } |
519 | printer.println(">"); |
520 | printer.pushLevel(); |
521 | } |
522 | |
523 | public void visitLeave(final SubstFree reason) { |
524 | printer.popLevel(); |
525 | printer.println("</SUBST_FREE>"); |
526 | } |
527 | |
528 | public void visitEnter(final SubstFunc reason) { |
529 | printer.print("<SUBST_FUNVAR"); |
530 | if (reason.getReference() != null) { |
531 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
532 | } |
533 | printer.println(">"); |
534 | printer.pushLevel(); |
535 | } |
536 | |
537 | public void visitLeave(final SubstFunc reason) { |
538 | printer.popLevel(); |
539 | printer.println("</SUBST_FUNVAR>"); |
540 | } |
541 | |
542 | public void visitEnter(final SubstPred reason) { |
543 | printer.print("<SUBST_PREDVAR"); |
544 | if (reason.getReference() != null) { |
545 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
546 | } |
547 | printer.println(">"); |
548 | printer.pushLevel(); |
549 | } |
550 | |
551 | public void visitLeave(final SubstPred reason) { |
552 | printer.popLevel(); |
553 | printer.println("</SUBST_PREDVAR>"); |
554 | } |
555 | |
556 | public void visitEnter(final Existential reason) { |
557 | printer.print("<EXISTENTIAL"); |
558 | if (reason.getReference() != null) { |
559 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
560 | } |
561 | printer.println(">"); |
562 | printer.pushLevel(); |
563 | } |
564 | |
565 | public void visitLeave(final Existential reason) { |
566 | printer.popLevel(); |
567 | printer.println("</EXISTENTIAL>"); |
568 | } |
569 | |
570 | public void visitEnter(final Universal reason) { |
571 | printer.print("<UNIVERSAL"); |
572 | if (reason.getReference() != null) { |
573 | printer.print(" ref=\"" + StringUtility.escapeXml(reason.getReference()) + "\""); |
574 | } |
575 | printer.println(">"); |
576 | printer.pushLevel(); |
577 | } |
578 | |
579 | public void visitLeave(final Universal reason) { |
580 | printer.popLevel(); |
581 | printer.println("</UNIVERSAL>"); |
582 | } |
583 | |
584 | public void visitEnter(final ConditionalProof reason) { |
585 | printer.println("<CP>"); |
586 | printer.pushLevel(); |
587 | } |
588 | |
589 | public void visitLeave(final ConditionalProof reason) { |
590 | printer.popLevel(); |
591 | printer.println("</CP>"); |
592 | } |
593 | |
594 | public void visitEnter(final Hypothesis hypothesis) { |
595 | printer.print("<HYPOTHESIS"); |
596 | if (hypothesis.getLabel() != null) { |
597 | printer.print(" label=\"" + StringUtility.escapeXml(hypothesis.getLabel()) + "\""); |
598 | } |
599 | printer.println(">"); |
600 | printer.pushLevel(); |
601 | } |
602 | |
603 | public void visitLeave(final Hypothesis hypothesis) { |
604 | printer.popLevel(); |
605 | printer.println("</HYPOTHESIS>"); |
606 | } |
607 | |
608 | public void visitEnter(final Conclusion conclusion) { |
609 | printer.print("<CONCLUSION"); |
610 | if (conclusion.getLabel() != null) { |
611 | printer.print(" label=\"" + StringUtility.escapeXml(conclusion.getLabel()) + "\""); |
612 | } |
613 | printer.println(">"); |
614 | printer.pushLevel(); |
615 | } |
616 | |
617 | public void visitLeave(final Conclusion conclusion) { |
618 | printer.popLevel(); |
619 | printer.println("</CONCLUSION>"); |
620 | } |
621 | |
622 | public void visitEnter(final InitialPredicateDefinition definition) { |
623 | printer.print("<DEFINITION_PREDICATE_INITIAL"); |
624 | if (definition.getArgumentNumber() != null) { |
625 | printer.print(" arguments=\"" + StringUtility.escapeXml(definition.getArgumentNumber()) + "\""); |
626 | } |
627 | if (definition.getName() != null) { |
628 | printer.print(" name=\"" + StringUtility.escapeXml(definition.getName()) + "\""); |
629 | } |
630 | printer.println(">"); |
631 | printer.pushLevel(); |
632 | if (definition.getLatexPattern() != null) { |
633 | printer.println("<LATEXPATTERN>" + StringUtility.escapeXml(definition.getLatexPattern()) |
634 | + "</LATEXPATTERN>"); |
635 | } |
636 | } |
637 | |
638 | public void visitLeave(final InitialPredicateDefinition definition) { |
639 | printer.popLevel(); |
640 | printer.println("</DEFINITION_PREDICATE_INITIAL>"); |
641 | } |
642 | |
643 | public void visitEnter(final PredicateDefinition definition) { |
644 | printer.print("<DEFINITION_PREDICATE"); |
645 | if (definition.getArgumentNumber() != null) { |
646 | printer.print(" arguments=\"" + StringUtility.escapeXml(definition.getArgumentNumber()) + "\""); |
647 | } |
648 | if (definition.getName() != null) { |
649 | printer.print(" name=\"" + StringUtility.escapeXml(definition.getName()) + "\""); |
650 | } |
651 | printer.println(">"); |
652 | printer.pushLevel(); |
653 | if (definition.getLatexPattern() != null) { |
654 | printer.println("<LATEXPATTERN>" + StringUtility.escapeXml(definition.getLatexPattern()) |
655 | + "</LATEXPATTERN>"); |
656 | } |
657 | } |
658 | |
659 | public void visitLeave(final PredicateDefinition definition) { |
660 | printer.popLevel(); |
661 | printer.println("</DEFINITION_PREDICATE>"); |
662 | } |
663 | |
664 | public void visitEnter(final InitialFunctionDefinition definition) { |
665 | printer.print("<DEFINITION_FUNCTION_INITIAL"); |
666 | if (definition.getArgumentNumber() != null) { |
667 | printer.print(" arguments=\"" + StringUtility.escapeXml(definition.getArgumentNumber()) + "\""); |
668 | } |
669 | if (definition.getName() != null) { |
670 | printer.print(" name=\"" + StringUtility.escapeXml(definition.getName()) + "\""); |
671 | } |
672 | printer.println(">"); |
673 | printer.pushLevel(); |
674 | if (definition.getLatexPattern() != null) { |
675 | printer.println("<LATEXPATTERN>" + definition.getLatexPattern() |
676 | + "</LATEXPATTERN>"); |
677 | } |
678 | } |
679 | |
680 | public void visitLeave(final InitialFunctionDefinition definition) { |
681 | printer.popLevel(); |
682 | printer.println("</DEFINITION_FUNCTION_INITIAL>"); |
683 | } |
684 | |
685 | public void visitEnter(final FunctionDefinition definition) { |
686 | printer.print("<DEFINITION_FUNCTION"); |
687 | if (definition.getArgumentNumber() != null) { |
688 | printer.print(" arguments=\"" + StringUtility.escapeXml(definition.getArgumentNumber()) + "\""); |
689 | } |
690 | if (definition.getName() != null) { |
691 | printer.print(" name=\"" + StringUtility.escapeXml(definition.getName()) + "\""); |
692 | } |
693 | printer.println(">"); |
694 | printer.pushLevel(); |
695 | if (definition.getLatexPattern() != null) { |
696 | printer.println("<LATEXPATTERN>" + definition.getLatexPattern() |
697 | + "</LATEXPATTERN>"); |
698 | } |
699 | } |
700 | |
701 | public void visitLeave(final FunctionDefinition definition) { |
702 | printer.popLevel(); |
703 | printer.println("</DEFINITION_FUNCTION>"); |
704 | } |
705 | |
706 | public void visitEnter(final Rule rule) { |
707 | printer.print("<RULE"); |
708 | if (rule.getName() != null) { |
709 | printer.print(" name=\"" + StringUtility.escapeXml(rule.getName()) + "\""); |
710 | } |
711 | if (rule.getVersion() != null) { |
712 | printer.print(" version=\"" + StringUtility.escapeXml(rule.getVersion()) + "\""); |
713 | } |
714 | printer.println(">"); |
715 | printer.pushLevel(); |
716 | } |
717 | |
718 | public void visitLeave(final Rule rule) { |
719 | printer.popLevel(); |
720 | printer.println("</RULE>"); |
721 | } |
722 | |
723 | public void visitEnter(final LinkList linkList) { |
724 | for (int i = 0; i < linkList.size(); i++) { |
725 | printer.print("<LINK"); |
726 | if (linkList.get(i) != null) { |
727 | printer.print(" id=\"" + StringUtility.escapeXml(linkList.get(i)) + "\""); |
728 | } |
729 | printer.println("/>"); |
730 | }; |
731 | } |
732 | |
733 | public void visitEnter(final ChangedRule rule) { |
734 | printer.print("<CHANGED_RULE"); |
735 | if (rule.getName() != null) { |
736 | printer.print(" name=\"" + StringUtility.escapeXml(rule.getName()) + "\""); |
737 | } |
738 | if (rule.getVersion() != null) { |
739 | printer.print(" version=\"" + StringUtility.escapeXml(rule.getVersion()) + "\""); |
740 | } |
741 | printer.println(">"); |
742 | } |
743 | |
744 | public void visitLeave(final ChangedRule rule) { |
745 | printer.println("</CHANGED_RULE>"); |
746 | } |
747 | |
748 | public void visitEnter(final Formula formula) { |
749 | printer.println("<FORMULA>"); |
750 | printer.pushLevel(); |
751 | } |
752 | |
753 | public void visitLeave(final Formula formula) { |
754 | printer.popLevel(); |
755 | printer.println("</FORMULA>"); |
756 | } |
757 | |
758 | public void visitEnter(final Term term) { |
759 | printer.println("<TERM>"); |
760 | printer.pushLevel(); |
761 | } |
762 | |
763 | public void visitLeave(final Term term) { |
764 | printer.popLevel(); |
765 | printer.println("</TERM>"); |
766 | } |
767 | |
768 | // TODO mime 20070217: what do we do if an atom is not first element of a list? |
769 | // we wouldn't get it here!!! But can we think of an output syntax anyway???? |
770 | public void visitEnter(final ElementList list) { |
771 | final String operator = list.getOperator(); |
772 | printer.print("<" + operator); |
773 | final boolean firstIsAtom = list.size() > 0 && list.getElement(0).isAtom(); |
774 | if (firstIsAtom) { |
775 | final String atom = list.getElement(0).getAtom().getString(); |
776 | if (atom != null) { |
777 | if ("VAR".equals(operator) || "PREDVAR".equals(operator) |
778 | || "FUNVAR".equals(operator)) { |
779 | printer.print(" id=\"" + StringUtility.escapeXml(atom) + "\""); |
780 | } else if ("PREDCON".equals(operator) || "FUNCON".equals(operator)) { |
781 | printer.print(" ref=\"" + StringUtility.escapeXml(atom) + "\""); |
782 | } else { |
783 | printer.print(" unknown=\"" + StringUtility.escapeXml(atom) + "\""); |
784 | } |
785 | } |
786 | } |
787 | if (list.size() == 0 || list.size() == 1 && list.getElement(0).isAtom()) { |
788 | printer.print("/"); |
789 | } |
790 | printer.println(">"); |
791 | printer.pushLevel(); |
792 | } |
793 | |
794 | public void visitLeave(final ElementList list) { |
795 | printer.popLevel(); |
796 | if (list.size() == 0 || list.size() == 1 && list.getElement(0).isAtom()) { |
797 | return; |
798 | } |
799 | printer.println("</" + list.getOperator() + ">"); |
800 | } |
801 | |
802 | public void visitEnter(final LiteratureItemList list) { |
803 | printer.println("<BIBLIOGRAPHY>"); |
804 | printer.pushLevel(); |
805 | } |
806 | |
807 | public void visitLeave(final LiteratureItemList list) { |
808 | printer.popLevel(); |
809 | printer.println("</BIBLIOGRAPHY>"); |
810 | } |
811 | |
812 | public void visitEnter(final LiteratureItem item) { |
813 | printer.print("<ITEM"); |
814 | if (item.getLabel() != null) { |
815 | printer.print(" label=\"" + StringUtility.escapeXml(item.getLabel()) + "\""); |
816 | } |
817 | printer.println(">"); |
818 | printer.pushLevel(); |
819 | } |
820 | |
821 | public void visitLeave(final LiteratureItem item) { |
822 | printer.popLevel(); |
823 | printer.println("</ITEM>"); |
824 | } |
825 | |
826 | public String getServiceId() { |
827 | return this.getClass().getName(); |
828 | } |
829 | |
830 | public String getServiceAction() { |
831 | return "generate XML"; |
832 | } |
833 | |
834 | public String getServiceDescription() { |
835 | return "Transformes QEDEQ module into XML data"; |
836 | } |
837 | |
838 | } |