changeset 34760 | dc7f5e0d9d27 |
parent 34759 | bfea7839d9e1 |
child 34777 | 91d6089cef88 |
34759:bfea7839d9e1 | 34760:dc7f5e0d9d27 |
---|---|
3 * |
3 * |
4 * @author Makarius |
4 * @author Makarius |
5 */ |
5 */ |
6 |
6 |
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
|
8 |
9 |
9 import org.gjt.sp.jedit.io.Encoding |
10 import org.gjt.sp.jedit.io.Encoding |
10 import org.gjt.sp.jedit.buffer.JEditBuffer |
11 import org.gjt.sp.jedit.buffer.JEditBuffer |
11 |
12 |
12 import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction} |
13 import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction} |