# HG changeset patch
# User wenzelm
# Date 1459599423 -7200
# Node ID ce22e5c3d4ceb2948a06815cd3233ef891aa19af
# Parent  1948d555a55a6088c3177f94b3e1c9702c06ff57
more robust display of bidirectional Unicode text: enforce left-to-right;

diff -r 1948d555a55a -r ce22e5c3d4ce etc/isabelle.css
--- a/etc/isabelle.css	Fri Apr 01 23:11:17 2016 +0200
+++ b/etc/isabelle.css	Sat Apr 02 14:17:03 2016 +0200
@@ -15,6 +15,7 @@
 
 .head     { background-color: #FFFFFF; }
 .source   {
+  direction: ltr; unicode-bidi: bidi-override;
   background-color: #FFFFFF;
   padding: 10px;
   font-family: IsabelleText;
diff -r 1948d555a55a -r ce22e5c3d4ce src/HOL/ex/Hebrew.thy
--- a/src/HOL/ex/Hebrew.thy	Fri Apr 01 23:11:17 2016 +0200
+++ b/src/HOL/ex/Hebrew.thy	Sat Apr 02 14:17:03 2016 +0200
@@ -10,17 +10,8 @@
 imports Main
 begin
 
-subsection \<open>Warning: formal Unicode considered harmful\<close>
-
 text \<open>
-  Important note: editors or browsers that implement the \<^emph>\<open>Unicode
-  Bidirectional Algorithm\<close> correctly (!) will display the following mix of
-  left-to-right versus right-to-left characters in a way that is logical
-  nonsense.
-
-  To avoid such uncertainty, formal notation should be restricted to
-  well-known Isabelle symbols and their controlled rendering (in Unicode or
-  LaTeX).
+  \<^bold>\<open>Warning:\<close> Bidirectional Unicode text may confuse display in browsers, editors, etc.!
 \<close>
 
 subsection \<open>The Hebrew Alef-Bet (א-ב).\<close>
diff -r 1948d555a55a -r ce22e5c3d4ce src/Pure/General/word.scala
--- 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)
 }
-
diff -r 1948d555a55a -r ce22e5c3d4ce src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Fri Apr 01 23:11:17 2016 +0200
+++ b/src/Tools/Graphview/shapes.scala	Sat Apr 02 14:17:03 2016 +0200
@@ -60,7 +60,10 @@
       (info.lines.length max 1) * metrics.height.ceil
     val x = (s.getCenterX - text_width / 2).round.toInt
     var y = (s.getCenterY - text_height / 2 + metrics.ascent).round.toInt
-    for (line <- info.lines) { gfx.drawString(line, x, y); y += metrics.height.ceil.toInt }
+    for (line <- info.lines) {
+      gfx.drawString(Word.bidi_override(line), x, y)
+      y += metrics.height.ceil.toInt
+    }
   }
 
   def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info)
diff -r 1948d555a55a -r ce22e5c3d4ce src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 01 23:11:17 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Apr 02 14:17:03 2016 +0200
@@ -420,19 +420,19 @@
               val s2 = str.substring(i, j)
               val s3 = str.substring(j)
 
-              if (s1.nonEmpty) gfx.drawString(s1, x1, y)
+              if (s1.nonEmpty) gfx.drawString(Word.bidi_override(s1), x1, y)
 
-              val astr = new AttributedString(s2)
+              val astr = new AttributedString(Word.bidi_override(s2))
               astr.addAttribute(TextAttribute.FONT, chunk_font)
               astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
 
               if (s3.nonEmpty)
-                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
+                gfx.drawString(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y)
 
             case _ =>
-              gfx.drawString(str, x1, y)
+              gfx.drawString(Word.bidi_override(str), x1, y)
           }
           x1 += string_width(str)
         }