001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof;
012:
013: import java.io.FileInputStream;
014: import java.io.FileOutputStream;
015: import java.io.IOException;
016: import java.io.PrintStream;
017:
018: import de.uka.ilkd.key.gui.Main;
019: import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent;
020: import de.uka.ilkd.key.pp.LogicPrinter;
021: import de.uka.ilkd.key.pp.NotationInfo;
022: import de.uka.ilkd.key.pp.ProgramPrinter;
023:
024: public class ProofSaverLatex extends ProofSaver {
025:
026: public ProofSaverLatex(Main main, String filename) {
027: super (main, filename);
028: }
029:
030: public String save() {
031: String errorMsg = null;
032: FileOutputStream fos = null;
033: PrintStream ps = null;
034: try {
035: fos = new FileOutputStream(filename);
036: ps = new PrintStream(fos);
037: StringBuffer tree = new StringBuffer();
038: Node root = proof.root();
039:
040: ps.println(texHeader());
041: ps
042: .println("\\pstree[treemode=R,treealign=down,treefit=loose,");
043: ps
044: .println(" treesep=0.3,levelsep=1,nodesep=0.1]{\\Tn}");
045: ps.println("{\n" + TRNode(root));
046: ps.print(collectProof(root.childrenIterator(), root
047: .childrenCount(), "", tree));
048:
049: ps.println("}");
050: ps.println("\\end{document}");
051:
052: } catch (IOException ioe) {
053: errorMsg = "Could not save \n" + filename + ".\n";
054: errorMsg += ioe.toString();
055: } catch (NullPointerException e) {
056: errorMsg = "Could not save \n" + filename + "\n";
057: errorMsg += "No proof present?";
058: e.printStackTrace();
059: } finally {
060: try {
061: if (fos != null)
062: fos.close();
063: } catch (IOException ioe) {
064: mediator.notify(new GeneralFailureEvent("IO Error: "
065: + ioe));
066: }
067: }
068: return errorMsg; // null if success
069: }
070:
071: String nodeSeqToString(Node node) {
072: LogicPrinter logicPrinter = new LogicPrinter(
073: new ProgramPrinter(null),
074: NotationInfo.createInstance(), node.proof()
075: .getServices(), true);
076: logicPrinter.printSequent(node.sequent());
077: StringBuffer buf = logicPrinter.result();
078: for (int i = 0; i < buf.length(); i++) {
079: char c = buf.charAt(i);
080: if (c == '{' || c == '}' || c == '&' || c == '%') {
081: buf.insert(i, '\\');
082: i++;
083: }
084: }
085: return buf.toString().replace('\n', ' ');
086: }
087:
088: private String TRNode(Node node) {
089: return "\\TR[href=-1]{\\lstinline$" + nodeSeqToString(node)
090: + "$}\n";
091: }
092:
093: private StringBuffer collectProof(IteratorOfNode it, int siblings,
094: String prefix, StringBuffer tree) {
095:
096: Node node;
097:
098: if (siblings == 0)
099: return tree;
100:
101: if (siblings == 1) {
102: node = it.next();
103: tree.append(prefix + TRNode(node));
104: collectProof(node.childrenIterator(), node.childrenCount(),
105: prefix, tree);
106: } else {
107: int i = 0;
108: while (it.hasNext()) {
109: i++;
110: node = it.next();
111: tree
112: .append(prefix + "\\pstree{\\TR{Case " + i
113: + "}}\n");
114: tree.append(prefix + " {\\Tn ");
115: tree.append(prefix + " " + TRNode(node));
116: collectProof(node.childrenIterator(), node
117: .childrenCount(), prefix + " ", tree);
118: tree.append(prefix + " }\n");
119: }
120: }
121: return tree;
122: }
123:
124: private StringBuffer texHeader() {
125: java.net.URL header = de.uka.ilkd.key.util.KeYResourceManager
126: .getManager().getResourceFile(ProofSaverLatex.class,
127: "proofheader.tex");
128: StringBuffer sb = new StringBuffer(8000);
129: sb.append("% " + proof.name() + "\n");
130: try {
131: FileInputStream inp = new FileInputStream(header.getFile());
132: while (inp.available() > 0)
133: sb.append((char) inp.read());
134: } catch (IOException ioe) {
135: sb = new StringBuffer("% Could not find proofheader.tex\n");
136: }
137: return sb;
138: }
139: }
|