43517
|
1 |
/* Title: Pure/System/isabelle_charset.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Charset for Isabelle symbols.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
import java.nio.Buffer
|
|
10 |
import java.nio.{ByteBuffer, CharBuffer}
|
|
11 |
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
|
|
12 |
import java.nio.charset.spi.CharsetProvider
|
|
13 |
|
|
14 |
|
|
15 |
object Isabelle_Charset
|
|
16 |
{
|
|
17 |
val name: String = "UTF-8-Isabelle-test" // FIXME
|
|
18 |
lazy val charset: Charset = new Isabelle_Charset
|
|
19 |
}
|
|
20 |
|
|
21 |
|
|
22 |
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null)
|
|
23 |
{
|
|
24 |
override def contains(cs: Charset): Boolean =
|
|
25 |
cs.name.equalsIgnoreCase(Standard_System.charset_name) ||
|
|
26 |
Standard_System.charset.contains(cs)
|
|
27 |
|
|
28 |
override def newDecoder(): CharsetDecoder =
|
|
29 |
Standard_System.charset.newDecoder
|
|
30 |
|
|
31 |
override def newEncoder(): CharsetEncoder =
|
|
32 |
Standard_System.charset.newEncoder
|
|
33 |
}
|
|
34 |
|
|
35 |
|
|
36 |
class Isabelle_Charset_Provider extends CharsetProvider
|
|
37 |
{
|
|
38 |
override def charsetForName(name: String): Charset =
|
|
39 |
{
|
|
40 |
if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
|
|
41 |
else null
|
|
42 |
}
|
|
43 |
|
|
44 |
override def charsets(): java.util.Iterator[Charset] =
|
|
45 |
{
|
|
46 |
import scala.collection.JavaConversions._
|
|
47 |
Iterator(Isabelle_Charset.charset)
|
|
48 |
}
|
|
49 |
}
|
|
50 |
|