src/Pure/System/isabelle_charset.scala
changeset 44778 18b1ba7cfcfe
parent 43517 87ec9a1c0f98
child 50203 00d8ad713e32
equal deleted inserted replaced
44777:1afb48f872ae 44778:18b1ba7cfcfe
    35 
    35 
    36 class Isabelle_Charset_Provider extends CharsetProvider
    36 class Isabelle_Charset_Provider extends CharsetProvider
    37 {
    37 {
    38   override def charsetForName(name: String): Charset =
    38   override def charsetForName(name: String): Charset =
    39   {
    39   {
    40     if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
    40     // FIXME inactive
    41     else null
    41     // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
       
    42     // else null
       
    43     null
    42   }
    44   }
    43 
    45 
    44   override def charsets(): java.util.Iterator[Charset] =
    46   override def charsets(): java.util.Iterator[Charset] =
    45   {
    47   {
    46     import scala.collection.JavaConversions._
    48     import scala.collection.JavaConversions._
    47     Iterator(Isabelle_Charset.charset)
    49     // FIXME inactive
       
    50     // Iterator(Isabelle_Charset.charset)
       
    51     Iterator()
    48   }
    52   }
    49 }
    53 }
    50 
    54