001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.xml.dao;
017
018 import java.io.IOException;
019
020 import org.qedeq.base.io.TextOutput;
021 import org.qedeq.base.utility.StringUtility;
022 import org.qedeq.kernel.bo.KernelContext;
023 import org.qedeq.kernel.bo.common.ServiceProcess;
024 import org.qedeq.kernel.bo.module.ControlVisitor;
025 import org.qedeq.kernel.bo.module.KernelQedeqBo;
026 import org.qedeq.kernel.se.base.list.ElementList;
027 import org.qedeq.kernel.se.base.module.Add;
028 import org.qedeq.kernel.se.base.module.Author;
029 import org.qedeq.kernel.se.base.module.AuthorList;
030 import org.qedeq.kernel.se.base.module.Axiom;
031 import org.qedeq.kernel.se.base.module.ChangedRule;
032 import org.qedeq.kernel.se.base.module.Chapter;
033 import org.qedeq.kernel.se.base.module.Conclusion;
034 import org.qedeq.kernel.se.base.module.ConditionalProof;
035 import org.qedeq.kernel.se.base.module.Existential;
036 import org.qedeq.kernel.se.base.module.FormalProof;
037 import org.qedeq.kernel.se.base.module.FormalProofLine;
038 import org.qedeq.kernel.se.base.module.FormalProofLineList;
039 import org.qedeq.kernel.se.base.module.Formula;
040 import org.qedeq.kernel.se.base.module.FunctionDefinition;
041 import org.qedeq.kernel.se.base.module.Header;
042 import org.qedeq.kernel.se.base.module.Hypothesis;
043 import org.qedeq.kernel.se.base.module.Import;
044 import org.qedeq.kernel.se.base.module.ImportList;
045 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
046 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
047 import org.qedeq.kernel.se.base.module.Latex;
048 import org.qedeq.kernel.se.base.module.LatexList;
049 import org.qedeq.kernel.se.base.module.LinkList;
050 import org.qedeq.kernel.se.base.module.LiteratureItem;
051 import org.qedeq.kernel.se.base.module.LiteratureItemList;
052 import org.qedeq.kernel.se.base.module.Location;
053 import org.qedeq.kernel.se.base.module.LocationList;
054 import org.qedeq.kernel.se.base.module.ModusPonens;
055 import org.qedeq.kernel.se.base.module.Node;
056 import org.qedeq.kernel.se.base.module.PredicateDefinition;
057 import org.qedeq.kernel.se.base.module.Proof;
058 import org.qedeq.kernel.se.base.module.Proposition;
059 import org.qedeq.kernel.se.base.module.Qedeq;
060 import org.qedeq.kernel.se.base.module.Rename;
061 import org.qedeq.kernel.se.base.module.Rule;
062 import org.qedeq.kernel.se.base.module.Section;
063 import org.qedeq.kernel.se.base.module.Specification;
064 import org.qedeq.kernel.se.base.module.Subsection;
065 import org.qedeq.kernel.se.base.module.SubsectionList;
066 import org.qedeq.kernel.se.base.module.SubstFree;
067 import org.qedeq.kernel.se.base.module.SubstFunc;
068 import org.qedeq.kernel.se.base.module.SubstPred;
069 import org.qedeq.kernel.se.base.module.Term;
070 import org.qedeq.kernel.se.base.module.Universal;
071 import org.qedeq.kernel.se.base.module.UsedByList;
072 import org.qedeq.kernel.se.common.Plugin;
073 import org.qedeq.kernel.se.common.SourceFileExceptionList;
074
075
076 /**
077 * This class prints a QEDEQ module in XML format in an output stream.
078 *
079 * @author Michael Meyling
080 */
081 public final class Qedeq2Xml extends ControlVisitor implements Plugin {
082
083 /** Output goes here. */
084 private TextOutput printer;
085
086 /**
087 * Constructor.
088 *
089 * @param plugin This plugin we work for.
090 * @param bo QEDEQ BO.
091 * @param printer Print herein.
092 */
093 public Qedeq2Xml(final Plugin plugin, final KernelQedeqBo bo, final TextOutput printer) {
094 super(plugin, bo);
095 this.printer = printer;
096 }
097
098 /**
099 * 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 ServiceProcess process,
109 final Plugin 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 getPluginId() {
827 return this.getClass().getName();
828 }
829
830 public String getPluginActionName() {
831 return "generate XML";
832 }
833
834 public String getPluginDescription() {
835 return "Transformes QEDEQ module into XML data";
836 }
837
838 }
|