001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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.bo.service;
017
018 import org.qedeq.base.trace.Trace;
019 import org.qedeq.kernel.bo.module.ControlVisitor;
020 import org.qedeq.kernel.bo.module.Element2Latex;
021 import org.qedeq.kernel.bo.module.Element2Utf8;
022 import org.qedeq.kernel.bo.module.KernelQedeqBo;
023 import org.qedeq.kernel.bo.module.ModuleLabels;
024 import org.qedeq.kernel.se.base.module.Axiom;
025 import org.qedeq.kernel.se.base.module.FunctionDefinition;
026 import org.qedeq.kernel.se.base.module.Import;
027 import org.qedeq.kernel.se.base.module.Node;
028 import org.qedeq.kernel.se.base.module.PredicateDefinition;
029 import org.qedeq.kernel.se.base.module.Proposition;
030 import org.qedeq.kernel.se.base.module.Rule;
031 import org.qedeq.kernel.se.common.ModuleDataException;
032 import org.qedeq.kernel.se.common.Plugin;
033 import org.qedeq.kernel.se.common.SourceFileExceptionList;
034 import org.qedeq.kernel.se.dto.module.NodeVo;
035
036
037 /**
038 * Create mapping from labels to {@link org.qedeq.kernel.se.dto.module.NodeVo} for a QEDEQ module.
039 *
040 * @author Michael Meyling
041 */
042 public final class ModuleLabelsCreator extends ControlVisitor {
043
044 /** This class. */
045 private static final Class CLASS = ModuleLabelsCreator.class;
046
047 /** QEDEQ module labels, definitions, references, etc. */
048 private ModuleLabels labels;
049
050 /** Converter to LaTeX. */
051 private Element2LatexImpl converter;
052
053 /** Converter to UTF-8 text. */
054 private Element2Utf8Impl textConverter;
055
056 /**
057 * Constructor.
058 *
059 * @param plugin This plugin we work for.
060 * @param prop Internal QedeqBo.
061 */
062 public ModuleLabelsCreator(final Plugin plugin, final KernelQedeqBo prop) {
063 super(plugin, prop);
064 }
065
066 /**
067 * Visit import. Loads referenced QEDEQ module and saves reference.
068 *
069 * @param imp Begin visit of this element.
070 */
071 public void visitEnter(final Import imp) {
072 try {
073 this.labels.addLabel(getCurrentContext(),
074 imp.getLabel());
075 } catch (ModuleDataException me) {
076 addError(me);
077 Trace.trace(CLASS, this, "visitEnter(Import)", me);
078 }
079 }
080
081 /**
082 * Increase axiom counter.
083 *
084 * @param axiom Visit this element.
085 */
086 public void visitEnter(final Axiom axiom) {
087 setBlocked(true); // block further traverse
088 }
089
090 /**
091 * Increase proposition counter.
092 *
093 * @param proposition Begin visit of this element.
094 */
095 public void visitEnter(final Proposition proposition) {
096 setBlocked(true); // block further traverse
097 }
098
099 /**
100 * Increase function definition counter.
101 *
102 * @param funcDef Begin visit of this element.
103 */
104 public void visitEnter(final FunctionDefinition funcDef) {
105 setBlocked(true); // block further traverse
106 // we always save the definition, even if there already exists an entry
107 labels.addFunction(funcDef, getCurrentContext());
108 }
109
110 /**
111 * Increase predicate definition counter.
112 *
113 * @param predDef Begin visit of this element.
114 */
115 public void visitEnter(final PredicateDefinition predDef) {
116 setBlocked(true); // block further traverse
117 // we always save the definition, even if there already exists an entry
118 labels.addPredicate(predDef, getCurrentContext());
119 }
120
121 /**
122 * Increase rule counter.
123 *
124 * @param rule Begin visit of this element.
125 */
126 public void visitEnter(final Rule rule) {
127 setBlocked(true); // block further traverse
128 }
129
130 /**
131 * Add node and counter informations.
132 *
133 * @param node End visit of this element.
134 */
135 public void visitLeave(final Node node) {
136 try {
137 this.labels.addNode(getCurrentContext(), (NodeVo) node, getQedeqBo(),
138 getCurrentNumbers());
139 } catch (ModuleDataException me) {
140 addError(me);
141 Trace.trace(CLASS, this, "visitEnter(Node)", me);
142 }
143 setBlocked(false); // allow further traverse
144 }
145
146 /**
147 * Create QEDEQ module labels and Element2Latex converter.
148 *
149 * @throws SourceFileExceptionList Traverse lead to errors.
150 */
151 public void createLabels() throws SourceFileExceptionList {
152 if (this.labels == null) {
153 this.labels = new ModuleLabels();
154 this.converter = new Element2LatexImpl(this.labels);
155 this.textConverter = new Element2Utf8Impl(this.converter);
156 traverse();
157 }
158 }
159
160 /**
161 * Get QEDEQ module labels.
162 *
163 * @return QEDEQ module labels. */
164 public ModuleLabels getLabels() {
165 return labels;
166 }
167
168 /**
169 * Get converter for module elements.
170 *
171 * @return Element to LaTeX converter.
172 */
173 public Element2Latex getConverter() {
174 return converter;
175 }
176
177 /**
178 * Get converter for module elements.
179 *
180 * @return Element to UTF-8 converter.
181 */
182 public Element2Utf8 getTextConverter() {
183 return textConverter;
184 }
185
186 }
|