diff --git a/src/Tools/jEdit/src/fold_handling.scala b/src/Tools/jEdit/src/fold_handling.scala --- a/src/Tools/jEdit/src/fold_handling.scala +++ b/src/Tools/jEdit/src/fold_handling.scala @@ -1,81 +1,80 @@ /* Title: Tools/jEdit/src/fold_handling.scala Author: Makarius Handling of folds within the text structure. */ package isabelle.jedit import isabelle._ import javax.swing.text.Segment -import scala.collection.convert.WrapAsJava +import scala.collection.JavaConverters import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler} object Fold_Handling { /* input: dynamic line context */ class Fold_Handler extends FoldHandler("isabelle") { override def equals(other: Any): Boolean = other match { case that: Fold_Handler => true case _ => false } override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = Token_Markup.Line_Context.after(buffer, line).structure.depth max 0 override def getPrecedingFoldLevels( buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] = { val structure = Token_Markup.Line_Context.after(buffer, line).structure val result = if (line > 0 && structure.command) Range.inclusive(line - 1, 0, -1).iterator. map(i => Token_Markup.Line_Context.after(buffer, i).structure). takeWhile(_.improper).map(_ => structure.depth max 0).toList else Nil if (result.isEmpty) null - else WrapAsJava.seqAsJavaList(result.map(Integer.valueOf)) + else JavaConverters.seqAsJavaList(result.map(Integer.valueOf)) } } /* output: static document rendering */ class Document_Fold_Handler(private val rendering: JEdit_Rendering) extends FoldHandler("isabelle-document") { override def equals(other: Any): Boolean = other match { case that: Document_Fold_Handler => this.rendering == that.rendering case _ => false } override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = { def depth(i: Text.Offset): Int = if (i < 0) 0 else { rendering.fold_depth(Text.Range(i, i + 1)) match { case Text.Info(_, d) :: _ => d case _ => 0 } } if (line <= 0) 0 else { val range = JEdit_Lib.line_range(buffer, line - 1) buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1) } } } } - diff --git a/src/Tools/jEdit/src/keymap_merge.scala b/src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala +++ b/src/Tools/jEdit/src/keymap_merge.scala @@ -1,259 +1,259 @@ /* Title: Tools/jEdit/src/keymap_merge.scala Author: Makarius Merge of Isabelle shortcuts vs. jEdit keymap. */ package isabelle.jedit import isabelle._ -import java.lang.Class import java.awt.{Color, Dimension, BorderLayout} import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane} import javax.swing.table.AbstractTableModel import scala.collection.JavaConverters -import org.gjt.sp.jedit.{jEdit, View, GUIUtilities} +import org.gjt.sp.jedit.{jEdit, View} +import org.gjt.sp.util.GenericGUIUtilities import org.jedit.keymap.{KeymapManager, Keymap} object Keymap_Merge { /** shortcuts **/ private def is_shortcut(property: String): Boolean = (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && !property.startsWith("options.shortcuts.") class Shortcut(val property: String, val binding: String) { override def toString: String = property + "=" + binding def primary: Boolean = property.endsWith(".shortcut") val action: String = Library.try_unsuffix(".shortcut", property) orElse Library.try_unsuffix(".shortcut2", property) getOrElse error("Bad shortcut property: " + quote(property)) val label: String = - GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) + GenericGUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) /* ignore wrt. keymap */ private def prop_ignore: String = property + ".ignore" def ignored_keymaps(): List[String] = space_explode(',', jEdit.getProperty(prop_ignore, "")) def is_ignored(keymap_name: String): Boolean = ignored_keymaps().contains(keymap_name) def ignore(keymap_name: String): Unit = jEdit.setProperty(prop_ignore, Library.insert(keymap_name)(ignored_keymaps()).sorted.mkString(",")) def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding) def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null) } /* content wrt. keymap */ def convert_properties(props: java.util.Properties): List[Shortcut] = if (props == null) Nil else { var result = List.empty[Shortcut] for (entry <- JavaConverters.mapAsScalaMap(props)) { entry match { case (a: String, b: String) if is_shortcut(a) => result ::= new Shortcut(a, b) case _ => } } result.sortBy(_.property) } def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] = { val keymap_shortcuts = if (keymap == null) Nil else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield { val conflicts = keymap_shortcuts.filter(s1 => s.property == s1.property && s.binding != s1.binding || s.property != s1.property && s.binding == s1.binding && s1.binding != "") (s, conflicts) } } /** table **/ private def conflict_color: Color = PIDE.options.color_value("error_color") private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) { override def toString: String = if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" else "" + HTML.output("--- " + shortcut.toString) + "" } private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel { private val entries_count = entries.length private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count private def get_entry(row: Int): Option[Table_Entry] = if (has_entry(row)) Some(entries(row)) else None private val selected = Synchronized[Set[Int]]( (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet) private def is_selected(row: Int): Boolean = selected.value.contains(row) private def select(head: Int, tail: List[Int], b: Boolean): Unit = selected.change(set => if (b) set + head -- tail else set - head ++ tail) def apply(keymap_name: String, keymap: Keymap) { GUI_Thread.require {} for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { val b = is_selected(row) if (b) { entry.tail.foreach(i => entries(i).shortcut.reset(keymap)) entry.shortcut.set(keymap) } else entry.shortcut.ignore(keymap_name) } } override def getColumnCount: Int = 2 override def getColumnClass(i: Int): Class[_ <: Object] = if (i == 0) classOf[java.lang.Boolean] else classOf[Object] override def getColumnName(i: Int): String = if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" override def getRowCount: Int = entries_count override def getValueAt(row: Int, column: Int): AnyRef = { get_entry(row) match { case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row)) case Some(entry) if column == 1 => entry case _ => null } } override def isCellEditable(row: Int, column: Int): Boolean = has_entry(row) && column == 0 override def setValueAt(value: AnyRef, row: Int, column: Int) { value match { case obj: java.lang.Boolean if has_entry(row) && column == 0 => val b = obj.booleanValue val entry = entries(row) entry.head match { case None => select(row, entry.tail, b) case Some(head_row) => val head_entry = entries(head_row) select(head_row, head_entry.tail, !b) } GUI_Thread.later { fireTableDataChanged() } case _ => } } } private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) { - private val cell_size = GUIUtilities.defaultTableCellSize() + private val cell_size = GenericGUIUtilities.defaultTableCellSize() private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) val table = new JTable(table_model) table.setShowGrid(false) table.setIntercellSpacing(new Dimension(0, 0)) table.setRowHeight(cell_size.height + 2) table.setPreferredScrollableViewportSize(table_size) table.setFillsViewportHeight(true) table.getTableHeader.setReorderingAllowed(false) table.getColumnModel.getColumn(0).setPreferredWidth(30) table.getColumnModel.getColumn(0).setMinWidth(30) table.getColumnModel.getColumn(0).setMaxWidth(30) table.getColumnModel.getColumn(0).setResizable(false) table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30) val scroller = new JScrollPane(table) scroller.getViewport.setBackground(table.getBackground) scroller.setPreferredSize(table_size) add(scroller, BorderLayout.CENTER) } /** check with optional dialog **/ def check_dialog(view: View) { GUI_Thread.require {} val keymap_manager = jEdit.getKeymapManager val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) val keymap = keymap_manager.getKeymap(keymap_name) match { case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) case keymap => keymap } val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap) val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty) val table_entries = for { ((shortcut, conflicts), i) <- shortcut_conflicts zip shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length }) entry <- Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: conflicts.map(Table_Entry(_, Some(i), Nil)) } yield entry val table_model = new Table_Model(table_entries) if (table_entries.nonEmpty && GUI.confirm_dialog(view, "Pending Isabelle/jEdit keymap changes", JOptionPane.OK_CANCEL_OPTION, "The following Isabelle keymap changes are in conflict with the current", "jEdit keymap " + quote(keymap_name) + ":", new Table(table_model), "Selected shortcuts will be applied, unselected changes will be ignored.", "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0) { table_model.apply(keymap_name, keymap) } no_shortcut_conflicts.foreach(_.set(keymap)) keymap.save() jEdit.saveSettings() jEdit.propertiesChanged() } } 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,697 +1,697 @@ /* 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: () => JEdit_Rendering, close_action: () => Unit, get_search_pattern: () => Option[Regex], caret_update: () => Unit, caret_visible: Boolean, enable_hovering: Boolean) { private val buffer = text_area.getBuffer /* robust extension body */ def check_robust_body: Boolean = GUI_Thread.require { buffer == text_area.getBuffer } def robust_body[A](default: A)(body: => A): A = { try { if (check_robust_body) 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: JEdit_Rendering = null @volatile private var painter_clip: Shape = null @volatile private var caret_focus: Set[Long] = Set.empty 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 caret_focus = JEdit_Lib.visible_range(text_area) match { case Some(visible_range) if caret_enabled && !painter_rendering.snapshot.is_outdated => painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range) case _ => Set.empty[Long] } } } 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 caret_focus = Set.empty } } def robust_rendering(body: JEdit_Rendering => Unit) { robust_body(()) { body(painter_rendering) } } /* active areas within the text */ private class Active_Area[A]( rendering: JEdit_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) { caret_update() 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: JEdit_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: JEdit_Rendering) => rendering.highlight, None) private val hyperlink_area = new Active_Area[PIDE.editor.Hyperlink]( (rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR)) private val active_area = new Active_Area[XML.Elem]( (rendering: JEdit_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 def area_active(): Boolean = active_areas.exists({ case (area, _) => area.is_active }) 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 + val control = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 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) => rendering.tooltip(range, control) match { case None => case Some(tip) => val painter = text_area.getPainter val loc = new Point(x, y + painter.getLineHeight / 2) val results = snapshot.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 <- physical_lines.indices) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) // line background color for { (c, separator) <- rendering.line_background(line_range) } { gfx.setColor(rendering.color(c)) 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, c) <- rendering.background(Rendering.background_elements, line_range, caret_focus) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.color(c)) 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, c) <- rendering.squiggly_underline(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.color(c)) 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.plugin.spell_checker.get spell <- rendering.spell_checker(line_range) text <- JEdit_Lib.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: JEdit_Rendering, offset: Text.Offset): Color = { if (text_area.isCaretVisible) text_area.getPainter.getCaretColor else { val debug_positions = (for { c <- PIDE.session.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: JEdit_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(Word.bidi_override(s1), x1, y) 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(Word.bidi_override(s3), x1 + string_width(str.substring(0, j)), y) case _ => 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 <- physical_lines.indices) { 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 <- physical_lines.indices) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) // foreground color for { Text.Info(range, c) <- rendering.foreground(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.color(c)) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } // search pattern for { regex <- search_pattern text <- JEdit_Lib.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) } // entity def range if (!area_active() && caret_visible) { for { Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) 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) } } // completion range if (!area_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) } } diff --git a/src/Tools/jEdit/src/token_markup.scala b/src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala +++ b/src/Tools/jEdit/src/token_markup.scala @@ -1,314 +1,314 @@ /* Title: Tools/jEdit/src/token_markup.scala Author: Makarius Outer syntax token markup. */ package isabelle.jedit import isabelle._ import javax.swing.text.Segment -import scala.collection.convert.WrapAsJava +import scala.collection.JavaConverters import org.gjt.sp.jedit.{Mode, Buffer} import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler, ParserRuleSet, ModeProvider, XModeHandler} import org.gjt.sp.jedit.indent.IndentRule import org.gjt.sp.jedit.buffer.JEditBuffer object Token_Markup { /* line context */ object Line_Context { def init(mode: String): Line_Context = new Line_Context(mode, Some(Scan.Finished), Line_Structure.init) def before(buffer: JEditBuffer, line: Int): Line_Context = if (line == 0) init(JEdit_Lib.buffer_mode(buffer)) else after(buffer, line - 1) def after(buffer: JEditBuffer, line: Int): Line_Context = { val line_mgr = JEdit_Lib.buffer_line_manager(buffer) def context = line_mgr.getLineContext(line) match { case c: Line_Context => Some(c) case _ => None } context getOrElse { buffer.markTokens(line, DummyTokenHandler.INSTANCE) context getOrElse init(JEdit_Lib.buffer_mode(buffer)) } } } class Line_Context( val mode: String, val context: Option[Scan.Line_Context], val structure: Line_Structure) extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null) { def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished) override def hashCode: Int = (mode, context, structure).hashCode override def equals(that: Any): Boolean = that match { case other: Line_Context => mode == other.mode && context == other.context && structure == other.structure case _ => false } } /* tokens from line (inclusive) */ private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int) : Option[List[Token]] = { val line_context = Line_Context.before(buffer, line) for { ctxt <- line_context.context text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line)) } yield Token.explode_line(syntax.keywords, text, ctxt)._1 } def line_token_iterator( syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int, end_line: Int): Iterator[Text.Info[Token]] = for { line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator tokens <- try_line_tokens(syntax, buffer, line).iterator starts = tokens.iterator.scanLeft(buffer.getLineStartOffset(line))( (i, tok) => i + tok.source.length) (i, tok) <- starts zip tokens.iterator } yield Text.Info(Text.Range(i, i + tok.source.length), tok) def line_token_reverse_iterator( syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int, end_line: Int): Iterator[Text.Info[Token]] = for { line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator tokens <- try_line_tokens(syntax, buffer, line).iterator stops = tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)( (i, tok) => i - tok.source.length) (i, tok) <- stops zip tokens.reverseIterator } yield Text.Info(Text.Range(i - tok.source.length, i), tok) /* tokens from offset (inclusive) */ def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset): Iterator[Text.Info[Token]] = if (JEdit_Lib.buffer_range(buffer).contains(offset)) line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount). dropWhile(info => !info.range.contains(offset)) else Iterator.empty def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset): Iterator[Text.Info[Token]] = if (JEdit_Lib.buffer_range(buffer).contains(offset)) line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1). dropWhile(info => !info.range.contains(offset)) else Iterator.empty /* command spans */ def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Option[Text.Info[Command_Span.Span]] = { val keywords = syntax.keywords def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] = token_reverse_iterator(syntax, buffer, i). find(info => keywords.is_before_command(info.info) || info.info.is_command) def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] = token_iterator(syntax, buffer, i). find(info => keywords.is_before_command(info.info) || info.info.is_command) if (JEdit_Lib.buffer_range(buffer).contains(offset)) { val start_info = { val info1 = maybe_command_start(offset) info1 match { case Some(Text.Info(range1, tok1)) if tok1.is_command => val info2 = maybe_command_start(range1.start - 1) info2 match { case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2 case _ => info1 } case _ => info1 } } val (start_before_command, start, start_next) = start_info match { case Some(Text.Info(range, tok)) => (keywords.is_before_command(tok), range.start, range.stop) case None => (false, 0, 0) } val stop_info = { val info1 = maybe_command_stop(start_next) info1 match { case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command => maybe_command_stop(range1.stop) case _ => info1 } } val stop = stop_info match { case Some(Text.Info(range, _)) => range.start case None => buffer.getLength } val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("") val spans = syntax.parse_spans(text) (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator). map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }). find(_.range.contains(offset)) } else None } private def _command_span_iterator( syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset, next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] = new Iterator[Text.Info[Command_Span.Span]] { private var next_span = command_span(syntax, buffer, offset) def hasNext: Boolean = next_span.isDefined def next: Text.Info[Command_Span.Span] = { val span = next_span.getOrElse(Iterator.empty.next) next_span = command_span(syntax, buffer, next_offset(span.range)) span } } def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Iterator[Text.Info[Command_Span.Span]] = _command_span_iterator(syntax, buffer, offset max 0, range => range.stop) def command_span_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Iterator[Text.Info[Command_Span.Span]] = _command_span_iterator(syntax, buffer, (offset min buffer.getLength) - 1, range => range.start - 1) /* token marker */ class Marker( protected val mode: String, protected val opt_buffer: Option[Buffer]) extends TokenMarker { override def hashCode: Int = (mode, opt_buffer).hashCode override def equals(that: Any): Boolean = that match { case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer case _ => false } override def toString: String = opt_buffer match { case None => "Marker(" + mode + ")" case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")" } override def markTokens(context: TokenMarker.LineContext, handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = { val line = if (raw_line == null) new Segment else raw_line val line_context = context match { case c: Line_Context => c case _ => Line_Context.init(mode) } val structure = line_context.structure val context1 = { val opt_syntax = opt_buffer match { case Some(buffer) => Isabelle.buffer_syntax(buffer) case None => Isabelle.mode_syntax(mode) } val (styled_tokens, context1) = (line_context.context, opt_syntax) match { case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" => val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt) val styled_tokens = tokens.map(tok => (JEdit_Rendering.ml_token_markup(tok), tok.source)) (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure)) case (Some(ctxt), Some(syntax)) if syntax.has_tokens => val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt) val structure1 = structure.update(syntax.keywords, tokens) val styled_tokens = tokens.map(tok => (JEdit_Rendering.token_markup(syntax, tok), tok.source)) (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1)) case _ => val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) (List(styled_token), new Line_Context(line_context.mode, None, structure)) } val extended = Syntax_Style.extended(line) var offset = 0 for ((style, token) <- styled_tokens) { val length = token.length val offsets = offset until (offset + length) if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) { for (i <- offsets) { val style1 = extended.get(i) match { case None => style case Some(ext) => ext(style) } handler.handleToken(line, style1, i, 1, context1) } } else handler.handleToken(line, style, offset, length, context1) offset += length } handler.handleToken(line, JEditToken.END, line.count, 0, context1) context1 } val context2 = context1.intern handler.setLineContext(context2) context2 } } /* mode provider */ class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider { for (mode <- orig_provider.getModes) addMode(mode) override def loadMode(mode: Mode, xmh: XModeHandler) { super.loadMode(mode, xmh) Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _) Isabelle.indent_rule(mode.getName).foreach(indent_rule => Untyped.set[java.util.List[IndentRule]]( - mode, "indentRules", WrapAsJava.seqAsJavaList(List(indent_rule)))) + mode, "indentRules", JavaConverters.seqAsJavaList(List(indent_rule)))) } } }