01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09:
10: package de.uka.ilkd.key.proof.reuse;
11:
12: import java.io.*;
13:
14: import org.apache.log4j.Logger;
15:
16: import de.uka.ilkd.key.gui.KeYMediator;
17: import de.uka.ilkd.key.parser.diffparser.*;
18: import de.uka.ilkd.key.proof.IteratorOfNode;
19: import de.uka.ilkd.key.proof.Node;
20: import de.uka.ilkd.key.proof.Proof;
21:
22: public class ReuseFrontend {
23:
24: private KeYMediator mediator;
25: LineNumberReader r;
26:
27: public ReuseFrontend(KeYMediator medi) {
28: this .mediator = medi;
29: }
30:
31: public String markup(Proof source, File diffFile) {
32: try {
33: return markup(source, new LineNumberReader(new FileReader(
34: diffFile)));
35: } catch (IOException ioe) {
36: return ioe.toString();
37: }
38: }
39:
40: public String markup(Proof source, String s) {
41: return markup(source, new LineNumberReader(new StringReader(s)));
42: }
43:
44: public String markup(Proof source, LineNumberReader r) {
45: try {
46: DiffParserTokenManager lexer = new DiffParserTokenManager(
47: new SimpleCharStream(r),
48: DiffParserConstants.LINE_BEGIN);
49: DiffParser p = new DiffParser(lexer);
50: p.UniDiff();
51: DiffParser.MarkerHint[] hints;
52: hints = p.getMarkers();
53: for (int i = 0; i < hints.length; i++) {
54: Logger.getLogger("key.proof.mgt").debug(
55: "Markup hint: " + hints[i].file + ":"
56: + hints[i].line);
57: recMark(source.root(), hints[i]);
58: }
59: markRoot(source);
60:
61: return null;
62: } catch (ParseException e) {
63: return e.toString();
64: } catch (TokenMgrError er) {
65: return er.toString();
66: }
67: }
68:
69: public void markRoot(Proof source) {
70: mediator.markPersistent(source.root());
71: }
72:
73: private void recMark(Node n, DiffParser.MarkerHint hint) {
74: if (("/" + hint.file).equals(n.getNodeInfo()
75: .getExecStatementParentClass())) {
76: int line = n.getNodeInfo().getExecStatementPosition()
77: .getLine();
78: if (line >= hint.line) {
79: mediator.markPersistent(n);
80: return;
81: }
82: }
83: IteratorOfNode ch = n.childrenIterator();
84: while (ch.hasNext())
85: recMark(ch.next(), hint);
86: }
87:
88: }
|