author | wenzelm |
Mon, 04 Dec 2017 22:52:16 +0100 | |
changeset 67130 | b023f64e0d16 |
parent 66457 | 9098c36abd1a |
child 73987 | fc363a3b690a |
permissions | -rw-r--r-- |
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 | 2 |
Author: Makarius |
3 |
||
4 |
Isabelle encoding -- based on UTF-8. |
|
5 |
*/ |
|
34619 | 6 |
|
7 |
package isabelle.jedit |
|
8 |
||
34760 | 9 |
|
36015 | 10 |
import isabelle._ |
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 | 13 |
|
14 |
||
34738 | 15 |
object Isabelle_Encoding |
34624 | 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 | 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 | 22 |
} |