1/** 2 * Loads the contents of a file all at once and passes its contents off to 3 * {@link org.antlr.runtime.ANTLRStringStream}. 4 * Currently this class can only be used in the Rhino JS interpreter. 5 * @class 6 * @extends org.antlr.runtime.ANTLRStringStream 7 * @param {String} fileName path of the file to be loaded 8 * @param {String} [encoding] name of the charset used for decoding 9 */ 10org.antlr.runtime.ANTLRFileStream = function(fileName, encoding) { 11 this.fileName = fileName; 12 13 // @todo need to add support for other JS interpreters that have file i/o 14 // hooks (SpiderMonkey and WSH come to mind). 15 var method; 16 if (org.antlr.env.ua.rhino) { 17 method = "loadFileUsingJava"; 18 } else { 19 throw new Error( 20 "ANTLR File I/O is not supported in this JS implementation." 21 ); 22 } 23 24 var data = this[method](fileName, encoding); 25 org.antlr.runtime.ANTLRFileStream.superclass.constructor.call(this, data); 26}; 27 28org.antlr.lang.extend(org.antlr.runtime.ANTLRFileStream, 29 org.antlr.runtime.ANTLRStringStream, 30/** @lends org.antlr.runtime.ANTLRFileStream.prototype */{ 31 /** 32 * Get the file path from which the input was loaded. 33 * @returns {String} the file path from which the input was loaded 34 */ 35 getSourceName: function() { 36 return this.fileName; 37 }, 38 39 /** 40 * Read the file and return its contents as a JS string. 41 * @private 42 * @param {String} fileName path of the file to be loaded 43 * @param {String} [encoding] name of the charset used for decoding 44 * @returns {String} the contents of the file 45 */ 46 loadFileUsingJava: function(fileName, encoding) { 47 // read the file using Java methods 48 var f = new java.io.File(fileName), 49 size = f.length(), 50 isr, 51 fis = new java.io.FileInputStream(f); 52 if (encoding) { 53 isr = new java.io.InputStreamReader(fis, encoding); 54 } else { 55 isr = new java.io.InputStreamReader(fis); 56 } 57 var data = java.lang.reflect.Array.newInstance(java.lang.Character.TYPE, size); 58 isr.read(data, 0, size); 59 60 // convert java char array to a javascript string 61 return new String(new java.lang.String(data)); 62 } 63}); 64