| author | blanchet | 
| Mon, 26 May 2014 14:15:48 +0200 | |
| changeset 57089 | 353652f47974 | 
| parent 55618 | 995162143ef4 | 
| child 71359 | 411c0322c09d | 
| 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  | 
||
15  | 
||
16  | 
object Isabelle_Charset  | 
|
17  | 
{
 | 
|
18  | 
val name: String = "UTF-8-Isabelle-test" // FIXME  | 
|
19  | 
lazy val charset: Charset = new Isabelle_Charset  | 
|
20  | 
}  | 
|
21  | 
||
22  | 
||
23  | 
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null)  | 
|
24  | 
{
 | 
|
25  | 
override def contains(cs: Charset): Boolean =  | 
|
| 50203 | 26  | 
cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)  | 
| 43517 | 27  | 
|
| 50203 | 28  | 
override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder  | 
| 43517 | 29  | 
|
| 50203 | 30  | 
override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder  | 
| 43517 | 31  | 
}  | 
32  | 
||
33  | 
||
34  | 
class Isabelle_Charset_Provider extends CharsetProvider  | 
|
35  | 
{
 | 
|
36  | 
override def charsetForName(name: String): Charset =  | 
|
37  | 
  {
 | 
|
| 
44778
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
38  | 
// FIXME inactive  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
39  | 
// 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
 | 
40  | 
// else null  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
41  | 
null  | 
| 43517 | 42  | 
}  | 
43  | 
||
44  | 
override def charsets(): java.util.Iterator[Charset] =  | 
|
45  | 
  {
 | 
|
46  | 
import scala.collection.JavaConversions._  | 
|
| 
44778
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
47  | 
// FIXME inactive  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
48  | 
// Iterator(Isabelle_Charset.charset)  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
49  | 
Iterator()  | 
| 43517 | 50  | 
}  | 
51  | 
}  | 
|
52  |