author | wenzelm |
Thu, 09 Jan 2020 13:47:08 +0100 | |
changeset 71359 | 411c0322c09d |
parent 55618 | 995162143ef4 |
child 73366 | 5f388e514ab8 |
permissions | -rw-r--r-- |
43517 | 1 |
/* Title: Pure/System/isabelle_charset.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Charset for Isabelle symbols. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
55618 | 9 |
|
43517 | 10 |
import java.nio.Buffer |
11 |
import java.nio.{ByteBuffer, CharBuffer} |
|
12 |
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult} |
|
13 |
import java.nio.charset.spi.CharsetProvider |
|
14 |
||
71359
411c0322c09d
eliminated deprecated scala.collection.JavaConversions;
wenzelm
parents:
55618
diff
changeset
|
15 |
import scala.collection.JavaConverters |
411c0322c09d
eliminated deprecated scala.collection.JavaConversions;
wenzelm
parents:
55618
diff
changeset
|
16 |
|
43517 | 17 |
|
18 |
object Isabelle_Charset |
|
19 |
{ |
|
20 |
val name: String = "UTF-8-Isabelle-test" // FIXME |
|
21 |
lazy val charset: Charset = new Isabelle_Charset |
|
22 |
} |
|
23 |
||
24 |
||
25 |
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) |
|
26 |
{ |
|
27 |
override def contains(cs: Charset): Boolean = |
|
50203 | 28 |
cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs) |
43517 | 29 |
|
50203 | 30 |
override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder |
43517 | 31 |
|
50203 | 32 |
override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder |
43517 | 33 |
} |
34 |
||
35 |
||
36 |
class Isabelle_Charset_Provider extends CharsetProvider |
|
37 |
{ |
|
38 |
override def charsetForName(name: String): Charset = |
|
39 |
{ |
|
44778
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
40 |
// FIXME inactive |
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
41 |
// if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset |
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
42 |
// else null |
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
43 |
null |
43517 | 44 |
} |
45 |
||
46 |
override def charsets(): java.util.Iterator[Charset] = |
|
47 |
{ |
|
44778
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
48 |
// FIXME inactive |
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
49 |
// Iterator(Isabelle_Charset.charset) |
71359
411c0322c09d
eliminated deprecated scala.collection.JavaConversions;
wenzelm
parents:
55618
diff
changeset
|
50 |
JavaConverters.asJavaIterator(Iterator()) |
43517 | 51 |
} |
52 |
} |