diff options
Diffstat (limited to 'support/latex/verbfilterScala.java')
-rw-r--r-- | support/latex/verbfilterScala.java | 324 |
1 files changed, 0 insertions, 324 deletions
diff --git a/support/latex/verbfilterScala.java b/support/latex/verbfilterScala.java deleted file mode 100644 index f65c0e7ba0..0000000000 --- a/support/latex/verbfilterScala.java +++ /dev/null @@ -1,324 +0,0 @@ -// $Id$ - -import java.io.*; - -public class verbfilterScala { - - static String[] reserved = { - "abstract", "case", "catch", "class", "def", - "do", "else", "extends", "false", "final", - "finally", "for", "if", "import", "new", - "null", "object", "override", "package", "private", - "protected", "requires", "return", "sealed", "super", "this", "throw", - "trait", "true", "try", "type", "val", - "var", "while", "with", "yield"}; - - static final int TABINC = 8; - - final static String beginVerbatim = "\\begin{verbatim}"; - final static String endVerbatim = "\\end{verbatim}"; - final static String verb = "\\verb"; - - static int lineCount, verbLine; - - static boolean startsWith(byte[] buf, int offset, String s) { - int i = 0; - while (i < s.length() && buf[offset+i] == s.charAt(i)) i++; - return i == s.length(); - } - - static void writeString(OutputStream out, String s) throws IOException { - for (int i = 0; i < s.length(); i++) - out.write(s.charAt(i)); - } - - static int skipBlanks(byte[] buf, int offset) { - while (buf[offset] == ' ') offset++; - return offset; - } - - static int compare(byte[] buf, int i, String key) { - int j = 0; - int l = key.length(); - while (i < buf.length && j < l) { - char bch = (char)buf[i]; - char kch = key.charAt(j); - if (bch < kch) return -1; - else if (bch > kch) return 1; - i++; - j++; - } - if (j < l) - return -1; - else if (i < buf.length && - ('A' <= buf[i] && buf[i] <= 'Z' || - 'a' <= buf[i] && buf[i] <= 'z' || - '0' <= buf[i] && buf[i] <= '9' || - buf[i] == '_')) - return 1; - else - return 0; - } - - static int keyIndex(byte[] buf, int i, String[] keys) { - int lo = 0; - int hi = keys.length - 1; - while (lo <= hi) { - int mid = (hi + lo) / 2; - int diff = compare(buf, i, keys[mid]); - if (diff < 0) hi = mid - 1; - else if (diff > 0) lo = mid + 1; - else return mid; - } - return -1; - } - - static int processLeadingWhitespace(byte[] buf, - int i, - OutputStream out) throws IOException { - int col = 0; - while (true) { - if (buf[i] == ' ') { - writeString(out, "~~"); i++; col++; - } else if (buf[i] == '\t') { - i++; - do { - writeString(out, "~~"); col++; - } while (col % TABINC != 0); - } else { - return i; - } - } - } - - static int processVerbatim(byte[] buf, - int i, - OutputStream out, - String delimiter) throws IOException { - - verbLine = lineCount; - int delimiter0 = delimiter.charAt(0); - int j = skipBlanks(buf, i); - if (buf[j] == '\n') { i = j+1; lineCount++; } - i = processLeadingWhitespace(buf, i, out); - while (true) { - if (buf[i] == delimiter0 && startsWith(buf, i, delimiter)) - return i + delimiter.length(); - switch (buf[i]) { - case ' ': - writeString(out, "~"); - break; - case '\n': - writeString(out, "\n"); - j = i+1; - lineCount++; - if (buf[j] == delimiter0 && startsWith(buf, j, delimiter)) - return j + delimiter.length(); - writeString(out, "\\\\"); - if (buf[i+1] == '\n') { - writeString(out, "[0.5em]"); i++; - lineCount++; - } - i = processLeadingWhitespace(buf, i+1, out)-1; - break; - case '^': - writeString(out, "\\^~$\\!\\!$"); - break; - case '&': - writeString(out, "\\&"); - break; - case '*': - writeString(out, "$*$"); - break; - case '%': - writeString(out, "$\\%$"); - break; - case '_': - writeString(out, "\\_"); - break; - case '~': - writeString(out, "\\~~$\\!\\!$"); - break; - case '{': - writeString(out, "{\\small\\{}"); - break; - case '}': - writeString(out, "{\\small\\}}"); - break; - case '[': - writeString(out, "$[$"); - //if (buf[i+1] == ']') out.write('~'); - break; - case ']': - writeString(out, "$]$"); - break; - case '(': - writeString(out, "$($"); - break; - case ')': - writeString(out, "$)$"); - break; - case ':': - if (i > 0 && Character.isJavaIdentifierPart((char)buf[i-1])) - writeString(out, "\\,"); - writeString(out, "{\\rm :}"); - break; - case '<': - if (buf[i+1] == '=') { - writeString(out, "$\\leq$"); i++; - } else if (buf[i+1] == '-') { - writeString(out, "$\\leftarrow$"); i++; - } else if (buf[i+1] == '<') { - writeString(out, "$<\\!$"); - } else { - writeString(out, "$<$"); - } - break; - case '>': - if (buf[i+1] == '=') { - writeString(out, "$\\geq$"); i++; - } else if (buf[i+1] == '>') { - writeString(out, "$>\\!$"); - } else { - writeString(out, "$>$"); - } - break; - case '=': - if (buf[i+1] == '=') { - writeString(out, "$==$"); i++; - } else if (buf[i+1] == '>') { - writeString(out, "$\\Rightarrow$"); i++; - } else { - out.write('='); - } - break; - case '/': - if (buf[i+1] == '/') { - out.write ('/'); - do { - out.write(buf[i+1]); - i++; - } while (buf[i+1] != '\n' && - (buf[i+1] != delimiter0 || - !startsWith(buf, i+1, delimiter))); - } else { - out.write('/'); - } - break; - case '-': - if (buf[i+1] == '>') { - writeString(out, "$\\rightarrow$"); - i++; - } else { - writeString(out, "$-$"); - } - break; - case '+': - writeString(out, "$+$"); - break; - case '|': - writeString(out, "$\\,|$"); - break; - case '#': - writeString(out, "\\#"); - break; - case '\\': - if (buf[i+1] == '=' || buf[i+1] == '>') { - out.write(buf[i]); - i++; - out.write(buf[i]); - } else if (buf[i+1] == '$') { - writeString(out, "\\$"); - i++; - } else if (buf[i+1] == 'R') { - writeString(out, "\\color{red}"); i++; - } else if (buf[i+1] == 'S') { - writeString(out, "\\color{black}"); i++; - } else if (buf[i+1] == 'B') { - writeString(out, "\\color{blue}"); i++; - } else if (buf[i+1] == 'G') { - writeString(out, "\\color{green}"); i++; - } else { - writeString(out, "$\\backslash$"); - } - break; - case '$': - out.write(buf[i]); - do { - i++; - out.write(buf[i]); - } while (i + 1 < buf.length && buf[i] != '$'); - break; - default: - if (i == 0 || !Character.isJavaIdentifierPart((char)buf[i-1])) { - int k = keyIndex(buf, i, reserved); - if (k >= 0) { - writeString(out, "{\\vem " + reserved[k] + "}"); - i = i + reserved[k].length() - 1; - break; - } - } - out.write(buf[i]); - break; - } - i++; - } - } - - static void process(byte[] buf, OutputStream out) throws IOException { - int i = 0; - while (i < buf.length - 1) { - if (buf[i] == '%') { - do { - out.write(buf[i]); - i++; - } while (buf[i] != '\n' && buf[i] != 0); - } else if (startsWith(buf, i, beginVerbatim)) { - writeString(out, "\\begin{program}"); - i = processVerbatim(buf, i + beginVerbatim.length(), out, - endVerbatim); - writeString(out, "\\end{program}"); - } else if (startsWith(buf, i, verb)) { - writeString(out, "\\prog{"); - i = i + verb.length(); - char[] delimiterArray = {(char)buf[i]}; - String delimiter = new String(delimiterArray); - i = processVerbatim(buf, i + 1, out, delimiter); - writeString(out, "}"); - } else { - if (buf[i] == '\n') lineCount++; - out.write(buf[i]); - i++; - } - } - } - - public static void main(String[] argv) throws IOException { - if (argv.length != 2) { - String classname = new Error().getStackTrace()[0].getClassName(); - System.err.println( - "Usage: " + classname + " <source-file> <destination-file>"); - System.exit(1); - } - InputStream in = new FileInputStream(new File(argv[0])); - byte[] buf = new byte[in.available() + 1]; - in.read(buf, 0, buf.length-1); - in.close(); - OutputStream out = - new BufferedOutputStream( - new FileOutputStream( - new File(argv[1]))); - try { - writeString(out,"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"); - writeString(out,"% DO NOT EDIT. Automatically generated file! %\n"); - writeString(out,"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"); - writeString(out,"\n"); - lineCount = 1; - process(buf, out); - } catch (RuntimeException ex) { - System.err.println ("\n **** error at line " + verbLine); - throw ex; - } - out.close(); - } -} |