src/Tools/jEdit/src-base/isabelle_encoding.scala
author wenzelm
Fri, 01 Sep 2017 15:15:29 +0200
changeset 66591 6efa351190d0
parent 66457 9098c36abd1a
child 67304 3cf05d7cf174
permissions -rw-r--r--
more robust: provide docking framework via base plugin;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 62527
diff changeset
     1
/*  Title:      Tools/jEdit/src-base/isabelle_encoding.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     4
Isabelle encoding -- based on UTF-8.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     5
*/
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     6
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 62527
diff changeset
     7
package isabelle.jedit_base
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     8
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
     9
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    10
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    11
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    12
import org.gjt.sp.jedit.io.Encoding
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    13
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    14
import java.nio.charset.{Charset, CodingErrorAction}
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    15
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    16
  CharArrayReader, ByteArrayOutputStream}
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    17
48277
f14e564fca1a tuned imports;
wenzelm
parents: 43695
diff changeset
    18
import scala.io.{Codec, BufferedSource}
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    19
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    20
34738
80408ffc84a8 tuned file name;
wenzelm
parents: 34625
diff changeset
    21
class Isabelle_Encoding extends Encoding
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    22
{
43516
1c4736b9396a prefer actual charset over charset name;
wenzelm
parents: 43282
diff changeset
    23
  private val BUFSIZE = 32768
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    24
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    25
  private def text_reader(in: InputStream, codec: Codec): Reader =
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    26
  {
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    27
    val source = new BufferedSource(in)(codec)
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43661
diff changeset
    28
    new CharArrayReader(Symbol.decode(source.mkString).toArray)
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    29
  }
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    30
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 48277
diff changeset
    31
  override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec())
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    32
37175
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
    33
  override def getPermissiveTextReader(in: InputStream): Reader =
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
    34
  {
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 48277
diff changeset
    35
    val codec = UTF8.codec()
37175
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
    36
    codec.onMalformedInput(CodingErrorAction.REPLACE)
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
    37
    codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
    38
    text_reader(in, codec)
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
    39
  }
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    40
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    41
  override def getTextWriter(out: OutputStream): Writer =
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    42
  {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    43
    val buffer = new ByteArrayOutputStream(BUFSIZE) {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    44
      override def flush()
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    45
      {
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 48277
diff changeset
    46
        val text = Symbol.encode(toString(UTF8.charset_name))
62527
aae9a2a855e0 tuned signature;
wenzelm
parents: 62104
diff changeset
    47
        out.write(UTF8.bytes(text))
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    48
        out.flush()
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    49
      }
34621
6cba4b3723e4 more precise wrapping of I/O streams;
wenzelm
parents: 34620
diff changeset
    50
      override def close() { out.close() }
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    51
    }
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 48277
diff changeset
    52
    new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    53
  }
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    54
}