--- a/NEWS Thu Aug 21 15:13:00 2025 +0200
+++ b/NEWS Thu Aug 21 21:33:34 2025 +0200
@@ -35,6 +35,9 @@
"show_results" (default true) and "show_states" (default false),
provided at build-time for the underlying session database.
+* For pretty-printed output a margin <= 0 means there is no margin to be
+observed: only forced breaks are taken.
+
*** Isabelle/jEdit Prover IDE ***
--- a/src/Pure/GUI/gui.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Pure/GUI/gui.scala Thu Aug 21 21:33:34 2025 +0200
@@ -12,10 +12,11 @@
import java.awt.event.{KeyAdapter, KeyEvent}
import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JButton, JLabel, JLayeredPane, JOptionPane,
+import javax.swing.{Icon, ImageIcon, JButton, JLabel, JLayeredPane, JOptionPane,
RootPaneContainer, JTextField, JComboBox, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Separator}
+import scala.swing.{Alignment, CheckBox, ComboBox, ScrollPane, TextArea, ListView, Separator}
+import scala.swing.Swing.EmptyIcon
import scala.swing.event.{ButtonClicked, SelectionChanged}
import com.formdev.flatlaf
@@ -228,6 +229,33 @@
}
+ /* label for other component */
+
+ class Label(
+ label_text: String,
+ label_icon: Icon,
+ label_align: Alignment.Value,
+ label_for: java.awt.Component
+ ) extends scala.swing.Label(label_text, label_icon, label_align) {
+
+ override lazy val peer: JLabel =
+ new JLabel(label_text, if (label_icon == EmptyIcon) null else label_icon, label_align.id)
+ with SuperMixin { labelFor = label_for }
+
+ override def this(label_text: String, label_icon: Icon, label_align: Alignment.Value) =
+ this(label_text, label_icon, label_align, null)
+
+ def this(label_text: String, label_for: java.awt.Component) =
+ this(label_text, EmptyIcon, Alignment.Center, label_for)
+
+ def this(label_text: String, label_for: scala.swing.Component) =
+ this(label_text, EmptyIcon, Alignment.Center, label_for.peer)
+
+ def this(label_text: String) =
+ this(label_text, EmptyIcon, Alignment.Center)
+ }
+
+
/* list selector */
object Selector {
--- a/src/Pure/GUI/tree_view.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Pure/GUI/tree_view.scala Thu Aug 21 21:33:34 2025 +0200
@@ -48,6 +48,7 @@
val root: Tree_View.Node = Tree_View.Node(),
single_selection_mode: Boolean = false
) extends JTree(root) {
+ getAccessibleContext.setAccessibleName(root.toString)
def get_selection[A](which: PartialFunction[AnyRef, A]): Option[A] =
getLastSelectedPathComponent match {
case Tree_View.Node(obj) if obj != null && which.isDefinedAt(obj) => Some(which(obj))
--- a/src/Pure/General/pretty.ML Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Pure/General/pretty.ML Thu Aug 21 21:33:34 2025 +0200
@@ -416,8 +416,11 @@
fun format_tree (ops: output_ops) input =
let
val margin = #margin ops;
- val breakgain = margin div 20; (*minimum added space required of a break*)
- val emergencypos = margin div 2; (*position too far to right*)
+ val margin_defined = margin > 0;
+ val margin1 = if margin_defined then margin else ML_Pretty.default_margin;
+
+ val breakgain = margin1 div 20; (*minimum added space required of a break*)
+ val emergencypos = Int.max (margin1 div 2, 1); (*position too far to right*)
fun blanks_state n state = add_state (#1 (output_spaces ops n)) state;
val blanks = string o output_spaces ops;
@@ -457,12 +460,13 @@
val pos' = pos + indent;
val pos'' = pos' mod emergencypos;
val before' =
- if pos' < emergencypos
+ if not margin_defined orelse pos' < emergencypos
then (Option.map (close_state o blanks_state indent) (#line text), pos')
else (Option.map (fn _ => blanks_state pos'' init_state) (#line text), pos'');
val after' = break_dist (ts, after)
val body' = body
- |> (consistent andalso pos + blen > margin - after') ? map force_break;
+ |> (margin_defined andalso consistent andalso pos + blen > margin - after') ?
+ map force_break;
val btext: text =
text |> push markup |> format (body' @ [End], before', after');
(*if this block was broken then force the next break*)
@@ -473,7 +477,8 @@
or if breaking would add only breakgain to space*)
format (ts, before, after)
(if not force andalso
- pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain)
+ (not margin_defined orelse
+ pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain))
then text |> blanks wd (*just insert wd blanks*)
else text |> break before |> blanks ind)
| Str str :: ts => format (ts, before, after) (string str text));
--- a/src/Pure/General/pretty.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Pure/General/pretty.scala Thu Aug 21 21:33:34 2025 +0200
@@ -223,7 +223,9 @@
breakgain: Double = default_breakgain,
metric: Metric = Codepoint.Metric
): XML.Body = {
- val emergencypos = (margin / 2).round.toInt
+ val margin_defined = margin > 0
+ val margin1 = if (margin_defined) margin else default_margin
+ val emergencypos = ((margin1 / 2) max 1).round.toInt
def make_tree(inp: XML.Body): List[Tree] =
inp flatMap {
@@ -254,10 +256,12 @@
case (block: Block) :: ts =>
val pos1 = text.pos + block.indent
val pos2 = (pos1.round.toInt % emergencypos).toDouble
- val before1 = if (pos1 < emergencypos) pos1 else pos2
+ val before1 = if (!margin_defined || pos1 < emergencypos) pos1 else pos2
val after1 = break_dist(ts, after)
val body1 =
- if (block.consistent && text.pos + block.length > margin - after1) force_all(block.body)
+ if (margin_defined && block.consistent && text.pos + block.length > margin - after1) {
+ force_all(block.body)
+ }
else block.body
val btext1 =
if (block.markup == no_markup) format(body1, before1, after1, text)
@@ -270,8 +274,10 @@
format(ts1, before, after, btext1)
case Break(force, wd, ind) :: ts =>
if (!force &&
- text.pos + wd <= ((margin - break_dist(ts, after)) max (before + breakgain)))
+ (!margin_defined ||
+ text.pos + wd <= ((margin - break_dist(ts, after)) max (before + breakgain)))) {
format(ts, before, after, text.blanks(wd))
+ }
else format(ts, before, after, text.newline.blanks((before + ind).ceil.toInt))
case Str(s, len) :: ts => format(ts, before, after, text.string(s, len))
}
--- a/src/Tools/Graphview/tree_panel.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Thu Aug 21 21:33:34 2025 +0200
@@ -91,14 +91,11 @@
case Some(re) => re.findFirstIn(node.toString).isDefined
}
- private val selection_label = new Label("Selection:") {
- tooltip = "Selection of nodes via regular expression"
- }
-
- private val selection_field = new TextField(10) {
- tooltip = selection_label.tooltip
- }
+ private val selection_tooltip = "Selection of nodes via regular expression"
+ private val selection_field = new TextField(10) { tooltip = selection_tooltip }
private val selection_field_foreground = selection_field.foreground
+ private val selection_label =
+ new GUI.Label("Selection:", selection_field) { tooltip = selection_tooltip }
private val selection_delay =
Delay.last(graphview.options.seconds("editor_input_delay"), gui = true) {
--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Aug 21 21:33:34 2025 +0200
@@ -15,7 +15,7 @@
import javax.swing.event.TreeSelectionEvent
import scala.collection.immutable.SortedMap
-import scala.swing.{Label, Component}
+import scala.swing.Component
import org.gjt.sp.jedit.{jEdit, View}
import org.gjt.sp.jedit.menu.EnhancedMenuItem
@@ -182,9 +182,7 @@
override def clicked(): Unit = thread_selection().foreach(debugger.step_out)
}
- private val context_label = new Label("Context:") {
- tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
- }
+ private val context_tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
private val context_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-context") {
override def processKeyEvent(evt: KeyEvent): Unit = {
@@ -194,13 +192,14 @@
super.processKeyEvent(evt)
}
setColumns(20)
- setToolTipText(context_label.tooltip)
+ setToolTipText(context_tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
+ private val context_label = new GUI.Label("Context:", context_field) {
+ tooltip = context_tooltip
+ }
- private val expression_label = new Label("ML:") {
- tooltip = "Isabelle/ML or Standard ML expression"
- }
+ private val expression_tooltip = "Isabelle/ML or Standard ML expression"
private val expression_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-expression") {
override def processKeyEvent(evt: KeyEvent): Unit = {
@@ -211,9 +210,12 @@
}
{ val max = getPreferredSize; max.width = Int.MaxValue; setMaximumSize(max) }
setColumns(40)
- setToolTipText(expression_label.tooltip)
+ setToolTipText(expression_tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
+ private val expression_label = new GUI.Label("ML:", expression_field) {
+ tooltip = expression_tooltip
+ }
private val eval_button =
new GUI.Button(GUI.Style_HTML.enclose_bold("Eval")) {
--- a/src/Tools/jEdit/src/documentation_dockable.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Thu Aug 21 21:33:34 2025 +0200
@@ -20,6 +20,7 @@
private val doc_contents = Doc.contents(PIDE.ml_settings)
private val tree = new Tree_View(single_selection_mode = true)
+ tree.getAccessibleContext.setAccessibleName("Documentation")
for (section <- doc_contents.sections) {
tree.root.add(Tree_View.Node(section.title))
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Aug 21 21:33:34 2025 +0200
@@ -16,7 +16,7 @@
import javax.swing.JTextField
import javax.swing.event.{DocumentListener, DocumentEvent}
-import scala.swing.{Label, Component}
+import scala.swing.Component
import scala.util.matching.Regex
import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
@@ -266,9 +266,7 @@
/* search */
- private val search_label: Component = new Label(jEdit.getProperty("view.search.find")) {
- tooltip = "Search and highlight output via regular expression"
- }
+ private val search_tooltip = "Search and highlight output via regular expression"
private val search_field: Component =
Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") {
@@ -280,12 +278,17 @@
def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
})
setColumns(20)
- setToolTipText(search_label.tooltip)
+ setToolTipText(search_tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
})
private val search_field_foreground = search_field.foreground
+ private val search_label: Component =
+ new GUI.Label(jEdit.getProperty("view.search.find"), label_for = search_field) {
+ tooltip = search_tooltip
+ }
+
private def search_action(text_field: JTextField): Unit = {
val (pattern, ok) =
text_field.getText match {
--- a/src/Tools/jEdit/src/query_dockable.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu Aug 21 21:33:34 2025 +0200
@@ -84,14 +84,15 @@
query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
}
- private val query_label = new Label("Find:") {
- tooltip =
- GUI.tooltip_lines(
- "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
- }
+ private val query_tooltip =
+ GUI.tooltip_lines(
+ "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
val query: Completion_Popup.History_Text_Field =
- make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
+ make_query("isabelle-find-theorems", query_tooltip, apply_query _)
+
+ private val query_label =
+ new GUI.Label("Find:", query) { tooltip = query_tooltip }
/* GUI page */
--- a/src/Tools/jEdit/src/session_build.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Thu Aug 21 21:33:34 2025 +0200
@@ -38,7 +38,7 @@
text.editable = false
text.columns = 60
text.rows = 24
- text.font = GUI.copy_font((new Label).font)
+ text.font = GUI.copy_font(GUI.label_font())
text.caret.color = text.background
private val scroll_text = new ScrollPane(text)
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Aug 21 21:33:34 2025 +0200
@@ -63,21 +63,20 @@
List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))
}
- private val provers_label = new Label("Provers:") {
- tooltip =
- GUI.tooltip_lines(
- "Automatic provers as space-separated list, e.g.\n" +
- PIDE.options.value.check_name("sledgehammer_provers").default_value)
- }
-
+ private val provers_tooltip =
+ GUI.tooltip_lines(
+ "Automatic provers as space-separated list, e.g.\n" +
+ PIDE.options.value.check_name("sledgehammer_provers").default_value)
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
override def processKeyEvent(evt: KeyEvent): Unit = {
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) hammer()
super.processKeyEvent(evt)
}
- setToolTipText(provers_label.tooltip)
+ setToolTipText(provers_tooltip)
setColumns(30)
}
+ private val provers_label =
+ new GUI.Label("Provers:", provers) { tooltip = provers_tooltip }
private def update_provers(): Unit = {
val new_provers = PIDE.options.string("sledgehammer_provers")
--- a/src/Tools/jEdit/src/status_widget.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/status_widget.scala Thu Aug 21 21:33:34 2025 +0200
@@ -25,7 +25,7 @@
abstract class GUI(view: View) extends JComponent {
/* init */
- setFont(new JLabel().getFont)
+ setFont(GUI.copy_font(GUI.label_font()))
private val font_render_context = new FontRenderContext(null, true, false)
private val line_metrics = getFont.getLineMetrics(template, font_render_context)
--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Aug 21 15:13:00 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Aug 21 21:33:34 2025 +0200
@@ -109,11 +109,6 @@
private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
private val threshold_tooltip = "Threshold for timing display (seconds)"
-
- private val threshold_label = new Label("Threshold: ") {
- tooltip = threshold_tooltip
- }
-
private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
reactions += {
case _: ValueChanged =>
@@ -126,6 +121,8 @@
tooltip = threshold_tooltip
verifier = { case Value.Double(x) => x >= 0.0 case _ => false }
}
+ private val threshold_label =
+ new GUI.Label("Threshold: ", threshold_value) { tooltip = threshold_tooltip }
private val controls = Wrap_Panel(List(threshold_label, threshold_value))