Coverage Report

Coverage Report - net.sourceforge.jeuclid.elements.support.operatordict.OperatorDictionary3

Classes in this File

Line Coverage

Branch Coverage

Complexity

OperatorDictionary3

10%

20/190

6/75

2,923

OperatorDictionary3$PersonalNamespaceContext

0/25

0/12

2,923

 /*
  * Copyright 2009 - 2009 JEuclid, http://jeuclid.sf.net
  *
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
  * You may obtain a copy of the License at
  *
  *      http://www.apache.org/licenses/LICENSE-2.0
  *
  * Unless required by applicable law or agreed to in writing, software
  * distributed under the License is distributed on an "AS IS" BASIS,
  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  * See the License for the specific language governing permissions and
  * limitations under the License.
  */
 
 /* $Id: OperatorDictionary3.java,v f5d68b2c52ae 2010/08/13 10:03:30 max $ */
 
 package net.sourceforge.jeuclid.elements.support.operatordict;
 
 import java.io.IOException;
 import java.io.InputStream;
 import java.io.Serializable;
 import java.util.EnumMap;
 import java.util.HashMap;
 import java.util.Iterator;
 import java.util.Map;
 
 import javax.xml.XMLConstants;
 import javax.xml.namespace.NamespaceContext;
 import javax.xml.xpath.XPath;
 import javax.xml.xpath.XPathConstants;
 import javax.xml.xpath.XPathExpression;
 import javax.xml.xpath.XPathExpressionException;
 import javax.xml.xpath.XPathFactory;
 
 import net.sourceforge.jeuclid.Constants;
 import net.sourceforge.jeuclid.elements.support.NamespaceContextAdder;
 import net.sourceforge.jeuclid.parser.Parser;
 
 import org.apache.commons.logging.Log;
 import org.apache.commons.logging.LogFactory;
 import org.w3c.dom.Document;
 import org.w3c.dom.Node;
 import org.w3c.dom.NodeList;
 import org.xml.sax.SAXException;
 
 /**
  * Implements an operator dictionary based on the MathML 3 spec.
  *
  * @version $Revision: f5d68b2c52ae $
  */
 public final class OperatorDictionary3 extends AbstractOperatorDictionary
         implements Serializable {
 
     /**
      * Logger for this class.
      */
     private static final Log LOGGER = LogFactory
             .getLog(OperatorDictionary3.class);
 
     private static final String NO_SPACE = "0em";
 
     private static final int INT_NO_SPACE = 0;
 
     private static final int INT_VERYVERYTHINMATHSPACE = 1;
 
     private static final int INT_VERYTHINMATHSPACE = 2;
 
     private static final int INT_THINMATHSPACE = 3;
 
     private static final int INT_MEDIUMMATHSPACE = 4;
 
     private static final int INT_THICKMATHSPACE = 5;
 
     private static final int INT_VERYTHICKMATHSPACE = 6;
 
     private static final int INT_VERYVERYTHICKMATHSPACE = 7;
 
     /**
      *
      */
     private static final long serialVersionUID = 1L;
 
     /**
      * MathML dictionary resource.
      */
     private static final String DICTIONARY_FILE = "/net/sourceforge/jeuclid/appendixc.xml";
 
     /**
      * MathML dictionary serialized resource.
      */
     private static final String DICTIONARY_SERIALIZED = "/net/sourceforge/jeuclid/appendixc.ser";
 
     /**
      * The instance of the Dictionary
      */
     private static OperatorDictionary instance;
 
     private class PersonalNamespaceContext implements NamespaceContext {
 
         public PersonalNamespaceContext() {
         }
 
         /** {@inheritDoc} */
         public String getNamespaceURI(final String prefix) {
             final String retVal;
             if ("html".equals(prefix)) {
                 retVal = "http://www.w3.org/1999/xhtml";
             } else if ("xml".equals(prefix)) {
                 retVal = XMLConstants.XML_NS_URI;
             } else {
                 retVal = XMLConstants.NULL_NS_URI;
             }
             return retVal;
         }
 
         /** {@inheritDoc} */
         // This method isn't necessary for XPath processing.
         public String getPrefix(final String uri) {
             throw new UnsupportedOperationException();
         }
 
         /** {@inheritDoc} */
         // This method isn't necessary for XPath processing either.
         public Iterator<String> getPrefixes(final String uri) {
             throw new UnsupportedOperationException();
         }
 
     }
 
     private OperatorDictionary3() {
         // nothing to do.
     }
 
     /**
      * Get the for singleton instance.
      *
      * @return an instance of OperatorDictionary.
      */
     public static OperatorDictionary getInstance() {
         synchronized (OperatorDictionary3.class) {
             if (OperatorDictionary3.instance == null) {
                 final OperatorDictionary newDict = AbstractOperatorDictionary
                         .deserialize(OperatorDictionary3.DICTIONARY_SERIALIZED);
                 if (newDict == null) {
                     OperatorDictionary3.instance = new OperatorDictionary3();
                 } else {
                     OperatorDictionary3.instance = newDict;
                 }
             }
         }
         return OperatorDictionary3.instance;
     }
 
     /** {@inheritDoc} */
     @Override
     protected void initializeFromXML(
             final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict) {
         try {
             final Document doc = this.loadDocument();
             final XPath xpath = this.createXPath();
             this.extractValuesFromDocument(doc, xpath, dict);
         } catch (final SAXException e) {
             OperatorDictionary3.LOGGER.warn(
                     "XML Could not be parsed in operator dictionary", e);
         } catch (final IOException e) {
             OperatorDictionary3.LOGGER.warn(
                     "IO error reading operator dictionary", e);
         } catch (final XPathExpressionException e) {
             OperatorDictionary3.LOGGER.warn(
                     "XPath error in operator dictionary", e);
         }
     }
 
     /**
      * @param doc
      * @param xpath
      * @throws XPathExpressionException
      */
     private void extractValuesFromDocument(
             final Document doc,
             final XPath xpath,
             final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict)
             throws XPathExpressionException {
         final XPathExpression expr = xpath
                 .compile("//html:table[@class='sortable']/html:tbody/html:tr");
 
         final XPathExpression operatorExpr = xpath
                 .compile("html:th[2]/text()");
         final XPathExpression formExpr = xpath.compile("html:th[4]/text()");
         final XPathExpression lspaceExpr = xpath.compile("html:td[2]/text()");
         final XPathExpression rspaceExpr = xpath.compile("html:td[3]/text()");
         final XPathExpression minsizeExpr = xpath
                 .compile("html:td[4]/text()");
         final XPathExpression propertiesExpr = xpath
                 .compile("html:td[5]/text()");
 
         final NodeList result = (NodeList) expr.evaluate(doc,
                 XPathConstants.NODESET);
 
         for (int i = 0; i < result.getLength(); i++) {
             final Node trNode = result.item(i);
             final String operator = (String) operatorExpr.evaluate(trNode,
                     XPathConstants.STRING);
             final String formStr = (String) formExpr.evaluate(trNode,
                     XPathConstants.STRING);
             final OperatorForm form = OperatorForm.parseOperatorForm(formStr);
             final String lspace = (String) lspaceExpr.evaluate(trNode,
                     XPathConstants.STRING);
             final String rspace = (String) rspaceExpr.evaluate(trNode,
                     XPathConstants.STRING);
             final String minsize = (String) minsizeExpr.evaluate(trNode,
                     XPathConstants.STRING);
             final String propertiesString = (String) propertiesExpr.evaluate(
                     trNode, XPathConstants.STRING);
 
             this.addAttr(operator, form, OperatorAttribute.LSPACE, this
                     .intToSpace(lspace), dict);
             this.addAttr(operator, form, OperatorAttribute.RSPACE, this
                     .intToSpace(rspace), dict);
             if (minsize.length() > 0) {
                 this.addAttr(operator, form, OperatorAttribute.MINSIZE,
                         minsize, dict);
             }
             this.addProperties(operator, form, propertiesString, dict);
         }
     }
 
     /**
      * @return
      * @throws SAXException
      * @throws IOException
      */
     private Document loadDocument() throws SAXException, IOException {
         final InputStream is = OperatorDictionary3.class
                 .getResourceAsStream(OperatorDictionary3.DICTIONARY_FILE);
         final Document doc = Parser.getInstance().getDocumentBuilder().parse(
                 is);
         return doc;
     }
 
     /**
      * @return
      */
     private XPath createXPath() {
         final XPathFactory factory = XPathFactory.newInstance();
         final XPath xpath = factory.newXPath();
         final NamespaceContext xml = new NamespaceContextAdder("xml",
                 XMLConstants.XML_NS_URI, null);
         final NamespaceContext html = new NamespaceContextAdder("html",
                 "http://www.w3.org/1999/xhtml", xml);
         xpath.setNamespaceContext(html);
         return xpath;
     }
 
     /**
      * @param operator
      * @param form
      * @param propertiesString
      */
     private void addProperties(
             final String operator,
             final OperatorForm form,
             final String propertiesString,
             final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict) {
         final String[] properties = propertiesString.split(" ");
         for (final String property : properties) {
             if (property.length() > 0) {
                 try {
                     final OperatorAttribute oa = OperatorAttribute
                             .parseOperatorAttribute(property);
                     this.addAttr(operator, form, oa, Constants.TRUE, dict);
                 } catch (final UnknownAttributeException uae) {
                     OperatorDictionary3.LOGGER.warn(
                             "Unkown Attribute when reading operator dictionary: "
                                     + property, uae);
                 }
             }
         }
     }
 
     /**
      * @param operator
      * @param form
      * @param lspace
      * @param intToSpace
      */
     private void addAttr(
             final String operator,
             final OperatorForm form,
             final OperatorAttribute attribute,
             final String value,
             final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict) {
 
         Map<String, Map<OperatorForm, String>> innerMap1 = dict
                 .get(attribute);
         if (innerMap1 == null) {
             innerMap1 = new HashMap<String, Map<OperatorForm, String>>();
             dict.put(attribute, innerMap1);
         }
 
         Map<OperatorForm, String> innerMap2 = innerMap1.get(operator);
         if (innerMap2 == null) {
             innerMap2 = new EnumMap<OperatorForm, String>(OperatorForm.class);
             innerMap1.put(operator, innerMap2);
         }
 
         innerMap2.put(form, value);
     }
 
     /**
      * @param lspace
      * @return
      */
     private String intToSpace(final String spaceInt) {
         String retVal;
         try {
             final int i = Integer.parseInt(spaceInt);
             switch (i) {
             case OperatorDictionary3.INT_NO_SPACE:
                 retVal = OperatorDictionary3.NO_SPACE;
                 break;
             case OperatorDictionary3.INT_VERYVERYTHINMATHSPACE:
                 retVal = OperatorDictionary.NAME_VERYVERYTHINMATHSPACE;
                 break;
             case OperatorDictionary3.INT_VERYTHINMATHSPACE:
                 retVal = OperatorDictionary.NAME_VERYTHINMATHSPACE;
                 break;
             case OperatorDictionary3.INT_THINMATHSPACE:
                 retVal = OperatorDictionary.NAME_THINMATHSPACE;
                 break;
             case OperatorDictionary3.INT_MEDIUMMATHSPACE:
                 retVal = OperatorDictionary.NAME_MEDIUMMATHSPACE;
                 break;
             case OperatorDictionary3.INT_THICKMATHSPACE:
                 retVal = OperatorDictionary.NAME_THICKMATHSPACE;
                 break;
             case OperatorDictionary3.INT_VERYTHICKMATHSPACE:
                 retVal = OperatorDictionary.NAME_VERYTHICKMATHSPACE;
                 break;
             case OperatorDictionary3.INT_VERYVERYTHICKMATHSPACE:
                 retVal = OperatorDictionary.NAME_VERYVERYTHICKMATHSPACE;
                 break;
             default:
                 retVal = OperatorDictionary3.NO_SPACE;
             }
         } catch (final NumberFormatException e) {
             retVal = OperatorDictionary3.NO_SPACE;
         }
         return retVal;
     }
 
 }

