mpdl-group: software/mpdl-services/mpiwg-mpdl-lt/src/de/mpg/mpiwg/berlin/mpdl/lt/text/transcode/Unicode2BetacodeLex.java annotate

author	Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de>
date	Wed, 09 Nov 2011 15:32:05 +0100
parents
children

rev	line source
19 4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	1 /* The following code was generated by JFlex 1.4.3 on 14.12.10 15:03 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	2
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	3 package de.mpg.mpiwg.berlin.mpdl.lt.text.transcode;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	4
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	5
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	6 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	7 * This class is a scanner generated by
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	8 * <a href="http://www.jflex.de/">JFlex</a> 1.4.3
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	9 * on 14.12.10 15:03 from the specification file
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	10 * <tt>/Users/jwillenborg/test/jflex/Unicode2Betacode.lex</tt>
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	11 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	12 public class Unicode2BetacodeLex {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	13
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	14 /** This character denotes the end of file */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	15 public static final int YYEOF = -1;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	16
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	17 /** initial size of the lookahead buffer */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	18 private static final int ZZ_BUFFERSIZE = 16384;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	19
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	20 /** lexical states */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	21 public static final int YYINITIAL = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	22
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	23 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	24 * ZZ_LEXSTATE[l] is the state in the DFA for the lexical state l
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	25 * ZZ_LEXSTATE[l+1] is the state in the DFA for the lexical state l
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	26 * at the beginning of a line
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	27 * l is of the form l = 2*k, k a non negative integer
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	28 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	29 private static final int ZZ_LEXSTATE[] = {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	30 0, 0
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	31 };
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	32
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	33 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	34 * Translates characters to character classes
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	35 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	36 private static final String ZZ_CMAP_PACKED =
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	37 "\12\0\1\0\26\0\1\u0118\1\0\1\u0130\2\0\1\u0113\4\u011c\2\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	38 "\1\u0112\1\11\1\u011c\1\u0131\2\u011c\1\u0132\5\u011c\1\u0133\1\0\1\u0116"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	39 "\1\1\1\u011c\1\2\1\u011b\1\0\5\u0134\1\6\1\u0134\1\4\22\u0134"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	40 "\1\u011d\1\0\1\u011a\1\0\1\u012a\1\0\1\u012f\3\u0135\1\u012c\1\7"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	41 "\1\u0114\1\5\3\u0135\1\u0119\3\u0135\1\u012e\1\u0135\1\u012d\1\u0135\1\u0115"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	42 "\1\3\1\u012b\4\u0135\2\0\1\u0117\71\0\1\12\u0248\0\1\344\1\345"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	43 "\1\351\1\0\1\346\1\0\1\347\1\0\1\350\12\0\1\352\1\353"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	44 "\16\0\1\354\41\0\1\355\113\0\1\357\1\361\1\363\1\365\1\367"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	45 "\1\371\1\373\1\375\1\377\1\u0101\1\u0103\1\u0105\1\u0107\1\u0109\1\u010b"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	46 "\1\u010d\1\u010f\1\0\1\10\1\u011f\1\u0121\1\u0123\1\u0125\1\u0127\1\u0129"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	47 "\7\0\1\356\1\360\1\362\1\364\1\366\1\370\1\372\1\374\1\376"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	48 "\1\u0100\1\u0102\1\u0104\1\u0106\1\u0108\1\u010a\1\u010c\1\u010e\1\u0111\1\u0110"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	49 "\1\u011e\1\u0120\1\u0122\1\u0124\1\u0126\1\u0128\u1b36\0\1\13\1\14\1\15"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	50 "\1\16\1\17\1\20\1\21\1\22\1\23\1\24\1\25\1\26\1\27"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	51 "\1\30\1\31\1\32\1\33\1\34\1\35\1\36\1\37\1\40\2\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	52 "\1\41\1\42\1\43\1\44\1\45\1\46\2\0\1\47\1\50\1\51"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	53 "\1\52\1\53\1\54\1\55\1\56\1\57\1\60\1\61\1\62\1\63"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	54 "\1\64\1\65\1\66\1\67\1\70\1\71\1\72\1\73\1\74\1\75"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	55 "\1\76\1\77\1\100\1\101\1\102\1\103\1\104\1\105\1\106\1\107"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	56 "\1\110\1\111\1\112\1\113\1\114\2\0\1\115\1\116\1\117\1\120"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	57 "\1\121\1\122\2\0\1\123\1\124\1\125\1\126\1\127\1\130\1\131"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	58 "\1\132\1\0\1\133\1\0\1\134\1\0\1\135\1\0\1\136\1\137"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	59 "\1\140\1\141\1\142\1\143\1\144\1\145\1\146\1\147\1\150\1\151"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	60 "\1\152\1\153\1\154\1\155\1\156\1\157\1\160\1\161\1\162\1\163"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	61 "\1\164\1\165\1\166\1\167\1\170\1\171\1\172\1\173\1\174\2\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	62 "\1\175\1\176\1\177\1\200\1\201\1\202\1\203\1\204\1\205\1\206"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	63 "\1\207\1\210\1\211\1\212\1\213\1\214\1\215\1\216\1\217\1\220"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	64 "\1\221\1\222\1\223\1\224\1\225\1\226\1\227\1\230\1\231\1\232"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	65 "\1\233\1\234\1\235\1\236\1\237\1\240\1\241\1\242\1\243\1\244"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	66 "\1\245\1\246\1\247\1\250\1\251\1\252\1\253\1\254\1\255\1\256"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	67 "\1\257\1\260\1\261\1\0\1\262\1\263\1\264\1\265\1\266\1\267"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	68 "\1\270\5\0\1\271\1\272\1\273\1\0\1\274\1\275\1\276\1\277"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	69 "\1\300\1\301\1\302\3\0\1\303\1\304\1\305\1\306\2\0\1\307"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	70 "\1\310\1\311\1\312\1\313\1\314\4\0\1\315\1\316\1\317\1\320"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	71 "\1\321\1\322\1\323\1\324\1\325\1\326\1\327\1\330\1\331\5\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	72 "\1\332\1\333\1\334\1\0\1\340\1\341\1\342\1\343\1\335\1\336"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	73 "\1\337\ue003\0";
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	74
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	75 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	76 * Translates characters to character classes
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	77 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	78 private static final char [] ZZ_CMAP = zzUnpackCMap(ZZ_CMAP_PACKED);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	79
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	80 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	81 * Translates DFA states to action switch labels.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	82 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	83 private static final int [] ZZ_ACTION = zzUnpackAction();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	84
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	85 private static final String ZZ_ACTION_PACKED_0 =
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	86 "\1\0\2\1\1\2\1\3\1\4\1\5\1\6\1\7"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	87 "\1\10\1\11\1\12\1\13\1\14\1\15\1\16\1\17"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	88 "\1\20\1\21\1\22\1\23\1\24\1\25\1\26\1\27"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	89 "\1\30\1\31\1\32\1\33\1\34\1\35\1\36\1\37"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	90 "\1\40\1\41\1\42\1\43\1\44\1\45\1\46\1\47"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	91 "\1\50\1\51\1\52\1\53\1\54\1\55\1\56\1\57"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	92 "\1\60\1\61\1\62\1\63\1\64\1\65\1\66\1\67"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	93 "\1\70\1\71\1\72\1\73\1\74\1\75\1\76\1\77"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	94 "\1\100\1\101\1\102\1\103\1\104\1\105\1\106\1\107"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	95 "\1\110\1\111\1\112\1\113\1\114\1\115\1\116\1\117"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	96 "\1\120\1\121\1\122\1\123\1\124\1\125\1\126\1\127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	97 "\1\130\1\131\1\132\1\133\1\134\1\135\1\136\1\137"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	98 "\1\140\1\141\1\142\1\143\1\144\1\145\1\146\1\147"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	99 "\1\150\1\151\1\152\1\153\1\154\1\155\1\156\1\157"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	100 "\1\160\1\161\1\162\1\163\1\164\1\165\1\166\1\167"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	101 "\1\170\1\171\1\172\1\173\1\174\1\175\1\176\1\177"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	102 "\1\200\1\201\1\202\1\203\1\204\1\205\1\206\1\207"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	103 "\1\210\1\211\1\212\1\213\1\214\1\215\1\216\1\217"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	104 "\1\220\1\221\1\222\1\223\1\224\1\225\1\226\1\227"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	105 "\1\230\1\231\1\232\1\233\1\234\1\235\1\236\1\237"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	106 "\1\240\1\241\1\242\1\243\1\244\1\245\1\246\1\247"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	107 "\1\250\1\251\1\252\1\253\1\254\1\255\1\256\1\257"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	108 "\1\260\1\261\1\262\1\263\1\264\1\265\1\266\1\267"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	109 "\1\270\1\271\1\272\1\273\1\274\1\275\1\276\1\277"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	110 "\1\300\1\301\1\302\1\303\1\304\1\305\1\306\1\307"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	111 "\1\310\1\311\1\312\1\313\1\314\1\315\1\316\1\317"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	112 "\1\320\1\321\1\322\1\323\1\324\1\325\1\326\1\327"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	113 "\1\330\1\331\1\332\1\333\1\334\1\335\1\336\1\337"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	114 "\1\340\1\341\1\342\1\343\1\344\1\345\1\346\1\347"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	115 "\1\350\1\351\1\352\1\353\1\354\1\355\1\356\1\357"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	116 "\1\360\1\361\1\362\1\363\1\364\1\365\1\366\1\367"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	117 "\1\370\1\371\1\372\1\373\1\374\1\375\1\376\1\377"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	118 "\1\u0100\1\u0101\1\u0102\1\u0103\1\u0104\1\u0105\1\u0106\1\u0107"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	119 "\1\u0108\1\u0109\1\u010a\1\u010b\1\u010c\1\u010d\1\u010e\2\1"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	120 "\1\u010f\1\u0110\1\u0111\1\u0112\1\u0113\1\u0114\1\u0115\1\u0116"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	121 "\1\u0117\1\u0118\1\u0119\1\u011a\1\1\3\0\1\u011b\1\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	122 "\1\u011b\33\0\1\u011c\1\u011d\17\0\1\u011e";
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	123
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	124 private static int [] zzUnpackAction() {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	125 int [] result = new int[338];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	126 int offset = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	127 offset = zzUnpackAction(ZZ_ACTION_PACKED_0, offset, result);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	128 return result;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	129 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	130
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	131 private static int zzUnpackAction(String packed, int offset, int [] result) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	132 int i = 0; /* index in packed string */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	133 int j = offset; /* index in unpacked array */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	134 int l = packed.length();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	135 while (i < l) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	136 int count = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	137 int value = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	138 do result[j++] = value; while (--count > 0);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	139 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	140 return j;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	141 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	142
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	143
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	144 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	145 * Translates a state to a row index in the transition table
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	146 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	147 private static final int [] ZZ_ROWMAP = zzUnpackRowMap();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	148
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	149 private static final String ZZ_ROWMAP_PACKED_0 =
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	150 "\0\0\0\u0136\0\u026c\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	151 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	152 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	153 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	154 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	155 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	156 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	157 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	158 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	159 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	160 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	161 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	162 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	163 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	164 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	165 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	166 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	167 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	168 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	169 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	170 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	171 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	172 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	173 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	174 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	175 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	176 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	177 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	178 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	179 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	180 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	181 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	182 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	183 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u03a2"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	184 "\0\u04d8\0\u060e\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	185 "\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0136\0\u0744\0\u087a"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	186 "\0\u09b0\0\u0ae6\0\u0136\0\u0c1c\0\u0d52\0\u0e88\0\u0fbe\0\u10f4"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	187 "\0\u122a\0\u1360\0\u1496\0\u15cc\0\u1702\0\u1838\0\u196e\0\u1aa4"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	188 "\0\u1bda\0\u1d10\0\u1e46\0\u1f7c\0\u20b2\0\u21e8\0\u231e\0\u2454"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	189 "\0\u258a\0\u26c0\0\u27f6\0\u292c\0\u2a62\0\u2b98\0\u2cce\0\u2e04"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	190 "\0\u0136\0\u0136\0\u2f3a\0\u3070\0\u31a6\0\u32dc\0\u3412\0\u3548"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	191 "\0\u367e\0\u37b4\0\u38ea\0\u3a20\0\u3b56\0\u3c8c\0\u3dc2\0\u3ef8"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	192 "\0\u402e\0\u0136";
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	193
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	194 private static int [] zzUnpackRowMap() {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	195 int [] result = new int[338];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	196 int offset = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	197 offset = zzUnpackRowMap(ZZ_ROWMAP_PACKED_0, offset, result);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	198 return result;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	199 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	200
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	201 private static int zzUnpackRowMap(String packed, int offset, int [] result) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	202 int i = 0; /* index in packed string */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	203 int j = offset; /* index in unpacked array */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	204 int l = packed.length();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	205 while (i < l) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	206 int high = packed.charAt(i++) << 16;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	207 result[j++] = high \| packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	208 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	209 return j;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	210 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	211
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	212 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	213 * The transition table of the DFA
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	214 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	215 private static final int [] ZZ_TRANS = zzUnpackTrans();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	216
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	217 private static final String ZZ_TRANS_PACKED_0 =
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	218 "\1\2\1\3\2\2\1\4\1\5\1\6\1\7\1\10"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	219 "\1\11\1\12\1\13\1\14\1\15\1\16\1\17\1\20"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	220 "\1\21\1\22\1\23\1\24\1\25\1\26\1\27\1\30"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	221 "\1\31\1\32\1\33\1\34\1\35\1\36\1\37\1\40"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	222 "\1\41\1\42\1\43\1\44\1\45\1\46\1\47\1\50"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	223 "\1\51\1\52\1\53\1\54\1\55\1\56\1\57\1\60"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	224 "\1\61\1\62\1\63\1\64\1\65\1\66\1\67\1\70"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	225 "\1\71\1\72\1\73\1\74\1\75\1\76\1\77\1\100"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	226 "\1\101\1\102\1\103\1\104\1\105\1\106\1\107\1\110"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	227 "\1\111\1\112\1\113\1\114\1\115\1\116\1\117\1\120"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	228 "\1\121\1\122\1\123\1\124\1\125\1\126\1\127\1\130"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	229 "\1\131\1\132\1\133\1\134\1\135\1\136\1\137\1\140"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	230 "\1\141\1\142\1\143\1\144\1\145\1\146\1\147\1\150"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	231 "\1\151\1\152\1\153\1\154\1\155\1\156\1\157\1\160"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	232 "\1\161\1\162\1\163\1\164\1\165\1\166\1\167\1\170"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	233 "\1\171\1\172\1\173\1\174\1\175\1\176\1\177\1\200"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	234 "\1\201\1\202\1\203\1\204\1\205\1\206\1\207\1\210"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	235 "\1\211\1\212\1\213\1\214\1\215\1\216\1\217\1\220"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	236 "\1\221\1\222\1\223\1\224\1\225\1\226\1\227\1\230"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	237 "\1\231\1\232\1\233\1\234\1\235\1\236\1\237\1\240"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	238 "\1\241\1\242\1\243\1\244\1\245\1\246\1\247\1\250"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	239 "\1\251\1\252\1\253\1\254\1\255\1\256\1\257\1\260"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	240 "\1\261\1\262\1\263\1\264\1\265\1\266\1\267\1\270"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	241 "\1\271\1\272\1\273\1\274\1\275\1\276\1\277\1\300"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	242 "\1\301\1\302\1\303\1\304\1\305\1\306\1\307\1\310"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	243 "\1\311\1\312\1\313\1\314\1\315\1\316\1\317\1\320"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	244 "\1\321\1\322\1\323\1\324\1\325\1\326\1\327\1\330"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	245 "\1\331\1\332\1\333\1\334\1\335\1\336\1\337\1\340"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	246 "\1\341\1\342\1\343\1\344\1\345\1\346\1\347\1\350"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	247 "\1\351\1\352\1\353\1\354\1\355\1\356\1\357\1\360"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	248 "\1\361\1\362\1\363\1\364\1\365\1\366\1\367\1\370"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	249 "\1\371\1\372\1\373\1\374\1\375\1\376\1\377\1\u0100"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	250 "\1\u0101\1\u0102\1\u0103\1\u0104\1\u0105\1\u0106\1\u0107\1\u0108"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	251 "\1\u0109\1\u010a\1\u010b\1\u010c\1\u010d\1\u010e\1\u010f\1\u0110"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	252 "\1\u0111\1\2\1\u0112\12\2\1\u0113\1\u0114\1\u0115\1\u0116"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	253 "\1\u0117\1\u0118\1\u0119\1\u011a\1\u011b\1\u011c\1\u011d\1\u011e"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	254 "\1\u011f\13\2\u0136\0\2\u0120\1\0\u0133\u0120\u0113\0\1\u0121"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	255 "\6\0\1\u0122\2\0\1\u0122\30\0\3\u0123\1\0\1\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	256 "\1\0\1\u0123\1\0\u010a\u0123\1\u0124\1\u0125\2\0\3\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	257 "\1\0\1\u0123\1\u0126\2\0\15\u0123\5\0\1\u0123\3\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	258 "\1\u0123\4\0\5\u0127\u010c\0\1\u0128\1\u0127\3\0\1\u0129"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	259 "\21\0\1\u012a\1\u0127\1\u012b\2\u0127\1\u012c\3\0\2\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	260 "\u0114\0\1\u012d\4\0\1\u012e\21\0\1\u012f\1\0\1\u0130"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	261 "\13\0\1\u0131\u0246\0\1\u0132\44\0\1\u0123\1\0\1\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	262 "\1\0\1\u0123\u010a\0\1\u0123\1\0\2\u0123\2\0\2\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	263 "\1\0\2\u0123\16\0\5\u0123\1\0\3\u0123\1\0\1\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	264 "\u0112\0\1\u0123\u013c\0\1\u0133\34\0\3\u0123\1\0\1\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	265 "\1\0\1\u0123\1\0\u010a\u0123\1\0\1\u0123\2\0\3\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	266 "\1\0\1\u0123\3\0\15\u0123\5\0\1\u0123\3\0\1\u0123"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	267 "\4\0\5\u0127\u010c\0\2\u0127\1\2\2\0\1\u0127\21\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	268 "\5\u0127\4\0\2\u0127\3\0\5\u0127\u010c\0\1\u0127\1\u0134"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	269 "\1\2\2\0\1\u0127\21\0\5\u0127\4\0\2\u0127\3\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	270 "\5\u0127\u010c\0\1\u0127\1\u0135\1\2\2\0\1\u0127\21\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	271 "\3\u0127\1\u0136\1\u0127\4\0\2\u0127\3\0\5\u0127\u010c\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	272 "\2\u0127\1\2\2\0\1\u0127\21\0\1\u0127\1\u0137\3\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	273 "\4\0\2\u0127\3\0\5\u0127\u010c\0\2\u0127\1\2\2\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	274 "\1\u0127\21\0\3\u0127\1\u0138\1\u0127\4\0\2\u0127\u0131\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	275 "\1\u0139\u0119\0\1\u013a\u0135\0\1\u013b\30\0\1\u013c\u0133\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	276 "\1\u013d\u0137\0\1\u013e\11\0\1\2\1\u0131\u0247\0\1\u013f"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	277 "\u0135\0\1\u0140\43\0\5\u0127\u010c\0\2\u0127\1\u0141\2\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	278 "\1\u0127\21\0\5\u0127\4\0\2\u0127\3\0\5\u0127\u010c\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	279 "\2\u0127\1\u0142\2\0\1\u0127\21\0\5\u0127\4\0\2\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	280 "\3\0\5\u0127\u010c\0\2\u0127\1\2\2\0\1\u0127\21\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	281 "\4\u0127\1\u0143\4\0\2\u0127\3\0\5\u0127\u010c\0\2\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	282 "\1\2\2\0\1\u0127\21\0\2\u0127\1\u0144\2\u0127\4\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	283 "\2\u0127\3\0\5\u0127\u010c\0\2\u0127\1\2\2\0\1\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	284 "\21\0\4\u0127\1\u0145\4\0\2\u0127\u0132\0\1\u0146\u0119\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	285 "\1\u0141\u0135\0\1\u0142\u014e\0\1\u0147\u0133\0\1\u0148\u0137\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	286 "\1\u0149\u011c\0\1\u014a\u0135\0\1\u0123\42\0\5\u0127\u010c\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	287 "\2\u0127\1\2\2\0\1\u0127\21\0\2\u0127\1\u014b\2\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	288 "\4\0\2\u0127\3\0\5\u0127\u010c\0\1\u0127\1\u014c\1\2"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	289 "\2\0\1\u0127\21\0\5\u0127\4\0\2\u0127\3\0\5\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	290 "\u010c\0\2\u0127\1\2\2\0\1\u0127\21\0\2\u0127\1\u014d"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	291 "\2\u0127\4\0\2\u0127\u0133\0\1\u014e\u012f\0\1\u014f\u011d\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	292 "\1\u0150\u014d\0\1\u0151\u011f\0\1\u0122\41\0\5\u0127\u010c\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	293 "\2\u0127\1\353\2\0\1\u0127\21\0\5\u0127\4\0\2\u0127"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	294 "\3\0\5\u0127\u010c\0\2\u0127\1\355\2\0\1\u0127\21\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	295 "\5\u0127\4\0\2\u0127\3\0\5\u0127\u010c\0\2\u0127\1\352"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	296 "\2\0\1\u0127\21\0\5\u0127\4\0\2\u0127\u0116\0\1\u0152"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	297 "\u0135\0\1\353\u0135\0\1\355\u0135\0\1\352\37\0";
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	298
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	299 private static int [] zzUnpackTrans() {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	300 int [] result = new int[16740];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	301 int offset = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	302 offset = zzUnpackTrans(ZZ_TRANS_PACKED_0, offset, result);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	303 return result;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	304 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	305
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	306 private static int zzUnpackTrans(String packed, int offset, int [] result) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	307 int i = 0; /* index in packed string */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	308 int j = offset; /* index in unpacked array */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	309 int l = packed.length();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	310 while (i < l) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	311 int count = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	312 int value = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	313 value--;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	314 do result[j++] = value; while (--count > 0);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	315 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	316 return j;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	317 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	318
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	319
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	320 /* error codes */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	321 private static final int ZZ_UNKNOWN_ERROR = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	322 private static final int ZZ_NO_MATCH = 1;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	323 private static final int ZZ_PUSHBACK_2BIG = 2;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	324
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	325 /* error messages for the codes above */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	326 private static final String ZZ_ERROR_MSG[] = {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	327 "Unkown internal scanner error",
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	328 "Error: could not match input",
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	329 "Error: pushback value was too large"
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	330 };
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	331
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	332 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	333 * ZZ_ATTRIBUTE[aState] contains the attributes of state <code>aState</code>
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	334 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	335 private static final int [] ZZ_ATTRIBUTE = zzUnpackAttribute();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	336
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	337 private static final String ZZ_ATTRIBUTE_PACKED_0 =
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	338 "\1\0\1\11\1\1\u010c\11\3\1\14\11\1\1\3\0"+
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	339 "\1\11\1\0\1\1\33\0\2\11\17\0\1\11";
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	340
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	341 private static int [] zzUnpackAttribute() {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	342 int [] result = new int[338];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	343 int offset = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	344 offset = zzUnpackAttribute(ZZ_ATTRIBUTE_PACKED_0, offset, result);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	345 return result;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	346 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	347
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	348 private static int zzUnpackAttribute(String packed, int offset, int [] result) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	349 int i = 0; /* index in packed string */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	350 int j = offset; /* index in unpacked array */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	351 int l = packed.length();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	352 while (i < l) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	353 int count = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	354 int value = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	355 do result[j++] = value; while (--count > 0);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	356 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	357 return j;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	358 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	359
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	360 /** the input device */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	361 private java.io.Reader zzReader;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	362
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	363 /** the current state of the DFA */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	364 private int zzState;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	365
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	366 /** the current lexical state */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	367 private int zzLexicalState = YYINITIAL;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	368
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	369 /** this buffer contains the current text to be matched and is
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	370 the source of the yytext() string */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	371 private char zzBuffer[] = new char[ZZ_BUFFERSIZE];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	372
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	373 /** the textposition at the last accepting state */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	374 private int zzMarkedPos;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	375
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	376 /** the current text position in the buffer */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	377 private int zzCurrentPos;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	378
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	379 /** startRead marks the beginning of the yytext() string in the buffer */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	380 private int zzStartRead;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	381
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	382 /** endRead marks the last character in the buffer, that has been read
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	383 from input */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	384 private int zzEndRead;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	385
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	386 /** number of newlines encountered up to the start of the matched text */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	387 private int yyline;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	388
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	389 /** the number of characters up to the start of the matched text */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	390 private int yychar;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	391
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	392 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	393 * the number of characters from the last newline up to the start of the
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	394 * matched text
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	395 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	396 private int yycolumn;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	397
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	398 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	399 * zzAtBOL == true <=> the scanner is currently at the beginning of a line
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	400 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	401 private boolean zzAtBOL = true;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	402
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	403 /** zzAtEOF == true <=> the scanner is at the EOF */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	404 private boolean zzAtEOF;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	405
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	406 /** denotes if the user-EOF-code has already been executed */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	407 private boolean zzEOFDone;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	408
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	409
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	410 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	411 * Creates a new scanner
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	412 * There is also a java.io.InputStream version of this constructor.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	413 *
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	414 * @param in the java.io.Reader to read input from.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	415 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	416 public Unicode2BetacodeLex(java.io.Reader in) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	417 this.zzReader = in;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	418 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	419
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	420 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	421 * Creates a new scanner.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	422 * There is also java.io.Reader version of this constructor.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	423 *
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	424 * @param in the java.io.Inputstream to read input from.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	425 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	426 public Unicode2BetacodeLex(java.io.InputStream in) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	427 this(new java.io.InputStreamReader(in));
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	428 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	429
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	430 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	431 * Unpacks the compressed character translation table.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	432 *
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	433 * @param packed the packed character translation table
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	434 * @return the unpacked character translation table
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	435 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	436 private static char [] zzUnpackCMap(String packed) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	437 char [] map = new char[0x10000];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	438 int i = 0; /* index in packed string */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	439 int j = 0; /* index in unpacked array */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	440 while (i < 724) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	441 int count = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	442 char value = packed.charAt(i++);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	443 do map[j++] = value; while (--count > 0);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	444 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	445 return map;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	446 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	447
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	448
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	449 /**
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	450 * Refills the input buffer.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	451 *
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	452 * @return <code>false</code>, iff there was new input.
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	453 *
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	454 * @exception java.io.IOException if any I/O-Error occurs
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	455 */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	456 private boolean zzRefill() throws java.io.IOException {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	457
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	458 /* first: make room (if you can) */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	459 if (zzStartRead > 0) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	460 System.arraycopy(zzBuffer, zzStartRead,
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	461 zzBuffer, 0,
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	462 zzEndRead-zzStartRead);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	463
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	464 /* translate stored positions */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	465 zzEndRead-= zzStartRead;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	466 zzCurrentPos-= zzStartRead;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	467 zzMarkedPos-= zzStartRead;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	468 zzStartRead = 0;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	469 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	470
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	471 /* is the buffer big enough? */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	472 if (zzCurrentPos >= zzBuffer.length) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	473 /* if not: blow it up */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	474 char newBuffer[] = new char[zzCurrentPos*2];
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	475 System.arraycopy(zzBuffer, 0, newBuffer, 0, zzBuffer.length);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	476 zzBuffer = newBuffer;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	477 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	478
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	479 /* finally: fill the buffer with new input */
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	480 int numRead = zzReader.read(zzBuffer, zzEndRead,
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	481 zzBuffer.length-zzEndRead);
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	482
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	483 if (numRead > 0) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	484 zzEndRead+= numRead;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	485 return false;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	486 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	487 // unlikely but not impossible: read 0 characters, but not at end of stream
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	488 if (numRead == 0) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	489 int c = zzReader.read();
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	490 if (c == -1) {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	491 return true;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	492 } else {
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	493 zzBuffer[zzEndRead++] = (char) c;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	494 return false;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	495 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	496 }
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	497
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	498 // numRead < 0
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	499 return true;
4a3641ae14d2 Erstellung Josef Willenborg <jwillenborg@mpiwg-berlin.mpg.de> parents: diff changeset	500 }

19

4a3641ae14d2 Erstellung