src/Pure/System/isabelle_charset.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73909 1d0d9772fff0
child 76356 92e9fa289056
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
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
55618
995162143ef4 tuned imports;
wenzelm
parents: 50203
diff changeset
     9
73909
1d0d9772fff0 tuned imports;
wenzelm
parents: 73366
diff changeset
    10
import java.util.{List => JList}
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    11
import java.nio.Buffer
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    12
import java.nio.{ByteBuffer, CharBuffer}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    13
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    14
import java.nio.charset.spi.CharsetProvider
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    15
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    16
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73909
diff changeset
    17
object Isabelle_Charset {
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    18
  val name: String = "UTF-8-Isabelle-test"  // FIXME
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    19
  lazy val charset: Charset = new Isabelle_Charset
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73909
diff changeset
    23
class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) {
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    24
  override def contains(cs: Charset): Boolean =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 44778
diff changeset
    25
    cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    26
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 44778
diff changeset
    27
  override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    28
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 44778
diff changeset
    29
  override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    30
}
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    31
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    32
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73909
diff changeset
    33
class Isabelle_Charset_Provider extends CharsetProvider {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73909
diff changeset
    34
  override def charsetForName(name: String): Charset = {
44778
18b1ba7cfcfe deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents: 43517
diff changeset
    35
    // FIXME inactive
18b1ba7cfcfe deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents: 43517
diff changeset
    36
    // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
18b1ba7cfcfe deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents: 43517
diff changeset
    37
    // else null
18b1ba7cfcfe deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents: 43517
diff changeset
    38
    null
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    39
  }
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    40
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73909
diff changeset
    41
  override def charsets(): java.util.Iterator[Charset] = {
44778
18b1ba7cfcfe deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents: 43517
diff changeset
    42
    // FIXME inactive
18b1ba7cfcfe deactivate unfinished charset provider for now, to avoid user confusion;
wenzelm
parents: 43517
diff changeset
    43
    // Iterator(Isabelle_Charset.charset)
73909
1d0d9772fff0 tuned imports;
wenzelm
parents: 73366
diff changeset
    44
    JList.of[Charset]().listIterator()
43517
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    45
  }
87ec9a1c0f98 basic setup for Isabelle charset;
wenzelm
parents:
diff changeset
    46
}