src/Tools/jEdit/src/jedit/isabelle_encoding.scala
author wenzelm
Sat, 08 May 2010 21:08:30 +0200
changeset 36760 b82a698ef6c9
parent 36015 6111de7c916a
child 37175 be764a7adb10
permissions -rw-r--r--
tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit/isabelle_encoding.scala
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
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
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
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    13
import org.gjt.sp.jedit.buffer.JEditBuffer
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    14
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    15
import java.nio.charset.{Charset, CodingErrorAction}
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    16
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    17
  CharArrayReader, ByteArrayOutputStream}
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    18
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    19
import scala.io.{Codec, Source, BufferedSource}
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    20
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    21
34738
80408ffc84a8 tuned file name;
wenzelm
parents: 34625
diff changeset
    22
object Isabelle_Encoding
34624
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    23
{
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    24
  val NAME = "UTF-8-Isabelle"
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    25
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34624
diff changeset
    26
  def is_active(buffer: JEditBuffer): Boolean =
34793
wenzelm
parents: 34777
diff changeset
    27
    buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
34624
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    28
}
5e4f33d033ba decentralized Isabelle component names;
wenzelm
parents: 34621
diff changeset
    29
34738
80408ffc84a8 tuned file name;
wenzelm
parents: 34625
diff changeset
    30
class Isabelle_Encoding extends Encoding
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    31
{
34805
c7417fb43112 Standard_System;
wenzelm
parents: 34793
diff changeset
    32
  private val charset = Charset.forName(Standard_System.charset)
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    33
  val BUFSIZE = 32768
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    34
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    35
  private def text_reader(in: InputStream, codec: Codec): Reader =
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    36
  {
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    37
    val source = new BufferedSource(in)(codec)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    38
    new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    39
  }
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    40
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    41
	override def getTextReader(in: InputStream): Reader =
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    42
    text_reader(in, Standard_System.codec())
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    43
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    44
	override def getPermissiveTextReader(in: InputStream): Reader =
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    45
	{
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    46
		val codec = Standard_System.codec()
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    47
		codec.onMalformedInput(CodingErrorAction.REPLACE)
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    48
		codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34805
diff changeset
    49
		text_reader(in, codec)
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    50
	}
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    51
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    52
  override def getTextWriter(out: OutputStream): Writer =
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    53
  {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    54
    val buffer = new ByteArrayOutputStream(BUFSIZE) {
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    55
      override def flush()
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    56
      {
34805
c7417fb43112 Standard_System;
wenzelm
parents: 34793
diff changeset
    57
        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
c7417fb43112 Standard_System;
wenzelm
parents: 34793
diff changeset
    58
        out.write(text.getBytes(Standard_System.charset))
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    59
        out.flush()
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    60
      }
34621
6cba4b3723e4 more precise wrapping of I/O streams;
wenzelm
parents: 34620
diff changeset
    61
      override def close() { out.close() }
34620
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    62
    }
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    63
		new OutputStreamWriter(buffer, charset.newEncoder())
5328c64f9866 some support for actual symbol recoding;
wenzelm
parents: 34619
diff changeset
    64
  }
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents:
diff changeset
    65
}