package org.ai4fm.proofprocess.zeves.parse;

import java.io.IOException;

import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.base.util.UnmarshalException;
import net.sourceforge.czt.parser.util.DeleteAnnVisitor;
import net.sourceforge.czt.parser.util.ParseException;
import net.sourceforge.czt.parser.zeves.ParseUtils;
import net.sourceforge.czt.print.util.XmlString;
import net.sourceforge.czt.session.CommandException;
import net.sourceforge.czt.session.Key;
import net.sourceforge.czt.session.Markup;
import net.sourceforge.czt.session.SectionManager;
import net.sourceforge.czt.session.Source;
import net.sourceforge.czt.session.StringSource;

/**
 * @author Andrius Velykis
 */
public class ZmlTermParser {

	private static final String ZML_PRINT_KEY = "term-zml";
	
	public static String convertToZml(Term cztTerm) {
		
		// strip all annotations (e.g. LocAnn, etc) during serialization
		cztTerm.accept(new DeleteAnnVisitor());
		
		// create new section manager
		SectionManager sectInfo = new SectionManager("zeves");
		
		sectInfo.put(new Key<Term>(ZML_PRINT_KEY, Term.class), cztTerm);
		try {
			
			XmlString printed = sectInfo.get(new Key<XmlString>(ZML_PRINT_KEY, XmlString.class));
			return printed.toString();
			
		} catch (CommandException e) {
			// TODO log?
			e.printStackTrace();
		}
		
		return null;
	}
	
	public static Term parseZml(String zml) {
		
		// create new section manager
		SectionManager sectInfo = new SectionManager("zeves");
		
		Source zmlSource = new StringSource(zml, ZML_PRINT_KEY);
		zmlSource.setMarkup(Markup.ZML);
		
		// TODO use SectionInfo (arbitrary ZML (non-Spec/ZSect) not supported at the moment)
		try {
			return ParseUtils.parse(zmlSource, sectInfo);
		} catch (ParseException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		} catch (IOException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		} catch (UnmarshalException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		
		return null;
	}
	
}

@@ -53,27 +53,90 @@
 java.io.
-IOException
+StringReader;%0Aimport java.io.StringWriter;%0A%0Aimport org.xml.sax.InputSource
 ;%0A%0Aimpor
@@ -317,414 +317,85 @@
 czt.
-parser.util.ParseException;%0Aimport net.sourceforge.czt.parser.zeves.ParseUtils;%0Aimport net.sourceforge.czt.print.util.XmlString;%0Aimport net.sourceforge.czt.session.CommandException;%0Aimport net.sourceforge.czt.session.Key;%0Aimport net.sourceforge.czt.session.Markup;%0Aimport net.sourceforge.czt.session.SectionManager;%0Aimport net.sourceforge.czt.session.Source;%0Aimport net.sourceforge.czt.session.StringSource
+zeves.jaxb.JaxbXmlReader;%0Aimport net.sourceforge.czt.zeves.jaxb.JaxbXmlWriter
 ;%0A%0A/
@@ -462,67 +462,8 @@
  %7B%0A%0A
-%09private static final String ZML_PRINT_KEY = %22term-zml%22;%0A%09%0A
 %09pub
@@ -633,548 +633,528 @@
 %09// 
-create new section manager%0A%09%09SectionManager sectInfo = new SectionManager(%22zeves%22);%0A%09%09%0A%09%09sectInfo.put(new Key%3CTerm%3E(ZML_PRINT_KEY, Term.class), cztTerm);%0A%09%09try %7B%0A%09%09%09%0A%09%09%09XmlString p
+use the JAXB writer directly, instead of going via SectionManager%0A%09%09// this allows us to avoid instantiating SectionManager%0A%09%09// and we always use the %22zeves%22 JAXB writer%0A%09%09JaxbXmlWriter xmlW
 ri
-n
 te
-d = sectInfo.get(new Key%3CXmlString%3E(ZML_PRINT_KEY, XmlString.class));%0A%09%09%09return printed.toString();%0A%09%09%09%0A%09%09%7D catch (CommandException e) %7B%0A%09%09%09// TODO log?%0A%09%09%09e.printStackTrace();%0A%09%09%7D%0A%09%09%0A%09%09return null;%0A%09%7D%0A%09%0A%09public static Term parseZml(String zml) %7B%0A%09%09%0A%09%09// create new section manager%0A%09%09SectionManager sectInfo = new SectionManager(%22zeves%22);%0A%09%09%0A%09%09
+r = new JaxbXmlWriter();%0A%09%09%0A%09%09StringWriter writer = new StringWriter();%0A%09%09xmlWriter.write(cztTerm, writer);%0A%09%09%0A%09%09return writer.toString();%0A%09%7D%0A%09%0A%09public static Term parseZml(String zml) %7B%0A%09%09%0A%09%09// use the JAXB reader directly to avoid instantiating a SectionManager%0A%09%09JaxbXmlReader reader = new JaxbXmlReader();%0A%09%09Input
 Source 
-zmlS
+s
 ourc
@@ -1165,221 +1165,80 @@
 new 
-StringSource(zml, ZML_PRINT_KEY);%0A%09%09zmlSource.setMarkup(Markup.ZML);%0A%09%09%0A%09%09// TODO use SectionInfo (arbitrary ZML (non-Spec/ZSect) not supported at the moment)%0A%09%09try %7B%0A%09%09%09return ParseUtils.parse(zmlSource, sectInfo
+InputSource(new StringReader(zml));%0A%09%09try %7B%0A%09%09%09return reader.read(source
 );%0A%09
@@ -1247,21 +1247,25 @@
  catch (
-Parse
+Unmarshal
 Exceptio
@@ -1286,221 +1286,33 @@
 ODO 
-Auto-generated catch block%0A%09%09%09e.printStackTrace();%0A%09%09%7D catch (IOException e) %7B%0A%09%09%09// TODO Auto-generated catch block%0A%09%09%09e.printStackTrace();%0A%09%09%7D catch (UnmarshalException e) %7B%0A%09%09%09// TODO Auto-generated catch block
+handle the errors better?
 %0A%09%09%09
@@ -1337,14 +1337,8 @@
 );%0A%09
-%09%7D%0A%09%09%0A
 %09%09re
@@ -1348,15 +1348,19 @@
 n null;%0A
+%09%09%7D%0A
 %09%7D%0A%09%0A%7D%0A

Use JaxbXmlWriter/Reader directly to avoid instantiating the SectionManager.