mpdl-group: software/eXist/mpdl-modules/src/de/mpg/mpiwg/berlin/mpdl/lt/general/Betacode2UnicodeLex.java annotate

author	Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de>
date	Wed, 24 Nov 2010 17:24:23 +0100
parents
children

rev	line source
0 408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	1 package de.mpg.mpiwg.berlin.mpdl.lt.general;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	2
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	3
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	4 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	5 * This class is a scanner generated by
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	6 * <a href="http://www.jflex.de/">JFlex</a> 1.4.3
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	7 * on 19.11.09 20:01 from the specification file
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	8 * <tt>/Users/jwillenborg/java/existDevMai2009/mpdl/extensions/mpdl-modules/src/de/mpg/mpiwg/berlin/mpdl/lt/general/Betacode2Unicode.lex</tt>
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	9 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	10 public class Betacode2UnicodeLex {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	11
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	12 /** This character denotes the end of file */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	13 public static final int YYEOF = -1;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	14
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	15 /** initial size of the lookahead buffer */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	16 private static final int ZZ_BUFFERSIZE = 16384;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	17
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	18 /** lexical states */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	19 public static final int YYINITIAL = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	20
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	21 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	22 * ZZ_LEXSTATE[l] is the state in the DFA for the lexical state l
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	23 * ZZ_LEXSTATE[l+1] is the state in the DFA for the lexical state l
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	24 * at the beginning of a line
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	25 * l is of the form l = 2*k, k a non negative integer
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	26 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	27 private static final int ZZ_LEXSTATE[] = {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	28 0, 0
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	29 };
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	30
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	31 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	32 * Translates characters to character classes
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	33 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	34 private static final String ZZ_CMAP_PACKED =
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	35 "\12\0\1\0\26\0\1\7\1\0\1\62\2\0\1\50\1\54\1\13"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	36 "\1\12\1\3\1\30\1\0\1\47\1\0\1\15\1\63\1\46\1\54"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	37 "\1\64\5\54\1\65\1\10\1\52\1\1\1\16\1\2\1\32\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	38 "\32\66\1\56\1\14\1\55\1\26\1\27\1\0\1\11\1\33\1\44"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	39 "\1\35\1\17\1\57\1\34\1\20\1\21\1\4\1\40\1\41\1\42"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	40 "\1\43\1\22\1\45\1\37\1\31\1\6\1\51\1\23\1\5\1\24"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	41 "\1\60\1\61\1\36\1\0\1\25\1\53\uff82\0";
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	42
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	43 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	44 * Translates characters to character classes
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	45 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	46 private static final char [] ZZ_CMAP = zzUnpackCMap(ZZ_CMAP_PACKED);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	47
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	48 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	49 * Translates DFA states to action switch labels.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	50 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	51 private static final int [] ZZ_ACTION = zzUnpackAction();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	52
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	53 private static final String ZZ_ACTION_PACKED_0 =
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	54 "\1\0\3\1\1\2\1\3\1\4\1\5\1\6\1\7"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	55 "\1\10\1\11\1\12\1\13\1\14\1\15\1\16\1\17"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	56 "\1\20\1\21\1\22\1\23\1\24\1\25\1\26\1\27"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	57 "\1\30\1\31\1\32\1\33\1\34\1\35\1\36\1\37"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	58 "\1\40\1\41\1\42\1\43\1\1\1\44\1\45\1\46"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	59 "\1\47\1\0\1\50\1\51\1\52\1\53\2\0\1\54"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	60 "\1\55\1\56\1\57\1\60\1\61\1\62\1\63\1\64"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	61 "\1\65\1\66\1\67\1\70\1\71\1\72\1\73\1\74"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	62 "\1\75\1\76\1\77\1\100\1\101\1\102\1\0\1\4"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	63 "\1\0\2\102\1\0\1\103\1\104\1\105\1\106\1\107"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	64 "\1\110\1\111\1\112\1\113\1\114\1\115\1\116\1\117"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	65 "\1\120\1\121\1\122\1\123\1\124\1\125\1\126\1\127"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	66 "\1\130\1\131\1\132\1\133\1\0\1\134\1\135\1\136"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	67 "\1\137\1\140\1\141\1\142\1\143\1\144\1\145\1\146"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	68 "\1\0\1\147\1\150\1\151\1\152\1\153\1\154\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	69 "\1\155\1\156\6\0\1\157\1\160\1\161\1\162\1\163"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	70 "\1\164\3\0\1\165\1\166\1\167\1\170\1\171\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	71 "\1\172\3\0\1\173\1\174\1\175\1\176\1\177\1\200"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	72 "\1\0\1\201\1\202\1\203\1\204\1\205\1\206\1\207"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	73 "\1\210\1\211\1\212\1\213\1\214\1\215\1\216\1\217"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	74 "\1\220\1\221\1\222\1\223\2\0\1\224\1\225\1\226"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	75 "\1\227\1\230\1\231\1\232\1\233\1\234\1\235\1\236"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	76 "\1\237\1\240\1\241\1\242\1\243\1\244\1\245\1\246"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	77 "\1\247\1\250\1\251\1\252\1\253\1\254\1\255\1\256"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	78 "\1\257\1\260\1\261\1\262\1\263\1\264\1\265\1\266"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	79 "\1\267\1\270\1\271\1\272\1\273\1\274\1\275\1\276"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	80 "\1\277\1\300\1\301\1\302\1\303\1\304\1\305\1\306"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	81 "\1\307\1\310\1\311\1\312\1\313\1\314\1\315\1\316"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	82 "\1\317\13\0\1\320\1\321\1\322\1\323\1\324\1\325"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	83 "\1\0\1\326\1\327\1\330\1\331\1\332\1\333\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	84 "\1\334\1\335\1\336\1\337\1\0\1\340\1\341\1\342"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	85 "\1\343\1\344\1\345\1\346\1\347\1\350\1\351\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	86 "\1\352\1\353\1\354\1\355\1\356\1\357\1\360\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	87 "\1\361\1\362\1\363\1\364\1\365\1\0\1\366\1\367"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	88 "\1\370\2\0\1\371\1\372\1\373\1\374\1\375\1\376"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	89 "\1\377\1\u0100\1\u0101\1\u0102\1\u0103\1\u0104\1\u0105\1\u0106"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	90 "\1\u0107\1\u0108\1\u0109\1\u010a\2\0\1\u010b\1\0\1\u010c"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	91 "\4\0\1\u010d\1\u010e\1\u010f\1\u0110\1\u0111\1\u0112\1\u0113"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	92 "\1\u0114\1\u0115\1\u0116\1\u0117\1\u0118\1\u0119\1\u011a\1\u011b"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	93 "\1\u011c\1\u011d\1\u011e\10\0\1\u011f\1\u0120\1\u0121\1\u0122";
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	94
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	95 private static int [] zzUnpackAction() {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	96 int [] result = new int[359];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	97 int offset = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	98 offset = zzUnpackAction(ZZ_ACTION_PACKED_0, offset, result);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	99 return result;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	100 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	101
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	102 private static int zzUnpackAction(String packed, int offset, int [] result) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	103 int i = 0; /* index in packed string */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	104 int j = offset; /* index in unpacked array */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	105 int l = packed.length();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	106 while (i < l) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	107 int count = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	108 int value = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	109 do result[j++] = value; while (--count > 0);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	110 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	111 return j;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	112 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	113
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	114
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	115 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	116 * Translates a state to a row index in the transition table
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	117 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	118 private static final int [] ZZ_ROWMAP = zzUnpackRowMap();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	119
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	120 private static final String ZZ_ROWMAP_PACKED_0 =
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	121 "\0\0\0\67\0\156\0\245\0\67\0\67\0\334\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	122 "\0\67\0\u0113\0\67\0\67\0\67\0\67\0\67\0\u014a"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	123 "\0\u0181\0\u01b8\0\u01ef\0\u0226\0\u025d\0\67\0\67\0\u0294"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	124 "\0\67\0\u02cb\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	125 "\0\67\0\67\0\67\0\67\0\67\0\67\0\u0302\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	126 "\0\67\0\67\0\67\0\u0339\0\67\0\67\0\67\0\u0370"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	127 "\0\u03a7\0\u03de\0\u0415\0\u044c\0\u0483\0\u04ba\0\u04f1\0\u0528"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	128 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	129 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	130 "\0\67\0\u055f\0\67\0\u0596\0\u05cd\0\u0604\0\u0604\0\u063b"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	131 "\0\u0672\0\u06a9\0\u06e0\0\u0717\0\67\0\67\0\67\0\u074e"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	132 "\0\u0785\0\67\0\67\0\u07bc\0\u07f3\0\u082a\0\u0861\0\u0898"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	133 "\0\67\0\u08cf\0\u0906\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	134 "\0\u093d\0\u0974\0\u09ab\0\67\0\67\0\u09e2\0\u0a19\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	135 "\0\67\0\67\0\67\0\67\0\u0a50\0\u0a87\0\u0abe\0\u0af5"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	136 "\0\u0b2c\0\u0b63\0\67\0\u0b9a\0\u0bd1\0\u0c08\0\u0c3f\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	137 "\0\67\0\u0c76\0\u0cad\0\u0ce4\0\u0d1b\0\u0d52\0\u0d89\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	138 "\0\67\0\67\0\67\0\67\0\67\0\u0dc0\0\u0df7\0\u0e2e"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	139 "\0\67\0\67\0\67\0\67\0\67\0\u0e65\0\67\0\u0e9c"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	140 "\0\u0ed3\0\u0f0a\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	141 "\0\u0f41\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	142 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	143 "\0\67\0\67\0\67\0\67\0\u0f78\0\u0faf\0\67\0\u0fe6"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	144 "\0\u101d\0\u1054\0\67\0\u108b\0\u10c2\0\u10f9\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	145 "\0\67\0\67\0\67\0\67\0\67\0\67\0\u1130\0\u1167"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	146 "\0\u119e\0\67\0\u11d5\0\u120c\0\u1243\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	147 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	148 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	149 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\u127a"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	150 "\0\u12b1\0\u12e8\0\67\0\u131f\0\u1356\0\u138d\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	151 "\0\67\0\67\0\u13c4\0\u13fb\0\u1432\0\u1469\0\u14a0\0\u14d7"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	152 "\0\u150e\0\u1545\0\u157c\0\u15b3\0\u15ea\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	153 "\0\67\0\67\0\67\0\u1621\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	154 "\0\67\0\67\0\u1658\0\67\0\67\0\67\0\67\0\u168f"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	155 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	156 "\0\67\0\67\0\u16c6\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	157 "\0\67\0\67\0\u16fd\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	158 "\0\u1734\0\67\0\67\0\67\0\u176b\0\u17a2\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	159 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	160 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	161 "\0\u17d9\0\u1810\0\67\0\u1847\0\67\0\u187e\0\u18b5\0\u18ec"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	162 "\0\u1923\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	163 "\0\67\0\67\0\67\0\67\0\67\0\67\0\67\0\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	164 "\0\67\0\67\0\67\0\u195a\0\u1991\0\u19c8\0\u19ff\0\u1a36"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	165 "\0\u1a6d\0\u1aa4\0\u1adb\0\67\0\67\0\67\0\67";
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	166
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	167 private static int [] zzUnpackRowMap() {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	168 int [] result = new int[359];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	169 int offset = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	170 offset = zzUnpackRowMap(ZZ_ROWMAP_PACKED_0, offset, result);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	171 return result;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	172 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	173
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	174 private static int zzUnpackRowMap(String packed, int offset, int [] result) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	175 int i = 0; /* index in packed string */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	176 int j = offset; /* index in unpacked array */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	177 int l = packed.length();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	178 while (i < l) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	179 int high = packed.charAt(i++) << 16;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	180 result[j++] = high \| packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	181 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	182 return j;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	183 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	184
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	185 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	186 * The transition table of the DFA
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	187 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	188 private static final int [] ZZ_TRANS = zzUnpackTrans();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	189
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	190 private static final String ZZ_TRANS_PACKED_0 =
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	191 "\1\2\1\3\1\2\1\4\1\5\1\6\1\7\1\10"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	192 "\1\11\1\12\1\13\1\14\1\15\1\16\1\17\1\20"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	193 "\1\21\1\22\1\23\1\24\1\25\1\26\1\27\1\30"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	194 "\1\31\1\32\1\33\1\34\1\35\1\36\1\37\1\40"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	195 "\1\41\1\42\1\43\1\44\1\45\1\46\2\2\1\47"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	196 "\1\50\5\2\1\51\1\52\1\53\5\2\67\0\2\54"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	197 "\1\0\64\54\4\0\1\55\1\56\1\57\2\0\1\60"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	198 "\1\61\1\62\3\0\1\63\1\64\1\65\1\66\1\67"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	199 "\1\70\4\0\1\71\1\0\1\72\1\73\1\74\1\75"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	200 "\1\76\1\77\1\100\1\101\1\102\1\103\1\104\3\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	201 "\1\105\5\0\1\106\1\107\1\110\5\0\3\111\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	202 "\2\111\3\0\1\111\10\0\4\111\1\0\1\112\13\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	203 "\1\113\1\114\1\115\1\0\2\111\1\0\1\116\1\117"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	204 "\3\0\1\111\3\0\1\111\12\0\1\120\1\121\1\122"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	205 "\1\123\1\124\6\0\1\125\1\126\1\127\51\0\1\130"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	206 "\1\131\1\132\1\133\63\0\1\134\1\135\1\136\1\137"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	207 "\1\140\6\0\1\141\53\0\1\142\1\143\1\144\1\145"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	208 "\1\146\7\0\1\147\1\150\1\151\50\0\1\152\1\153"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	209 "\1\154\1\155\63\0\1\156\1\157\1\160\1\161\1\162"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	210 "\7\0\1\163\1\164\1\165\50\0\1\166\1\167\1\170"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	211 "\1\171\1\172\6\0\1\173\46\0\1\174\23\0\1\175"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	212 "\2\0\1\176\4\0\1\177\37\0\1\200\1\201\57\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	213 "\1\202\1\203\1\202\2\0\1\202\5\0\6\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	214 "\1\204\1\0\1\202\1\205\4\202\1\206\4\202\3\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	215 "\1\202\5\0\3\202\1\207\3\0\1\202\2\54\1\2"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	216 "\64\54\14\0\1\210\1\211\7\0\1\212\1\213\1\214"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	217 "\50\0\1\215\2\0\1\216\1\217\1\220\1\221\1\222"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	218 "\1\223\1\224\1\0\1\225\1\226\52\0\1\227\2\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	219 "\1\230\1\231\1\232\1\233\1\234\1\235\1\236\1\237"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	220 "\1\240\1\241\3\0\1\242\51\0\1\243\1\244\65\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	221 "\1\245\1\246\7\0\1\247\55\0\1\250\1\251\10\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	222 "\1\252\1\253\53\0\1\254\1\255\65\0\1\256\1\257"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	223 "\10\0\1\260\1\261\53\0\1\262\1\263\7\0\1\264"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	224 "\41\0\3\111\4\0\2\111\3\0\1\111\10\0\4\111"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	225 "\17\0\1\111\1\0\2\111\1\0\1\111\4\0\1\111"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	226 "\3\0\1\111\47\0\1\111\53\0\1\265\4\0\1\266"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	227 "\30\0\5\267\1\0\3\267\1\0\10\267\4\0\17\267"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	228 "\1\0\1\267\2\0\1\267\2\0\3\267\1\0\3\267"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	229 "\15\0\1\270\1\271\1\272\6\0\1\273\55\0\1\274"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	230 "\1\275\1\276\6\0\1\277\66\0\1\300\66\0\1\301"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	231 "\66\0\1\302\55\0\1\303\1\304\65\0\1\305\1\306"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	232 "\65\0\1\307\1\310\1\311\6\0\1\312\55\0\1\313"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	233 "\1\314\1\315\6\0\1\316\66\0\1\317\66\0\1\320"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	234 "\66\0\1\321\55\0\1\322\1\323\1\324\64\0\1\325"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	235 "\1\326\1\327\64\0\1\330\1\331\1\332\64\0\1\333"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	236 "\1\334\65\0\1\335\1\336\65\0\1\337\1\340\1\341"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	237 "\64\0\1\342\1\343\1\344\64\0\1\345\1\346\1\347"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	238 "\64\0\1\350\1\351\1\352\6\0\1\353\55\0\1\354"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	239 "\1\355\1\356\6\0\1\357\66\0\1\360\66\0\1\361"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	240 "\66\0\1\362\60\0\1\363\114\0\1\364\72\0\1\365"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	241 "\62\0\1\366\3\0\1\367\21\0\3\202\2\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	242 "\5\0\6\202\4\0\1\202\1\0\13\202\3\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	243 "\1\2\4\0\3\202\4\0\1\202\4\0\3\202\2\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	244 "\1\202\5\0\1\370\5\202\4\0\1\202\1\0\13\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	245 "\3\0\1\202\1\2\4\0\3\202\4\0\1\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	246 "\3\202\2\0\1\202\5\0\6\202\4\0\1\202\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	247 "\12\202\1\371\3\0\1\202\1\2\4\0\3\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	248 "\1\202\4\0\3\202\2\0\1\202\5\0\6\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	249 "\1\202\1\0\13\202\3\0\1\372\1\2\4\0\3\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	250 "\4\0\1\202\4\0\3\202\2\0\1\202\5\0\6\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	251 "\4\0\1\202\1\0\12\202\1\373\3\0\1\374\1\2"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	252 "\4\0\3\202\4\0\1\202\63\0\1\375\14\0\1\376"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	253 "\5\0\1\377\1\u0100\1\u0101\1\u0102\1\0\1\u0103\1\u0104"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	254 "\52\0\1\u0105\5\0\1\u0106\1\u0107\1\u0108\1\u0109\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	255 "\1\u010a\1\u010b\52\0\1\u010c\6\0\1\u010d\1\u010e\2\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	256 "\1\u010f\1\u0110\52\0\1\u0111\6\0\1\u0112\3\0\1\u0113"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	257 "\53\0\1\u0114\5\0\1\u0115\1\u0116\1\u0117\1\u0118\1\u0119"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	258 "\1\u011a\1\u011b\52\0\1\u011c\5\0\1\u011d\1\u011e\1\u011f"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	259 "\1\u0120\1\u0121\1\u0122\1\u0123\52\0\1\u0124\6\0\1\u0125"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	260 "\1\u0126\1\0\1\u0127\1\u0128\1\u0129\52\0\1\u012a\6\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	261 "\1\u012b\3\0\1\u012c\113\0\1\u012d\66\0\1\u012e\42\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	262 "\1\u012f\66\0\1\u0130\66\0\1\u0131\66\0\1\u0132\66\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	263 "\1\u0133\66\0\1\u0134\66\0\1\u0135\66\0\1\u0136\66\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	264 "\1\u0137\66\0\1\u0138\66\0\1\u0139\66\0\1\u013a\66\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	265 "\1\u013b\66\0\1\u013c\66\0\1\u013d\66\0\1\u013e\66\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	266 "\1\u013f\66\0\1\u0140\72\0\1\u0141\46\0\1\u0142\127\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	267 "\1\u0143\25\0\1\u0144\127\0\1\u0145\20\0\3\202\2\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	268 "\1\202\5\0\6\202\4\0\1\u0146\1\0\13\202\3\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	269 "\1\202\1\2\4\0\3\202\4\0\1\202\4\0\3\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	270 "\2\0\1\u0147\5\0\6\202\4\0\1\202\1\0\13\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	271 "\3\0\1\202\1\2\4\0\3\202\4\0\1\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	272 "\3\202\2\0\1\202\5\0\6\202\4\0\1\202\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	273 "\13\202\3\0\1\202\1\u0143\4\0\3\202\4\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	274 "\4\0\3\202\2\0\1\u0148\5\0\6\202\4\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	275 "\1\0\13\202\3\0\1\202\1\2\4\0\3\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	276 "\1\202\4\0\3\202\2\0\1\202\5\0\6\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	277 "\1\202\1\0\13\202\3\0\1\202\1\u0145\4\0\3\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	278 "\4\0\1\202\64\0\1\u0149\13\0\1\u014a\6\0\1\u014b"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	279 "\3\0\1\u014c\53\0\1\u014d\6\0\1\u014e\3\0\1\u014f"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	280 "\53\0\1\u0150\6\0\1\u0151\3\0\1\u0152\53\0\1\u0153"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	281 "\6\0\1\u0154\3\0\1\u0155\53\0\1\u0156\6\0\1\u0157"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	282 "\3\0\1\u0158\53\0\1\u0159\6\0\1\u015a\3\0\1\u015b"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	283 "\114\0\1\u015c\66\0\1\111\65\0\1\u015d\46\0\1\u015e"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	284 "\66\0\1\u015f\41\0\3\202\2\0\1\202\5\0\6\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	285 "\4\0\1\202\1\0\13\202\3\0\1\u0160\1\2\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	286 "\3\202\4\0\1\202\4\0\3\202\2\0\1\202\5\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	287 "\6\202\4\0\1\u0161\1\0\13\202\3\0\1\202\1\2"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	288 "\4\0\3\202\4\0\1\202\4\0\3\202\2\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	289 "\5\0\6\202\4\0\1\u0162\1\0\13\202\3\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	290 "\1\2\4\0\3\202\4\0\1\202\65\0\1\u0163\54\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	291 "\1\117\65\0\1\u0164\66\0\1\u0165\66\0\1\u0166\20\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	292 "\3\202\2\0\1\202\5\0\6\202\4\0\1\202\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	293 "\13\202\3\0\1\202\1\u0164\4\0\3\202\4\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	294 "\4\0\3\202\2\0\1\202\5\0\6\202\4\0\1\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	295 "\1\0\13\202\3\0\1\202\1\u0165\4\0\3\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	296 "\1\202\4\0\3\202\2\0\1\202\5\0\6\202\4\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	297 "\1\202\1\0\13\202\3\0\1\202\1\u0166\4\0\3\202"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	298 "\4\0\1\202\52\0\1\u0167\14\0";
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	299
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	300 private static int [] zzUnpackTrans() {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	301 int [] result = new int[6930];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	302 int offset = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	303 offset = zzUnpackTrans(ZZ_TRANS_PACKED_0, offset, result);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	304 return result;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	305 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	306
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	307 private static int zzUnpackTrans(String packed, int offset, int [] result) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	308 int i = 0; /* index in packed string */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	309 int j = offset; /* index in unpacked array */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	310 int l = packed.length();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	311 while (i < l) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	312 int count = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	313 int value = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	314 value--;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	315 do result[j++] = value; while (--count > 0);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	316 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	317 return j;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	318 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	319
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	320
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	321 /* error codes */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	322 private static final int ZZ_UNKNOWN_ERROR = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	323 private static final int ZZ_NO_MATCH = 1;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	324 private static final int ZZ_PUSHBACK_2BIG = 2;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	325
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	326 /* error messages for the codes above */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	327 private static final String ZZ_ERROR_MSG[] = {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	328 "Unkown internal scanner error",
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	329 "Error: could not match input",
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	330 "Error: pushback value was too large"
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	331 };
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	332
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	333 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	334 * ZZ_ATTRIBUTE[aState] contains the attributes of state <code>aState</code>
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	335 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	336 private static final int [] ZZ_ATTRIBUTE = zzUnpackAttribute();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	337
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	338 private static final String ZZ_ATTRIBUTE_PACKED_0 =
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	339 "\1\0\1\11\2\1\2\11\1\1\2\11\1\1\5\11"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	340 "\6\1\2\11\1\1\1\11\1\1\14\11\1\1\4\11"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	341 "\1\0\3\11\1\1\2\0\6\1\21\11\1\0\1\11"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	342 "\1\0\2\1\1\0\5\1\3\11\2\1\2\11\5\1"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	343 "\1\11\2\1\5\11\1\0\2\1\2\11\2\1\5\11"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	344 "\1\0\5\1\1\11\4\0\2\11\6\0\6\11\3\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	345 "\5\11\1\0\1\11\3\0\6\11\1\0\23\11\2\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	346 "\1\11\3\1\1\11\3\1\10\11\3\1\1\11\3\1"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	347 "\32\11\3\1\1\11\3\1\4\11\13\0\6\11\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	348 "\6\11\1\0\4\11\1\0\12\11\1\0\7\11\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	349 "\5\11\1\0\3\11\2\0\22\11\2\0\1\11\1\0"+
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	350 "\1\11\4\0\22\11\10\0\4\11";
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	351
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	352 private static int [] zzUnpackAttribute() {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	353 int [] result = new int[359];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	354 int offset = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	355 offset = zzUnpackAttribute(ZZ_ATTRIBUTE_PACKED_0, offset, result);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	356 return result;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	357 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	358
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	359 private static int zzUnpackAttribute(String packed, int offset, int [] result) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	360 int i = 0; /* index in packed string */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	361 int j = offset; /* index in unpacked array */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	362 int l = packed.length();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	363 while (i < l) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	364 int count = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	365 int value = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	366 do result[j++] = value; while (--count > 0);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	367 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	368 return j;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	369 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	370
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	371 /** the input device */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	372 private java.io.Reader zzReader;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	373
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	374 /** the current state of the DFA */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	375 private int zzState;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	376
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	377 /** the current lexical state */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	378 private int zzLexicalState = YYINITIAL;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	379
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	380 /** this buffer contains the current text to be matched and is
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	381 the source of the yytext() string */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	382 private char zzBuffer[] = new char[ZZ_BUFFERSIZE];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	383
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	384 /** the textposition at the last accepting state */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	385 private int zzMarkedPos;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	386
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	387 /** the current text position in the buffer */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	388 private int zzCurrentPos;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	389
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	390 /** startRead marks the beginning of the yytext() string in the buffer */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	391 private int zzStartRead;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	392
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	393 /** endRead marks the last character in the buffer, that has been read
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	394 from input */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	395 private int zzEndRead;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	396
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	397 /** number of newlines encountered up to the start of the matched text */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	398 private int yyline;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	399
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	400 /** the number of characters up to the start of the matched text */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	401 private int yychar;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	402
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	403 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	404 * the number of characters from the last newline up to the start of the
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	405 * matched text
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	406 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	407 private int yycolumn;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	408
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	409 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	410 * zzAtBOL == true <=> the scanner is currently at the beginning of a line
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	411 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	412 private boolean zzAtBOL = true;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	413
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	414 /** zzAtEOF == true <=> the scanner is at the EOF */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	415 private boolean zzAtEOF;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	416
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	417 /** denotes if the user-EOF-code has already been executed */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	418 private boolean zzEOFDone;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	419
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	420 /* user code: */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	421 /*
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	422 * Betacode to Unicode conversion
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	423 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	424
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	425 private String toUnicode(int in) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	426 char c = (char) in;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	427 Character ch = new Character(c);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	428 String retString = ch.toString();
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	429 return retString;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	430 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	431
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	432
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	433
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	434 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	435 * Creates a new scanner
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	436 * There is also a java.io.InputStream version of this constructor.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	437 *
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	438 * @param in the java.io.Reader to read input from.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	439 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	440 public Betacode2UnicodeLex(java.io.Reader in) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	441 this.zzReader = in;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	442 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	443
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	444 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	445 * Creates a new scanner.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	446 * There is also java.io.Reader version of this constructor.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	447 *
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	448 * @param in the java.io.Inputstream to read input from.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	449 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	450 public Betacode2UnicodeLex(java.io.InputStream in) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	451 this(new java.io.InputStreamReader(in));
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	452 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	453
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	454 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	455 * Unpacks the compressed character translation table.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	456 *
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	457 * @param packed the packed character translation table
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	458 * @return the unpacked character translation table
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	459 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	460 private static char [] zzUnpackCMap(String packed) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	461 char [] map = new char[0x10000];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	462 int i = 0; /* index in packed string */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	463 int j = 0; /* index in unpacked array */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	464 while (i < 134) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	465 int count = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	466 char value = packed.charAt(i++);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	467 do map[j++] = value; while (--count > 0);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	468 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	469 return map;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	470 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	471
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	472
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	473 /**
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	474 * Refills the input buffer.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	475 *
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	476 * @return <code>false</code>, iff there was new input.
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	477 *
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	478 * @exception java.io.IOException if any I/O-Error occurs
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	479 */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	480 private boolean zzRefill() throws java.io.IOException {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	481
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	482 /* first: make room (if you can) */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	483 if (zzStartRead > 0) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	484 System.arraycopy(zzBuffer, zzStartRead,
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	485 zzBuffer, 0,
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	486 zzEndRead-zzStartRead);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	487
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	488 /* translate stored positions */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	489 zzEndRead-= zzStartRead;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	490 zzCurrentPos-= zzStartRead;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	491 zzMarkedPos-= zzStartRead;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	492 zzStartRead = 0;
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	493 }
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	494
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	495 /* is the buffer big enough? */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	496 if (zzCurrentPos >= zzBuffer.length) {
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	497 /* if not: blow it up */
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	498 char newBuffer[] = new char[zzCurrentPos*2];
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	499 System.arraycopy(zzBuffer, 0, newBuffer, 0, zzBuffer.length);
408254cf2f1d Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	500 zzBuffer = newBuffer;

0

408254cf2f1d Erstellung