--- a/src/Pure/General/word.scala Fri Apr 01 23:11:17 2016 +0200
+++ b/src/Pure/General/word.scala Sat Apr 02 14:17:03 2016 +0200
@@ -7,7 +7,7 @@
package isabelle
-
+import java.text.Bidi
import java.util.Locale
@@ -30,6 +30,15 @@
def codepoint(c: Int): String = new String(Array(c), 0, 1)
+ /* directionality */
+
+ def bidi_detect(str: String): Boolean =
+ str.exists(c => c >= 0x590) && Bidi.requiresBidi(str.toArray, 0, str.length)
+
+ def bidi_override(str: String): String =
+ if (bidi_detect(str)) "\u200E\u202D" + str + "\u202C" else str
+
+
/* case */
def lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
@@ -88,4 +97,3 @@
def explode(text: String): List[String] =
explode(Character.isWhitespace(_), text)
}
-