| 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 |   {
 | 
|  |     40 |     if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
 | 
|  |     41 |     else null
 | 
|  |     42 |   }
 | 
|  |     43 | 
 | 
|  |     44 |   override def charsets(): java.util.Iterator[Charset] =
 | 
|  |     45 |   {
 | 
|  |     46 |     import scala.collection.JavaConversions._
 | 
|  |     47 |     Iterator(Isabelle_Charset.charset)
 | 
|  |     48 |   }
 | 
|  |     49 | }
 | 
|  |     50 | 
 |