equal
deleted
inserted
replaced
727 System.out.println("processComment(" + pos |
727 System.out.println("processComment(" + pos |
728 + "," + endPos + "," + style + ")=|" |
728 + "," + endPos + "," + style + ")=|" |
729 + new String(reader.getRawCharacters(pos, endPos)) |
729 + new String(reader.getRawCharacters(pos, endPos)) |
730 + "|"); |
730 + "|"); |
731 char[] buf = reader.getRawCharacters(pos, endPos); |
731 char[] buf = reader.getRawCharacters(pos, endPos); |
732 return new BasicComment<UnicodeReader>(new UnicodeReader(fac, buf, buf.length), style); |
732 return new BasicComment<>(new UnicodeReader(fac, buf, buf.length), style); |
733 } |
733 } |
734 |
734 |
735 /** |
735 /** |
736 * Called when a complete whitespace run has been scanned. pos and endPos |
736 * Called when a complete whitespace run has been scanned. pos and endPos |
737 * will mark the whitespace boundary. |
737 * will mark the whitespace boundary. |