| author | wenzelm |
| Wed, 12 Mar 2025 11:22:08 +0100 | |
| changeset 82264 | 756e88885a7c |
| parent 82142 | 508a673c87ac |
| 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 |
|
| 73909 | 10 |
import java.util.{List => JList}
|
| 82142 | 11 |
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder}
|
| 43517 | 12 |
import java.nio.charset.spi.CharsetProvider |
13 |
||
14 |
||
| 75393 | 15 |
object Isabelle_Charset {
|
| 43517 | 16 |
val name: String = "UTF-8-Isabelle-test" // FIXME |
17 |
lazy val charset: Charset = new Isabelle_Charset |
|
18 |
} |
|
19 |
||
20 |
||
| 75393 | 21 |
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) {
|
| 43517 | 22 |
override def contains(cs: Charset): Boolean = |
| 76356 | 23 |
cs.name.equalsIgnoreCase(UTF8.charset.name) || UTF8.charset.contains(cs) |
| 43517 | 24 |
|
| 50203 | 25 |
override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder |
| 43517 | 26 |
|
| 50203 | 27 |
override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder |
| 43517 | 28 |
} |
29 |
||
30 |
||
| 75393 | 31 |
class Isabelle_Charset_Provider extends CharsetProvider {
|
32 |
override def charsetForName(name: String): Charset = {
|
|
|
44778
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
33 |
// FIXME inactive |
|
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
34 |
// 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
|
35 |
// else null |
|
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents:
43517
diff
changeset
|
36 |
null |
| 43517 | 37 |
} |
38 |
||
| 75393 | 39 |
override def charsets(): java.util.Iterator[Charset] = {
|
|
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 |
// Iterator(Isabelle_Charset.charset) |
| 73909 | 42 |
JList.of[Charset]().listIterator() |
| 43517 | 43 |
} |
44 |
} |