diff --git a/etc/isabelle.css b/etc/isabelle.css --- a/etc/isabelle.css +++ b/etc/isabelle.css @@ -1,65 +1,66 @@ /* style file for Isabelle XHTML/XML output */ @font-face { font-family: 'IsabelleText'; src: url('IsabelleText.ttf') format('truetype'); } @font-face { font-family: 'IsabelleText'; src: url('IsabelleTextBold.ttf') format('truetype'); font-weight: bold; } body { background-color: #FFFFFF; } .head { background-color: #FFFFFF; } .source { + direction: ltr; unicode-bidi: bidi-override; background-color: #FFFFFF; padding: 10px; font-family: IsabelleText; line-height: 120%; } .external_source { background-color: #FFFFFF; padding: 10px; } .external_footer { background-color: #FFFFFF; } .theories { background-color: #FFFFFF; padding: 10px; } .sessions { background-color: #FFFFFF; padding: 10px; } .name { font-style: italic; } .filename { font-family: fixed; } /* basic syntax markup */ .hidden { font-size: 1px; visibility: hidden; } .binding { color: #336655; } .tfree { color: #A020F0; } .tvar { color: #A020F0; } .free { color: blue; } .skolem { color: #D2691E; } .bound { color: green; } .var { color: #00009B; } .numeral { } .literal { font-weight: bold; } .delimiter { } .inner_string { color: #FF00CC; } .inner_cartouche { color: #CC6600; } .inner_comment { color: #CC0000; } .bold { font-weight: bold; } .keyword1 { color: #006699; font-weight: bold; } .keyword2 { color: #009966; font-weight: bold; } .keyword3 { color: #0099FF; font-weight: bold; } .operator { } .string { color: #FF00CC; } .alt_string { color: #CC00CC; } .verbatim { color: #6600CC; } .cartouche { color: #CC6600; } .comment { color: #CC0000; } .improper { color: #FF5050; } .bad { background-color: #FF6A6A; } diff --git a/src/HOL/ex/Hebrew.thy b/src/HOL/ex/Hebrew.thy --- a/src/HOL/ex/Hebrew.thy +++ b/src/HOL/ex/Hebrew.thy @@ -1,87 +1,78 @@ (* Author: Makarius Example theory involving Unicode characters (UTF-8 encoding) -- both formal and informal ones. *) section \A Hebrew theory\ theory Hebrew imports Main begin -subsection \Warning: formal Unicode considered harmful\ - text \ - Important note: editors or browsers that implement the \<^emph>\Unicode - Bidirectional Algorithm\ 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>\Warning:\ Bidirectional Unicode text may confuse display in browsers, editors, etc.! \ subsection \The Hebrew Alef-Bet (א-ב).\ datatype alef_bet = Alef ("א") | Bet ("ב") | Gimel ("ג") | Dalet ("ד") | He ("ה") | Vav ("ו") | Zayin ("ז") | Het ("ח") | Tet ("ט") | Yod ("י") | Kaf ("כ") | Lamed ("ל") | Mem ("מ") | Nun ("נ") | Samekh ("ס") | Ayin ("ע") | Pe ("פ") | Tsadi ("צ") | Qof ("ק") | Resh ("ר") | Shin ("ש") | Tav ("ת") thm alef_bet.induct subsection \Interpreting Hebrew letters as numbers.\ primrec mispar :: "alef_bet \ nat" where "mispar א = 1" | "mispar ב = 2" | "mispar ג = 3" | "mispar ד = 4" | "mispar ה = 5" | "mispar ו = 6" | "mispar ז = 7" | "mispar ח = 8" | "mispar ט = 9" | "mispar י = 10" | "mispar כ = 20" | "mispar ל = 30" | "mispar מ = 40" | "mispar נ = 50" | "mispar ס = 60" | "mispar ע = 70" | "mispar פ = 80" | "mispar צ = 90" | "mispar ק = 100" | "mispar ר = 200" | "mispar ש = 300" | "mispar ת = 400" thm mispar.simps lemma "mispar ק + mispar ל + mispar ה = 135" by simp end diff --git a/src/Pure/General/word.scala b/src/Pure/General/word.scala --- a/src/Pure/General/word.scala +++ b/src/Pure/General/word.scala @@ -1,91 +1,99 @@ /* Title: Pure/General/word.scala Module: PIDE Author: Makarius Support for words within Unicode text. */ package isabelle - +import java.text.Bidi import java.util.Locale object Word { /* codepoints */ def codepoint_iterator(str: String): Iterator[Int] = new Iterator[Int] { var offset = 0 def hasNext: Boolean = offset < str.length def next: Int = { val c = str.codePointAt(offset) offset += Character.charCount(c) c } } 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) def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) def capitalize(str: String): String = if (str.length == 0) str else { val n = Character.charCount(str.codePointAt(0)) uppercase(str.substring(0, n)) + lowercase(str.substring(n)) } def perhaps_capitalize(str: String): String = if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c))) capitalize(str) else str sealed abstract class Case case object Lowercase extends Case case object Uppercase extends Case case object Capitalized extends Case object Case { def apply(c: Case, str: String): String = c match { case Lowercase => lowercase(str) case Uppercase => uppercase(str) case Capitalized => capitalize(str) } def unapply(str: String): Option[Case] = if (str.nonEmpty) { if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase) else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase) else { val it = codepoint_iterator(str) if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_))) Some(Capitalized) else None } } else None } /* sequence of words */ def implode(words: Iterable[String]): String = words.iterator.mkString(" ") def explode(sep: Char => Boolean, text: String): List[String] = Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList def explode(sep: Char, text: String): List[String] = explode(_ == sep, text) def explode(text: String): List[String] = explode(Character.isWhitespace(_), text) } - diff --git a/src/Tools/Graphview/shapes.scala b/src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala +++ b/src/Tools/Graphview/shapes.scala @@ -1,226 +1,229 @@ /* Title: Tools/Graphview/shapes.scala Author: Markus Kaiser, TU Muenchen Author: Makarius Drawable shapes. */ package isabelle.graphview import isabelle._ import java.awt.{BasicStroke, Graphics2D, Shape} import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, RoundRectangle2D, PathIterator} object Shapes { private val default_stroke = new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) def shape(info: Layout.Info): Rectangle2D.Double = new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height) def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node) { val metrics = graphview.metrics val extra = metrics.char_width val info = graphview.layout.get_node(node) gfx.setColor(graphview.highlight_color) gfx.fill(new Rectangle2D.Double( info.x - info.width2 - extra, info.y - info.height2 - extra, info.width + 2 * extra, info.height + 2 * extra)) } def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node) { val metrics = graphview.metrics val info = graphview.layout.get_node(node) val c = graphview.node_color(node) val s = shape(info) gfx.setColor(c.background) gfx.fill(s) gfx.setColor(c.border) gfx.setStroke(default_stroke) gfx.draw(s) gfx.setColor(c.foreground) gfx.setFont(metrics.font) val text_width = (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth } val text_height = (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) { gfx.setStroke(default_stroke) gfx.setColor(graphview.dummy_color) gfx.draw(shape(info)) } object Straight_Edge { def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge) { val p = graphview.layout.get_node(edge._1) val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) ds.foreach(d => path.lineTo(d.x, d.y)) path.lineTo(q.x, q.y) if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } object Cardinal_Spline_Edge { private val slack = 0.1 def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge) { val p = graphview.layout.get_node(edge._1) val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge) else { val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) val coords = p :: ds ::: List(q) val dx = coords(2).x - coords(0).x val dy = coords(2).y - coords(0).y val (dx2, dy2) = ((dx, dy) /: coords.sliding(3)) { case ((dx, dy), List(l, m, r)) => val dx2 = r.x - l.x val dy2 = r.y - l.y path.curveTo( l.x + slack * dx, l.y + slack * dy, m.x - slack * dx2, m.y - slack * dy2, m.x, m.y) (dx2, dy2) } val l = ds.last path.curveTo( l.x + slack * dx2, l.y + slack * dy2, q.x - slack * dx2, q.y - slack * dy2, q.x, q.y) if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } } object Arrow_Head { type Point = (Double, Double) private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = { def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = { val i = path.getPathIterator(null, 1.0) val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0) var p1 = (0.0, 0.0) var p2 = (0.0, 0.0) while (!i.isDone) { i.currentSegment(seg) match { case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) case PathIterator.SEG_LINETO => p1 = p2 p2 = (seg(0), seg(1)) if(shape.contains(seg(0), seg(1))) return Some((p1, p2)) case _ => } i.next() } None } def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = { val ((fx, fy), (tx, ty)) = line if (shape.contains(fx, fy) == shape.contains(tx, ty)) None else { val (dx, dy) = (fx - tx, fy - ty) if ((dx * dx + dy * dy) < 1.0) { val at = AffineTransform.getTranslateInstance(fx, fy) at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) Some(at) } else { val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) if (shape.contains(fx, fy) == shape.contains(mx, my)) binary_search(((mx, my), (tx, ty)), shape) else binary_search(((fx, fy), (mx, my)), shape) } } } intersecting_line(path, shape) match { case None => None case Some(line) => binary_search(line, shape) } } def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape) { position(path, shape) match { case None => case Some(at) => val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) arrow.moveTo(0, 0) arrow.lineTo(-10, 4) arrow.lineTo(-6, 0) arrow.lineTo(-10, -4) arrow.lineTo(0, 0) arrow.transform(at) gfx.fill(arrow) } } } } diff --git a/src/Tools/jEdit/src/rich_text_area.scala b/src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala +++ b/src/Tools/jEdit/src/rich_text_area.scala @@ -1,673 +1,673 @@ /* Title: Tools/jEdit/src/rich_text_area.scala Author: Makarius Enhanced version of jEdit text area, with rich text rendering, tooltips, hyperlinks etc. */ package isabelle.jedit import isabelle._ import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo} import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} import java.awt.font.TextAttribute import javax.swing.SwingUtilities import java.text.AttributedString import java.util.ArrayList import scala.util.matching.Regex import org.gjt.sp.util.Log import org.gjt.sp.jedit.{OperatingSystem, Debug, View} import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} class Rich_Text_Area( view: View, text_area: TextArea, get_rendering: () => Rendering, close_action: () => Unit, get_search_pattern: () => Option[Regex], caret_visible: Boolean, enable_hovering: Boolean) { private val buffer = text_area.getBuffer /* robust extension body */ def robust_body[A](default: A)(body: => A): A = { try { GUI_Thread.require {} if (buffer == text_area.getBuffer) body else { Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer")) default } } catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default } } /* original painters */ private def pick_extension(name: String): TextAreaExtension = { text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList match { case List(x) => x case _ => error("Expected exactly one " + name) } } private val orig_text_painter = pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") /* common painter state */ @volatile private var painter_rendering: Rendering = null @volatile private var painter_clip: Shape = null private val set_state = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { painter_rendering = get_rendering() painter_clip = gfx.getClip } } private val reset_state = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { painter_rendering = null painter_clip = null } } def robust_rendering(body: Rendering => Unit) { robust_body(()) { body(painter_rendering) } } /* active areas within the text */ private class Active_Area[A]( rendering: Rendering => Text.Range => Option[Text.Info[A]], cursor: Option[Int]) { private var the_text_info: Option[(String, Text.Info[A])] = None def is_active: Boolean = the_text_info.isDefined def text_info: Option[(String, Text.Info[A])] = the_text_info def info: Option[Text.Info[A]] = the_text_info.map(_._2) def update(new_info: Option[Text.Info[A]]) { val old_text_info = the_text_info val new_text_info = new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) if (new_text_info != old_text_info) { if (cursor.isDefined) { if (new_text_info.isDefined) text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) else text_area.getPainter.resetCursor() } for { r0 <- JEdit_Lib.visible_range(text_area) opt <- List(old_text_info, new_text_info) (_, Text.Info(r1, _)) <- opt r2 <- r1.try_restrict(r0) // FIXME more precise?! } JEdit_Lib.invalidate_range(text_area, r2) the_text_info = new_text_info } } def update_rendering(r: Rendering, range: Text.Range) { update(rendering(r)(range)) } def reset { update(None) } } // owned by GUI thread private val highlight_area = new Active_Area[Color]( (rendering: Rendering) => rendering.highlight _, None) private val hyperlink_area = new Active_Area[PIDE.editor.Hyperlink]( (rendering: Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR)) private val active_area = new Active_Area[XML.Elem]( (rendering: Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR)) private val active_areas = List((highlight_area, true), (hyperlink_area, true), (active_area, false)) def active_reset(): Unit = active_areas.foreach(_._1.reset) private val focus_listener = new FocusAdapter { override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } } } private val window_listener = new WindowAdapter { override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } } override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } } } private val mouse_listener = new MouseAdapter { override def mouseClicked(e: MouseEvent) { robust_body(()) { hyperlink_area.info match { case Some(Text.Info(range, link)) => if (!link.external) { try { text_area.moveCaretPosition(range.start) } catch { case _: ArrayIndexOutOfBoundsException => case _: IllegalArgumentException => } text_area.requestFocus } link.follow(view) case None => } active_area.text_info match { case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup) close_action() case None => } } } } private def mouse_inside_painter(): Boolean = MouseInfo.getPointerInfo match { case null => false case info => val point = info.getLocation val painter = text_area.getPainter SwingUtilities.convertPointFromScreen(point, painter) painter.contains(point) } private val mouse_motion_listener = new MouseMotionAdapter { override def mouseDragged(evt: MouseEvent) { robust_body(()) { active_reset() Completion_Popup.Text_Area.dismissed(text_area) Pretty_Tooltip.dismiss_descendant(text_area.getPainter) } } override def mouseMoved(evt: MouseEvent) { robust_body(()) { val x = evt.getX val y = evt.getY val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 if ((control || enable_hovering) && !buffer.isLoading) { JEdit_Lib.buffer_lock(buffer) { JEdit_Lib.pixel_range(text_area, x, y) match { case None => active_reset() case Some(range) => val rendering = get_rendering() for ((area, require_control) <- active_areas) { if (control == require_control && !rendering.snapshot.is_outdated) area.update_rendering(rendering, range) else area.reset } } } } else active_reset() if (evt.getSource == text_area.getPainter) { Pretty_Tooltip.invoke(() => robust_body(()) { if (mouse_inside_painter()) { val rendering = get_rendering() val snapshot = rendering.snapshot if (!snapshot.is_outdated) { JEdit_Lib.pixel_range(text_area, x, y) match { case None => case Some(range) => val result = if (control) rendering.tooltip(range) else rendering.tooltip_message(range) result match { case None => case Some(tip) => val painter = text_area.getPainter val loc = new Point(x, y + painter.getLineHeight / 2) val results = rendering.command_results(tip.range) Pretty_Tooltip(view, painter, loc, rendering, results, tip) } } } } }) } } } } /* text background */ private val background_painter = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { robust_rendering { rendering => val fm = text_area.getPainter.getFontMetrics for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) // line background color for { (color, separator) <- rendering.line_background(line_range) } { gfx.setColor(color) val sep = if (separator) 2 min (line_height / 2) else 0 gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) } // background color for { Text.Info(range, color) <- rendering.background(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } // active area -- potentially from other snapshot for { info <- active_area.info Text.Info(range, _) <- info.try_restrict(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.active_hover_color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } // squiggly underline for { Text.Info(range, color) <- rendering.squiggly_underline(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) val x0 = (r.x / 2) * 2 val y0 = r.y + fm.getAscent + 1 for (x1 <- Range(x0, x0 + r.length, 2)) { val y1 = if (x1 % 4 < 2) y0 else y0 + 1 gfx.drawLine(x1, y1, x1 + 1, y1) } } // spell checker for { spell_checker <- PIDE.spell_checker.get spell_range <- rendering.spell_checker_ranges(line_range) text <- JEdit_Lib.try_get_text(buffer, spell_range) info <- spell_checker.marked_words(spell_range.start, text) r <- JEdit_Lib.gfx_range(text_area, info.range) } { gfx.setColor(rendering.spell_checker_color) val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) gfx.drawLine(r.x, y0, r.x + r.length, y0) } } } } } } /* text */ private def caret_enabled: Boolean = caret_visible && (!text_area.hasFocus || text_area.isCaretVisible) private def caret_color(rendering: Rendering, offset: Text.Offset): Color = { if (text_area.isCaretVisible) text_area.getPainter.getCaretColor else { val debug_positions = (for { c <- Debugger.focus().iterator pos <- c.debug_position.iterator } yield pos).toList if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _))) rendering.caret_debugger_color else rendering.caret_invisible_color } } private def paint_chunk_list(rendering: Rendering, gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = { val clip_rect = gfx.getClipBounds val painter = text_area.getPainter val font_context = painter.getFontRenderContext val caret_range = if (caret_enabled) JEdit_Lib.caret_range(text_area) else Text.Range.offside var w = 0.0f var chunk = head while (chunk != null) { val chunk_offset = line_start + chunk.offset if (x + w + chunk.width > clip_rect.x && x + w < clip_rect.x + clip_rect.width && chunk.length > 0) { val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str val chunk_font = chunk.style.getFont val chunk_color = chunk.style.getForegroundColor def string_width(s: String): Float = if (s.isEmpty) 0.0f else chunk_font.getStringBounds(s, font_context).getWidth.toFloat val markup = for { r1 <- rendering.text_color(chunk_range, chunk_color) r2 <- r1.try_restrict(chunk_range) } yield r2 val padded_markup_iterator = if (markup.isEmpty) Iterator(Text.Info(chunk_range, chunk_color)) else Iterator( Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++ markup.iterator ++ Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color)) var x1 = x + w gfx.setFont(chunk_font) for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) { val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset) gfx.setColor(color) range.try_restrict(caret_range) match { case Some(r) if !r.is_singularity => val i = r.start - range.start val j = r.stop - range.start val s1 = str.substring(0, i) 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) } } w += chunk.width chunk = chunk.next.asInstanceOf[Chunk] } w } private val text_painter = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { robust_rendering { rendering => val painter = text_area.getPainter val fm = painter.getFontMetrics val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext) val clip = gfx.getClip val x0 = text_area.getHorizontalOffset var y0 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent val (bullet_x, bullet_y, bullet_w, bullet_h) = { val w = fm.charWidth(' ') val b = (w / 2) max 1 val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt ((w - b + 1) / 2, c - b / 2, w - b, line_height - b) } for (i <- 0 until physical_lines.length) { val line = physical_lines(i) if (line != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) // text chunks val screen_line = first_line + i val chunks = text_area.getChunksOfScreenLine(screen_line) if (chunks != null) { try { val line_start = buffer.getLineStartOffset(line) gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height) val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) orig_text_painter.paintValidLine(gfx, screen_line, line, start(i), end(i), y + line_height * i) } finally { gfx.setClip(clip) } } // bullet bar for { Text.Info(range, color) <- rendering.bullet(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y, r.length - bullet_w, line_height - bullet_h) } } y0 += line_height } } } } /* foreground */ private val foreground_painter = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { robust_rendering { rendering => val search_pattern = get_search_pattern() for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) // foreground color for { Text.Info(range, color) <- rendering.foreground(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } // search pattern for { regex <- search_pattern text <- JEdit_Lib.try_get_text(buffer, line_range) m <- regex.findAllMatchIn(text) range = Text.Range(m.start, m.end) + line_range.start r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.search_color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } // highlight range -- potentially from other snapshot for { info <- highlight_area.info Text.Info(range, color) <- info.try_restrict(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } // hyperlink range -- potentially from other snapshot for { info <- hyperlink_area.info Text.Info(range, _) <- info.try_restrict(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.hyperlink_color) gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) } // completion range if (!hyperlink_area.is_active && caret_visible) { for { completion <- Completion_Popup.Text_Area(text_area) Text.Info(range, color) <- completion.rendering(rendering, line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) } } } } } } } /* caret -- outside of text range */ private class Caret_Painter(before: Boolean) extends TextAreaExtension { override def paintValidLine(gfx: Graphics2D, screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) { robust_rendering { _ => if (before) gfx.clipRect(0, 0, 0, 0) else gfx.setClip(painter_clip) } } } private val before_caret_painter1 = new Caret_Painter(true) private val after_caret_painter1 = new Caret_Painter(false) private val before_caret_painter2 = new Caret_Painter(true) private val after_caret_painter2 = new Caret_Painter(false) private val caret_painter = new TextAreaExtension { override def paintValidLine(gfx: Graphics2D, screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) { robust_rendering { rendering => if (caret_visible) { val caret = text_area.getCaretPosition if (caret_enabled && start <= caret && caret == end - 1) { val painter = text_area.getPainter val fm = painter.getFontMetrics val offset = caret - text_area.getLineStartOffset(physical_line) val x = text_area.offsetToXY(physical_line, offset).x val y1 = y + painter.getLineHeight - (fm.getLeading + 1) - fm.getDescent val astr = new AttributedString(" ") astr.addAttribute(TextAttribute.FONT, painter.getFont) astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret)) astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) val clip = gfx.getClip try { gfx.clipRect(x, y, Integer.MAX_VALUE, painter.getLineHeight) gfx.drawString(astr.getIterator, x, y1) } finally { gfx.setClip(clip) } } } } } } /* activation */ def activate() { val painter = text_area.getPainter painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state) painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter) painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1) painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) painter.addExtension(500, foreground_painter) painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) painter.removeExtension(orig_text_painter) painter.addMouseListener(mouse_listener) painter.addMouseMotionListener(mouse_motion_listener) text_area.addFocusListener(focus_listener) view.addWindowListener(window_listener) } def deactivate() { active_reset() val painter = text_area.getPainter view.removeWindowListener(window_listener) text_area.removeFocusListener(focus_listener) painter.removeMouseMotionListener(mouse_motion_listener) painter.removeMouseListener(mouse_listener) painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) painter.removeExtension(reset_state) painter.removeExtension(foreground_painter) painter.removeExtension(caret_painter) painter.removeExtension(after_caret_painter2) painter.removeExtension(before_caret_painter2) painter.removeExtension(after_caret_painter1) painter.removeExtension(before_caret_painter1) painter.removeExtension(text_painter) painter.removeExtension(background_painter) painter.removeExtension(set_state) } }