equal
deleted
inserted
replaced
3 |
3 |
4 Charset for Isabelle symbols. |
4 Charset for Isabelle symbols. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
|
8 |
8 |
9 |
9 import java.nio.Buffer |
10 import java.nio.Buffer |
10 import java.nio.{ByteBuffer, CharBuffer} |
11 import java.nio.{ByteBuffer, CharBuffer} |
11 import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult} |
12 import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult} |
12 import java.nio.charset.spi.CharsetProvider |
13 import java.nio.charset.spi.CharsetProvider |