+ private String get_line(InputStream f) throws IOException, FileEndedException, NonHexcharException {
+ int c;
+ StringBuffer line = new StringBuffer();
+
+ do {
+ c = f.read();
+ } while (Character.isWhitespace(c));
+
+ do {
+ line.append((char) c);
+ c = f.read();
+ } while (!Character.isWhitespace(c));
+ return new String(line);
+ }
+