src/Pure/System/isabelle_charset.scala
author wenzelm
Thu, 23 Jun 2011 10:58:29 +0200
changeset 43517 87ec9a1c0f98
child 44778 18b1ba7cfcfe
permissions -rw-r--r--
basic setup for Isabelle charset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/isabelle_charset.scala
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     3
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     4
Charset for Isabelle symbols.
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     5
*/
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     6
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     7
package isabelle
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     8
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
     9
import java.nio.Buffer
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    10
import java.nio.{ByteBuffer, CharBuffer}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    11
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    12
import java.nio.charset.spi.CharsetProvider
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    13
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    14
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    15
object Isabelle_Charset
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    16
{
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    17
  val name: String = "UTF-8-Isabelle-test"  // FIXME
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    18
  lazy val charset: Charset = new Isabelle_Charset
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    19
}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    20
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    21
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    22
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null)
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    23
{
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    24
  override def contains(cs: Charset): Boolean =
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    25
    cs.name.equalsIgnoreCase(Standard_System.charset_name) ||
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    26
    Standard_System.charset.contains(cs)
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    27
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    28
  override def newDecoder(): CharsetDecoder =
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    29
    Standard_System.charset.newDecoder
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    30
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    31
  override def newEncoder(): CharsetEncoder =
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    32
    Standard_System.charset.newEncoder
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    33
}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    34
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    35
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    36
class Isabelle_Charset_Provider extends CharsetProvider
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    37
{
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    38
  override def charsetForName(name: String): Charset =
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    39
  {
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    40
    if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    41
    else null
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    42
  }
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    43
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    44
  override def charsets(): java.util.Iterator[Charset] =
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    45
  {
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    46
    import scala.collection.JavaConversions._
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    47
    Iterator(Isabelle_Charset.charset)
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    48
  }
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    49
}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    50