src/Pure/System/isabelle_charset.scala
changeset 44778 18b1ba7cfcfe
parent 43517 87ec9a1c0f98
child 50203 00d8ad713e32
--- 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()
   }
 }