src/Pure/System/isabelle_charset.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 50203 00d8ad713e32
child 55618 995162143ef4
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
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@50203
    25
    cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)
wenzelm@43517
    26
wenzelm@50203
    27
  override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder
wenzelm@43517
    28
wenzelm@50203
    29
  override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder
wenzelm@43517
    30
}
wenzelm@43517
    31
wenzelm@43517
    32
wenzelm@43517
    33
class Isabelle_Charset_Provider extends CharsetProvider
wenzelm@43517
    34
{
wenzelm@43517
    35
  override def charsetForName(name: String): Charset =
wenzelm@43517
    36
  {
wenzelm@44778
    37
    // FIXME inactive
wenzelm@44778
    38
    // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
wenzelm@44778
    39
    // else null
wenzelm@44778
    40
    null
wenzelm@43517
    41
  }
wenzelm@43517
    42
wenzelm@43517
    43
  override def charsets(): java.util.Iterator[Charset] =
wenzelm@43517
    44
  {
wenzelm@43517
    45
    import scala.collection.JavaConversions._
wenzelm@44778
    46
    // FIXME inactive
wenzelm@44778
    47
    // Iterator(Isabelle_Charset.charset)
wenzelm@44778
    48
    Iterator()
wenzelm@43517
    49
  }
wenzelm@43517
    50
}
wenzelm@43517
    51