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