isabelle: src/Tools/jEdit/src/isabelle_encoding.scala@3dced198b9ec (annotated)

43282 5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory; wenzelm parents: 37175 diff changeset	1	/* Title: Tools/jEdit/src/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
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
34625 799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file); wenzelm parents: 34624 diff changeset	12	import org.gjt.sp.jedit.buffer.JEditBuffer
34619 e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now; wenzelm parents: diff changeset	13
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now; wenzelm parents: diff changeset	14
34738 80408ffc84a8 tuned file name; wenzelm parents: 34625 diff changeset	15	object Isabelle_Encoding
34624 5e4f33d033ba decentralized Isabelle component names; wenzelm parents: 34621 diff changeset	16	{
34625 799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file); wenzelm parents: 34624 diff changeset	17	def is_active(buffer: JEditBuffer): Boolean =
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	18	buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 50203 diff changeset	19
67130 b023f64e0d16 tuned signature; wenzelm parents: 66457 diff changeset	20	def perhaps_decode(buffer: JEditBuffer, s: String): String =
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 50203 diff changeset	21	if (is_active(buffer)) Symbol.decode(s) else s
34624 5e4f33d033ba decentralized Isabelle component names; wenzelm parents: 34621 diff changeset	22	}

author	wenzelm
	Mon, 25 Mar 2019 17:21:26 +0100
changeset 69981	3dced198b9ec
parent 67130	b023f64e0d16
child 73987	fc363a3b690a
permissions	-rw-r--r--