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.File;
014: import java.io.FileInputStream;
015: import java.io.IOException;
016: import java.io.InputStream;
017: import java.net.MalformedURLException;
018: import java.net.URL;
019:
020: import de.uka.ilkd.key.util.KeYResourceManager;
021:
022: public class RuleSource {
023:
024: private URL url = null;
025:
026: private File f = null;
027:
028: private long numberOfChars;
029:
030: private RuleSource(File f) {
031: this .f = f;
032: if (f != null) {
033: numberOfChars = f.length();
034: }
035: }
036:
037: private RuleSource(URL url) {
038: this .url = url;
039: if (f != null) {
040: numberOfChars = f.length();
041: }
042: if (url.getProtocol().equals("file")) {
043: numberOfChars = (new File(url.getFile())).length();
044: } else {
045: try {
046: InputStream input = url.openStream();
047: numberOfChars = 0;
048: int i = input.read();
049: while (i != -1) {
050: numberOfChars++;
051: i = input.read();
052: }
053: } catch (IOException ioex) {
054: System.err.println("IOException in class RuleSource");
055: }
056: }
057: }
058:
059: public static RuleSource initRuleFile(String filename) {
060: URL u = KeYResourceManager.getManager().getResourceFile(
061: RuleSource.class, "rules/" + filename);
062: if (u == null) {
063: // a more specific exception type woul probably be better
064: throw new RuntimeException("Could not find rule file "
065: + filename);
066: }
067: return new RuleSource(u);
068: }
069:
070: public static RuleSource initRuleFile(URL url) {
071: return new RuleSource(url);
072: }
073:
074: public int getNumberOfChars() {
075: return (int) numberOfChars;
076: }
077:
078: public static RuleSource initRuleFile(File file) {
079: return new RuleSource(file);
080: }
081:
082: public File file() {
083: if (f == null) {
084: return new File(url.getFile());
085: } else {
086: return f;
087: }
088: }
089:
090: public String getInclusionString() {
091: return "\\includeFile \"" + file().getAbsolutePath() + "\";\n";
092: }
093:
094: public String toString() {
095: if (url != null) {
096: return url.toString();
097: } else {
098: return f.toString();
099: }
100: }
101:
102: public String getExternalForm() {
103: URL localURL = null;
104: if (f == null) {
105: localURL = url;
106: } else {
107: try {
108: localURL = f.toURL();
109: } catch (MalformedURLException e) {
110: return null;
111: }
112: }
113: return localURL.toExternalForm();
114: }
115:
116: public InputStream getNewStream() {
117: try {
118: if (f == null) {
119: return url.openStream();
120: } else {
121: return new FileInputStream(f);
122: }
123: } catch (IOException ioe) {
124: System.err
125: .println("*******************************************");
126: System.err
127: .println("IO-Error occured while opening rule stream.");
128: System.err.println("URL: " + url);
129: System.err.println(ioe);
130: System.err
131: .println("*******************************************");
132: ioe.printStackTrace();
133: throw new RuntimeException("Error while parsing rules.",
134: ioe);
135: }
136: }
137:
138: public boolean isDirectory() {
139: return file().isDirectory();
140: }
141:
142: public boolean isAvailable() {
143: InputStream is;
144: try {
145: is = getNewStream();
146: is.close();
147: } catch (RuntimeException re) {
148: return false;
149: } catch (IOException e) {
150: return false;
151: }
152: return true;
153: }
154: }
|