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