1		/*
2		* Copyright 2009 - 2009 JEuclid, http://jeuclid.sf.net
3		*
4		* Licensed under the Apache License, Version 2.0 (the "License");
5		* you may not use this file except in compliance with the License.
6		* You may obtain a copy of the License at
7		*
8		* http://www.apache.org/licenses/LICENSE-2.0
9		*
10		* Unless required by applicable law or agreed to in writing, software
11		* distributed under the License is distributed on an "AS IS" BASIS,
12		* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13		* See the License for the specific language governing permissions and
14		* limitations under the License.
15		*/
16
17		/* $Id: OperatorDictionary3.java,v f5d68b2c52ae 2010/08/13 10:03:30 max $ */
18
19		package net.sourceforge.jeuclid.elements.support.operatordict;
20
21		import java.io.IOException;
22		import java.io.InputStream;
23		import java.io.Serializable;
24		import java.util.EnumMap;
25		import java.util.HashMap;
26		import java.util.Iterator;
27		import java.util.Map;
28
29		import javax.xml.XMLConstants;
30		import javax.xml.namespace.NamespaceContext;
31		import javax.xml.xpath.XPath;
32		import javax.xml.xpath.XPathConstants;
33		import javax.xml.xpath.XPathExpression;
34		import javax.xml.xpath.XPathExpressionException;
35		import javax.xml.xpath.XPathFactory;
36
37		import net.sourceforge.jeuclid.Constants;
38		import net.sourceforge.jeuclid.elements.support.NamespaceContextAdder;
39		import net.sourceforge.jeuclid.parser.Parser;
40
41		import org.apache.commons.logging.Log;
42		import org.apache.commons.logging.LogFactory;
43		import org.w3c.dom.Document;
44		import org.w3c.dom.Node;
45		import org.w3c.dom.NodeList;
46		import org.xml.sax.SAXException;
47
48		/**
49		* Implements an operator dictionary based on the MathML 3 spec.
50		*
51		* @version $Revision: f5d68b2c52ae $
52		*/
53		public final class OperatorDictionary3 extends AbstractOperatorDictionary
54		implements Serializable {
55
56		/**
57		* Logger for this class.
58	201	*/
59	8	private static final Log LOGGER = LogFactory
60		.getLog(OperatorDictionary3.class);
61
62		private static final String NO_SPACE = "0em";
63
64		private static final int INT_NO_SPACE = 0;
65
66		private static final int INT_VERYVERYTHINMATHSPACE = 1;
67
68		private static final int INT_VERYTHINMATHSPACE = 2;
69
70		private static final int INT_THINMATHSPACE = 3;
71
72		private static final int INT_MEDIUMMATHSPACE = 4;
73
74		private static final int INT_THICKMATHSPACE = 5;
75
76		private static final int INT_VERYTHICKMATHSPACE = 6;
77
78		private static final int INT_VERYVERYTHICKMATHSPACE = 7;
79
80		/**
81		*
82		*/
83		private static final long serialVersionUID = 1L;
84
85	0	/**
86	0	* MathML dictionary resource.
87		*/
88		private static final String DICTIONARY_FILE = "/net/sourceforge/jeuclid/appendixc.xml";
89
90		/**
91	0	* MathML dictionary serialized resource.
92	0	*/
93	0	private static final String DICTIONARY_SERIALIZED = "/net/sourceforge/jeuclid/appendixc.ser";
94	0
95		/**
96	0	* The instance of the Dictionary
97		*/
98	0	private static OperatorDictionary instance;
99
100		private class PersonalNamespaceContext implements NamespaceContext {
101	0
102	0	public PersonalNamespaceContext() {
103	0	}
104	0
105		/** {@inheritDoc} */
106		public String getNamespaceURI(final String prefix) {
107	0	final String retVal;
108	0	if ("html".equals(prefix)) {
109	0	retVal = "http://www.w3.org/1999/xhtml";
110	0	} else if ("xml".equals(prefix)) {
111	0	retVal = XMLConstants.XML_NS_URI;
112	0	} else {
113	0	retVal = XMLConstants.NULL_NS_URI;
114	0	}
115	0	return retVal;
116		}
117	0
118		/** {@inheritDoc} */
119		// This method isn't necessary for XPath processing.
120	0	public String getPrefix(final String uri) {
121	0	throw new UnsupportedOperationException();
122		}
123
124		/** {@inheritDoc} */
125	2	// This method isn't necessary for XPath processing either.
126	2	public Iterator<String> getPrefixes(final String uri) {
127	2	throw new UnsupportedOperationException();
128		}
129	2
130	0	}
131	0
132	2	private OperatorDictionary3() {
133	0	// nothing to do.
134	0	}
135	2
136	2	/**
137		* Get the for singleton instance.
138		*
139		* @return an instance of OperatorDictionary.
140		*/
141	199	public static OperatorDictionary getInstance() {
142	207	synchronized (OperatorDictionary3.class) {
143	207	if (OperatorDictionary3.instance == null) {
144	8	final OperatorDictionary newDict = AbstractOperatorDictionary
145	199	.deserialize(OperatorDictionary3.DICTIONARY_SERIALIZED);
146	8	if (newDict == null) {
147	0	OperatorDictionary3.instance = new OperatorDictionary3();
148	199	} else {
149	8	OperatorDictionary3.instance = newDict;
150	0	}
151	199	}
152	207	}
153	8	return OperatorDictionary3.instance;
154	0	}
155
156	0	/** {@inheritDoc} */
157	0	@Override
158		protected void initializeFromXML(
159		final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict) {
160	0	try {
161	0	final Document doc = this.loadDocument();
162	0	final XPath xpath = this.createXPath();
163	0	this.extractValuesFromDocument(doc, xpath, dict);
164	0	} catch (final SAXException e) {
165	0	OperatorDictionary3.LOGGER.warn(
166	0	"XML Could not be parsed in operator dictionary", e);
167	0	} catch (final IOException e) {
168	0	OperatorDictionary3.LOGGER.warn(
169	0	"IO error reading operator dictionary", e);
170	0	} catch (final XPathExpressionException e) {
171	0	OperatorDictionary3.LOGGER.warn(
172	0	"XPath error in operator dictionary", e);
173	0	}
174	0	}
175	0
176	0	/**
177	0	* @param doc
178		* @param xpath
179		* @throws XPathExpressionException
180	0	*/
181		private void extractValuesFromDocument(
182		final Document doc,
183	0	final XPath xpath,
184	0	final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict)
185	0	throws XPathExpressionException {
186	0	final XPathExpression expr = xpath
187	0	.compile("//html:table[@class='sortable']/html:tbody/html:tr");
188	0
189	0	final XPathExpression operatorExpr = xpath
190	0	.compile("html:th[2]/text()");
191	0	final XPathExpression formExpr = xpath.compile("html:th[4]/text()");
192	0	final XPathExpression lspaceExpr = xpath.compile("html:td[2]/text()");
193	0	final XPathExpression rspaceExpr = xpath.compile("html:td[3]/text()");
194	0	final XPathExpression minsizeExpr = xpath
195	0	.compile("html:td[4]/text()");
196	0	final XPathExpression propertiesExpr = xpath
197		.compile("html:td[5]/text()");
198	0
199	0	final NodeList result = (NodeList) expr.evaluate(doc,
200		XPathConstants.NODESET);
201	0
202	0	for (int i = 0; i < result.getLength(); i++) {
203	0	final Node trNode = result.item(i);
204	0	final String operator = (String) operatorExpr.evaluate(trNode,
205	0	XPathConstants.STRING);
206	0	final String formStr = (String) formExpr.evaluate(trNode,
207	0	XPathConstants.STRING);
208	0	final OperatorForm form = OperatorForm.parseOperatorForm(formStr);
209	0	final String lspace = (String) lspaceExpr.evaluate(trNode,
210	0	XPathConstants.STRING);
211	0	final String rspace = (String) rspaceExpr.evaluate(trNode,
212	0	XPathConstants.STRING);
213	0	final String minsize = (String) minsizeExpr.evaluate(trNode,
214	0	XPathConstants.STRING);
215	0	final String propertiesString = (String) propertiesExpr.evaluate(
216		trNode, XPathConstants.STRING);
217	0
218	0	this.addAttr(operator, form, OperatorAttribute.LSPACE, this
219	0	.intToSpace(lspace), dict);
220	0	this.addAttr(operator, form, OperatorAttribute.RSPACE, this
221	0	.intToSpace(rspace), dict);
222	0	if (minsize.length() > 0) {
223	0	this.addAttr(operator, form, OperatorAttribute.MINSIZE,
224		minsize, dict);
225	0	}
226	0	this.addProperties(operator, form, propertiesString, dict);
227	0	}
228	0	}
229	0
230	0	/**
231	0	* @return
232		* @throws SAXException
233		* @throws IOException
234		*/
235	0	private Document loadDocument() throws SAXException, IOException {
236	0	final InputStream is = OperatorDictionary3.class
237	0	.getResourceAsStream(OperatorDictionary3.DICTIONARY_FILE);
238	0	final Document doc = Parser.getInstance().getDocumentBuilder().parse(
239	0	is);
240	0	return doc;
241		}
242
243		/**
244	0	* @return
245	0	*/
246	0	private XPath createXPath() {
247	0	final XPathFactory factory = XPathFactory.newInstance();
248	0	final XPath xpath = factory.newXPath();
249	0	final NamespaceContext xml = new NamespaceContextAdder("xml",
250	0	XMLConstants.XML_NS_URI, null);
251	0	final NamespaceContext html = new NamespaceContextAdder("html",
252	0	"http://www.w3.org/1999/xhtml", xml);
253	0	xpath.setNamespaceContext(html);
254	0	return xpath;
255	0	}
256
257		/**
258	0	* @param operator
259		* @param form
260		* @param propertiesString
261		*/
262	0	private void addProperties(
263	0	final String operator,
264	0	final OperatorForm form,
265		final String propertiesString,
266	0	final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict) {
267	0	final String[] properties = propertiesString.split(" ");
268	0	for (final String property : properties) {
269	0	if (property.length() > 0) {
270	0	try {
271	0	final OperatorAttribute oa = OperatorAttribute
272		.parseOperatorAttribute(property);
273	0	this.addAttr(operator, form, oa, Constants.TRUE, dict);
274	0	} catch (final UnknownAttributeException uae) {
275	0	OperatorDictionary3.LOGGER.warn(
276	0	"Unkown Attribute when reading operator dictionary: "
277		+ property, uae);
278	0	}
279	0	}
280	0	}
281	0	}
282	0
283		/**
284		* @param operator
285	0	* @param form
286	0	* @param lspace
287		* @param intToSpace
288		*/
289		private void addAttr(
290		final String operator,
291	0	final OperatorForm form,
292		final OperatorAttribute attribute,
293	0	final String value,
294	0	final Map<OperatorAttribute, Map<String, Map<OperatorForm, String>>> dict) {
295	0
296	0	Map<String, Map<OperatorForm, String>> innerMap1 = dict
297		.get(attribute);
298	0	if (innerMap1 == null) {
299	0	innerMap1 = new HashMap<String, Map<OperatorForm, String>>();
300	0	dict.put(attribute, innerMap1);
301	0	}
302	0
303	0	Map<OperatorForm, String> innerMap2 = innerMap1.get(operator);
304	0	if (innerMap2 == null) {
305	0	innerMap2 = new EnumMap<OperatorForm, String>(OperatorForm.class);
306	0	innerMap1.put(operator, innerMap2);
307	0	}
308	0
309	0	innerMap2.put(form, value);
310	0	}
311	0
312		/**
313	0	* @param lspace
314	0	* @return
315	0	*/
316	0	private String intToSpace(final String spaceInt) {
317	0	String retVal;
318	0	try {
319	0	final int i = Integer.parseInt(spaceInt);
320	0	switch (i) {
321	0	case OperatorDictionary3.INT_NO_SPACE:
322	0	retVal = OperatorDictionary3.NO_SPACE;
323	0	break;
324	0	case OperatorDictionary3.INT_VERYVERYTHINMATHSPACE:
325	0	retVal = OperatorDictionary.NAME_VERYVERYTHINMATHSPACE;
326	0	break;
327	0	case OperatorDictionary3.INT_VERYTHINMATHSPACE:
328	0	retVal = OperatorDictionary.NAME_VERYTHINMATHSPACE;
329	0	break;
330	0	case OperatorDictionary3.INT_THINMATHSPACE:
331	0	retVal = OperatorDictionary.NAME_THINMATHSPACE;
332	0	break;
333	0	case OperatorDictionary3.INT_MEDIUMMATHSPACE:
334	0	retVal = OperatorDictionary.NAME_MEDIUMMATHSPACE;
335	0	break;
336	0	case OperatorDictionary3.INT_THICKMATHSPACE:
337	0	retVal = OperatorDictionary.NAME_THICKMATHSPACE;
338	0	break;
339	0	case OperatorDictionary3.INT_VERYTHICKMATHSPACE:
340	0	retVal = OperatorDictionary.NAME_VERYTHICKMATHSPACE;
341	0	break;
342		case OperatorDictionary3.INT_VERYVERYTHICKMATHSPACE:
343	0	retVal = OperatorDictionary.NAME_VERYVERYTHICKMATHSPACE;
344	0	break;
345	0	default:
346	0	retVal = OperatorDictionary3.NO_SPACE;
347		}
348	0	} catch (final NumberFormatException e) {
349	0	retVal = OperatorDictionary3.NO_SPACE;
350	0	}
351	0	return retVal;
352		}
353
354		}