| author | wenzelm | 
| Sun, 02 Sep 2012 19:26:05 +0200 | |
| changeset 49065 | 8ead9e8b15fb | 
| parent 44778 | 18b1ba7cfcfe | 
| child 50203 | 00d8ad713e32 | 
| 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  | 
||
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  | 
  {
 | 
|
| 
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  | 
  {
 | 
|
48  | 
import scala.collection.JavaConversions._  | 
|
| 
44778
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
49  | 
// FIXME inactive  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
50  | 
// Iterator(Isabelle_Charset.charset)  | 
| 
 
18b1ba7cfcfe
deactivate unfinished charset provider for now, to avoid user confusion;
 
wenzelm 
parents: 
43517 
diff
changeset
 | 
51  | 
Iterator()  | 
| 43517 | 52  | 
}  | 
53  | 
}  | 
|
54  |