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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
010: // and Chalmers University of Technology, Sweden
011: //
012: //The KeY system is protected by the GNU General Public License.
013: //See LICENSE.TXT for details.
014: //
015:
016: package de.uka.ilkd.key.rule.export.html;
017:
018: import java.io.FileNotFoundException;
019: import java.io.FileReader;
020: import java.io.FileWriter;
021: import java.io.IOException;
022: import java.net.URL;
023: import java.util.HashMap;
024:
025: import de.uka.ilkd.key.rule.Taclet;
026: import de.uka.ilkd.key.util.KeYResourceManager;
027:
028: public class HTMLModel extends HTMLContainer {
029: private HashMap key2fragment = new HashMap();
030:
031: private HTMLFragment getFragment(Object key) {
032: return (HTMLFragment) key2fragment.get(key);
033: }
034:
035: private void putFragment(Object key, HTMLFragment fragment) {
036: key2fragment.put(key, fragment);
037: }
038:
039: public String getRelPath(HTMLFile source, HTMLFile target) {
040: return target.getFilename();
041: }
042:
043: public HTMLModel(String rootFolder) {
044: super (rootFolder);
045: }
046:
047: public void writeAllFiles() {
048: super .writeAllFiles();
049:
050: writeStyleSheet();
051: }
052:
053: private void writeStyleSheet() {
054: URL css = KeYResourceManager.getManager().getResourceFile(
055: HTMLFile.class, "templates/style.css");
056: copyFile(css.getFile(), getRootFolder() + "style.css");
057: }
058:
059: private void copyFile(String from, String to) {
060: FileReader reader;
061: FileWriter writer;
062:
063: //System.out.println ( "copying file "+from+" to "+to);
064:
065: try {
066: reader = new FileReader(from);
067: } catch (FileNotFoundException e) {
068: System.err.println(e);
069: return;
070: }
071:
072: try {
073: writer = new FileWriter(to);
074: } catch (IOException e) {
075: System.err.println(e);
076: return;
077: }
078:
079: try {
080: int ch;
081: while ((ch = reader.read()) != -1) {
082: writer.write(ch);
083: //System.out.write(ch);
084: }
085: reader.close();
086: writer.close();
087: } catch (IOException e) {
088: System.err.println(e);
089: return;
090: }
091: }
092:
093: public HTMLLink getFileLink(HTMLFile source, HTMLFile target) {
094: return new HTMLFileLink(source, target);
095: }
096:
097: public HTMLLink getFragmentLink(HTMLFile sourceFile,
098: Object targetKey) {
099: HTMLFragment fragment = getFragment(targetKey);
100:
101: if (fragment == null) {
102: fragment = new HTMLFragment(null, targetKey);
103: putFragment(targetKey, fragment);
104: }
105:
106: return new HTMLFragmentLink(sourceFile, fragment);
107: }
108:
109: public HTMLLink getTacletLink(final HTMLFile source, final Taclet t) {
110: return getFragmentLink(source, t);
111: }
112:
113: public HTMLAnchor getFragmentAnchor(HTMLFile file, Object key) {
114: HTMLFragment fragment = getFragment(key);
115:
116: if (fragment != null) {
117: if (fragment.getFile() == null) {
118: fragment.setFile(file);
119: String id = file.getNextId();
120: file.addFragment(fragment, id);
121: //System.out.println("missing fragment definition: "+file.getFilename()+", "+key);
122: } else {
123: //System.out.println("ignored fragment redefinition: "+file.getFilename()+", "+key);
124: }
125: } else {
126: fragment = new HTMLFragment(file, key);
127: putFragment(key, fragment);
128: String id = file.getNextId();
129: file.addFragment(fragment, id);
130: //System.out.println("fragment definition: "+file.getFilename()+", "+key);
131: }
132:
133: final HTMLFragment f = fragment;
134:
135: return new HTMLAnchor() {
136:
137: public String toString() {
138: return f.getId();
139: }
140: };
141: }
142: }
|