# HG changeset patch
# User nipkow
# Date 1690398237 -7200
# Node ID 7c3d681f11d43b50771fc71513a3a1e31c48764d
# Parent  33bc244eafdb2201b51af399de71d69cdfa881bd
added mbox-like latex sugar

diff -r 33bc244eafdb -r 7c3d681f11d4 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/Doc/Sugar/Sugar.thy	Wed Jul 26 21:03:57 2023 +0200
@@ -231,6 +231,25 @@
 Instead of a single variable \verb!z! you can give a whole list \verb!x y z!
 to perform multiple $\eta$-expansions.
 
+
+\subsection{Breaks and boxes}
+
+Printing longer formulas can easily lead to line breaks in unwanted places.
+This can be avoided by putting \LaTeX-like mboxes in formulas.
+There is a function @{const_typ mbox} that you can wrap around subterms and that
+is pretty-printed as a \LaTeX\ \verb$\mbox{ }$.
+If you are printing a term or formula, you can just insert @{const mbox}
+wherever you want. You can also insert it into theorems by
+virtue of the fact that @{const mbox} is defined as an identity function. Of course
+you need to adapt the proof accordingly.
+
+Unless the argument of @{const mbox} is an identifier or an application (i.e.\ of the highest precedence),
+it will be enclosed in parentheses. Thus \verb!x < mbox(f y)! results in @{term "x < mbox(f y)"}
+but \verb!x < mbox(y+z)! results in @{term "x < mbox(y+z)"}. You can switch off the
+parentheses by using the variant @{const mbox0} instead of @{const mbox}:
+\verb!x < mbox0(y+z)! results in @{term "x < mbox0(y+z)"}.
+
+
 \subsection{Inference rules}
 
 To print theorems as inference rules you need to include Didier
diff -r 33bc244eafdb -r 7c3d681f11d4 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jul 26 21:03:57 2023 +0200
@@ -8,6 +8,18 @@
 imports Main
 begin
 
+(* Boxing *)
+
+definition mbox :: "'a \<Rightarrow> 'a" where
+"mbox x = x"
+
+definition mbox0 :: "'a \<Rightarrow> 'a" where
+"mbox0 x = x"
+
+notation (latex) mbox ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>" [999] 999)
+
+notation (latex) mbox0 ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>" [0] 999)
+
 (* LOGIC *)
 notation (latex output)
   If  ("(\<^latex>\<open>\\textsf{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>else\<^latex>\<open>}\<close> (_))" 10)