# HG changeset patch # User wenzelm # Date 1607979714 -3600 # Node ID 69f768aff611cc4eb5ca1eae467f7d9e3def84ea # Parent 71618a89a4e9a25546681aa9541ab5cdaef03a62 clarified caret focus modifier, depending on option "jedit_focus_modifier"; diff -r 71618a89a4e9 -r 69f768aff611 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Dec 14 16:51:12 2020 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Dec 14 22:01:54 2020 +0100 @@ -178,6 +178,13 @@ val empty: Focus = apply(Set.empty) def make(args: List[Text.Info[Focus]]): Focus = (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }) + + val full: Focus = + new Focus(Set.empty) + { + override def apply(id: Long): Boolean = true + override def toString: String = "Focus.full" + } } sealed class Focus private[Rendering](protected val rep: Set[Long]) @@ -504,30 +511,36 @@ case _ => None })) - def entity_focus(range: Text.Range, visible_defs: Rendering.Focus): Rendering.Focus = + def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus = Rendering.Focus.make( snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ => { case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _))) - if visible_defs(i) => Some(focus + i) + if defs_focus(i) => Some(focus + i) case _ => None })) /* caret focus */ - def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus = + def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus = { val focus = entity_focus_defs(caret_range) if (focus.defined) focus - else entity_focus(caret_range, entity_focus_defs(visible_range)) + else if (defs_range == Text.Range.offside) Rendering.Focus.empty + else { + val defs_focus = + if (defs_range == Text.Range.full) Rendering.Focus.full + else entity_focus_defs(defs_range) + entity_focus(caret_range, defs_focus) + } } - def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] = + def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] = { - val focus = caret_focus(caret_range, visible_range) + val focus = caret_focus(caret_range, defs_range) if (focus.defined) { - snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ => + snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ => { case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true) case _ => None diff -r 71618a89a4e9 -r 69f768aff611 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Mon Dec 14 16:51:12 2020 +0100 +++ b/src/Tools/jEdit/etc/options Mon Dec 14 22:01:54 2020 +0100 @@ -39,6 +39,9 @@ public option jedit_text_overview : bool = true -- "paint text overview column" +public option jedit_focus_modifier : string = "CS" + -- "keyboard modifier to enable entity focus regardless of def visibility" + public option isabelle_fonts_hinted : bool = true -- "use hinted Isabelle DejaVu fonts (change requires restart)" diff -r 71618a89a4e9 -r 69f768aff611 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 14 16:51:12 2020 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Dec 14 22:01:54 2020 +0100 @@ -359,8 +359,7 @@ for (doc_view <- Document_View.get(text_area)) { val rendering = doc_view.get_rendering() val caret_range = JEdit_Lib.caret_range(text_area) - val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer) - val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range) + val active_focus = rendering.caret_focus_ranges(caret_range, Text.Range.full) if (active_focus.nonEmpty) { text_area.selectNone() for (r <- active_focus) diff -r 71618a89a4e9 -r 69f768aff611 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 14 16:51:12 2020 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 14 22:01:54 2020 +0100 @@ -17,8 +17,8 @@ import scala.util.parsing.input.CharSequenceReader import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} -import org.gjt.sp.jedit.gui.KeyEventWorkaround +import org.gjt.sp.jedit.io.{FileVFS, VFSManager} +import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator} import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} @@ -400,4 +400,10 @@ def shift_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0 + + def modifier_string(evt: InputEvent): String = + KeyEventTranslator.getModifierString(evt) match { + case null => "" + case s => s + } } diff -r 71618a89a4e9 -r 69f768aff611 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Mon Dec 14 16:51:12 2020 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Dec 14 22:01:54 2020 +0100 @@ -10,9 +10,9 @@ import isabelle._ -import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo} +import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo} import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, - FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} + FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent} import java.awt.font.TextAttribute import javax.swing.SwingUtilities import java.text.AttributedString @@ -71,6 +71,32 @@ pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") + /* caret focus modifier */ + + @volatile private var caret_focus_modifier = false + + def caret_focus_range: Text.Range = + if (caret_focus_modifier) Text.Range.full + else JEdit_Lib.visible_range(text_area) getOrElse Text.Range.offside + + private val key_listener = + JEdit_Lib.key_listener( + key_pressed = (evt: KeyEvent) => + { + val mod = PIDE.options.string("jedit_focus_modifier") + val old = caret_focus_modifier + caret_focus_modifier = (mod.nonEmpty && mod == JEdit_Lib.modifier_string(evt)) + if (caret_focus_modifier != old) caret_update() + }, + key_released = _ => + { + if (caret_focus_modifier) { + caret_focus_modifier = false + caret_update() + } + }) + + /* common painter state */ @volatile private var painter_rendering: JEdit_Rendering = null @@ -86,11 +112,10 @@ 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 _ => Rendering.Focus.empty + if (caret_enabled && !painter_rendering.snapshot.is_outdated) { + painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), caret_focus_range) } + else Rendering.Focus.empty } } @@ -674,6 +699,7 @@ painter.removeExtension(orig_text_painter) painter.addMouseListener(mouse_listener) painter.addMouseMotionListener(mouse_motion_listener) + text_area.addKeyListener(key_listener) text_area.addFocusListener(focus_listener) view.addWindowListener(window_listener) } @@ -684,6 +710,7 @@ val painter = text_area.getPainter view.removeWindowListener(window_listener) text_area.removeFocusListener(focus_listener) + text_area.removeKeyListener(key_listener) painter.removeMouseMotionListener(mouse_motion_listener) painter.removeMouseListener(mouse_listener) painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)