src/Pure/System/isabelle_charset.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 44778 18b1ba7cfcfe
child 50203 00d8ad713e32
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@43517
     1
/*  Title:      Pure/System/isabelle_charset.scala
wenzelm@43517
     2
    Author:     Makarius
wenzelm@43517
     3
wenzelm@43517
     4
Charset for Isabelle symbols.
wenzelm@43517
     5
*/
wenzelm@43517
     6
wenzelm@43517
     7
package isabelle
wenzelm@43517
     8
wenzelm@43517
     9
import java.nio.Buffer
wenzelm@43517
    10
import java.nio.{ByteBuffer, CharBuffer}
wenzelm@43517
    11
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
wenzelm@43517
    12
import java.nio.charset.spi.CharsetProvider
wenzelm@43517
    13
wenzelm@43517
    14
wenzelm@43517
    15
object Isabelle_Charset
wenzelm@43517
    16
{
wenzelm@43517
    17
  val name: String = "UTF-8-Isabelle-test"  // FIXME
wenzelm@43517
    18
  lazy val charset: Charset = new Isabelle_Charset
wenzelm@43517
    19
}
wenzelm@43517
    20
wenzelm@43517
    21
wenzelm@43517
    22
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null)
wenzelm@43517
    23
{
wenzelm@43517
    24
  override def contains(cs: Charset): Boolean =
wenzelm@43517
    25
    cs.name.equalsIgnoreCase(Standard_System.charset_name) ||
wenzelm@43517
    26
    Standard_System.charset.contains(cs)
wenzelm@43517
    27
wenzelm@43517
    28
  override def newDecoder(): CharsetDecoder =
wenzelm@43517
    29
    Standard_System.charset.newDecoder
wenzelm@43517
    30
wenzelm@43517
    31
  override def newEncoder(): CharsetEncoder =
wenzelm@43517
    32
    Standard_System.charset.newEncoder
wenzelm@43517
    33
}
wenzelm@43517
    34
wenzelm@43517
    35
wenzelm@43517
    36
class Isabelle_Charset_Provider extends CharsetProvider
wenzelm@43517
    37
{
wenzelm@43517
    38
  override def charsetForName(name: String): Charset =
wenzelm@43517
    39
  {
wenzelm@44778
    40
    // FIXME inactive
wenzelm@44778
    41
    // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
wenzelm@44778
    42
    // else null
wenzelm@44778
    43
    null
wenzelm@43517
    44
  }
wenzelm@43517
    45
wenzelm@43517
    46
  override def charsets(): java.util.Iterator[Charset] =
wenzelm@43517
    47
  {
wenzelm@43517
    48
    import scala.collection.JavaConversions._
wenzelm@44778
    49
    // FIXME inactive
wenzelm@44778
    50
    // Iterator(Isabelle_Charset.charset)
wenzelm@44778
    51
    Iterator()
wenzelm@43517
    52
  }
wenzelm@43517
    53
}
wenzelm@43517
    54