| author | wenzelm | 
| Fri, 16 Sep 2022 20:54:56 +0200 | |
| changeset 76177 | b847a9983784 | 
| parent 75393 | 87ebf5a50283 | 
| child 76356 | 92e9fa289056 | 
| 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}
 | 
| 43517 | 11  | 
import java.nio.Buffer  | 
12  | 
import java.nio.{ByteBuffer, CharBuffer}
 | 
|
13  | 
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
 | 
|
14  | 
import java.nio.charset.spi.CharsetProvider  | 
|
15  | 
||
16  | 
||
| 75393 | 17  | 
object Isabelle_Charset {
 | 
| 43517 | 18  | 
val name: String = "UTF-8-Isabelle-test" // FIXME  | 
19  | 
lazy val charset: Charset = new Isabelle_Charset  | 
|
20  | 
}  | 
|
21  | 
||
22  | 
||
| 75393 | 23  | 
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) {
 | 
| 43517 | 24  | 
override def contains(cs: Charset): Boolean =  | 
| 50203 | 25  | 
cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)  | 
| 43517 | 26  | 
|
| 50203 | 27  | 
override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder  | 
| 43517 | 28  | 
|
| 50203 | 29  | 
override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder  | 
| 43517 | 30  | 
}  | 
31  | 
||
32  | 
||
| 75393 | 33  | 
class Isabelle_Charset_Provider extends CharsetProvider {
 | 
34  | 
  override def charsetForName(name: String): Charset = {
 | 
|
| 
44778
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
35  | 
// FIXME inactive  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
36  | 
// 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
 | 
37  | 
// else null  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
38  | 
null  | 
| 43517 | 39  | 
}  | 
40  | 
||
| 75393 | 41  | 
  override def charsets(): java.util.Iterator[Charset] = {
 | 
| 
44778
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
42  | 
// FIXME inactive  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
43  | 
// Iterator(Isabelle_Charset.charset)  | 
| 73909 | 44  | 
JList.of[Charset]().listIterator()  | 
| 43517 | 45  | 
}  | 
46  | 
}  |