--- a/src/Pure/System/isabelle_charset.scala Wed Sep 07 11:26:27 2011 +0200
+++ b/src/Pure/System/isabelle_charset.scala Wed Sep 07 11:36:39 2011 +0200
@@ -37,14 +37,18 @@
{
override def charsetForName(name: String): Charset =
{
- if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
- else null
+ // FIXME inactive
+ // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
+ // else null
+ null
}
override def charsets(): java.util.Iterator[Charset] =
{
import scala.collection.JavaConversions._
- Iterator(Isabelle_Charset.charset)
+ // FIXME inactive
+ // Iterator(Isabelle_Charset.charset)
+ Iterator()
}
}