--- a/src/Doc/Prog_Prove/Logic.thy Sun Sep 27 17:02:59 2020 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Sun Sep 27 23:02:25 2020 +0200
@@ -49,7 +49,7 @@
\<open>\<forall>\<close> & \xsymbol{forall} & \texttt{ALL}\\
\<open>\<exists>\<close> & \xsymbol{exists} & \texttt{EX}\\
\<open>\<lambda>\<close> & \xsymbol{lambda} & \texttt{\%}\\
-\<open>\<longrightarrow>\<close> & \texttt{-{}->}\\
+\<open>\<longrightarrow>\<close> & \texttt{-{\kern0pt}->}\\
\<open>\<longleftrightarrow>\<close> & \texttt{<->}\\
\<open>\<and>\<close> & \texttt{/\char`\\} & \texttt{\&}\\
\<open>\<or>\<close> & \texttt{\char`\\/} & \texttt{|}\\
--- a/src/Pure/Thy/latex.ML Sun Sep 27 17:02:59 2020 +0200
+++ b/src/Pure/Thy/latex.ML Sun Sep 27 23:02:25 2020 +0200
@@ -115,8 +115,9 @@
| "\t" => "\\ "
| "\n" => "\\isanewline\n"
| s =>
- if exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~"
- then enclose "{\\char`\\" "}" s else s);
+ s
+ |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
+ |> suffix "{\\kern0pt}");
fun output_ascii_breakable sep =
space_explode sep
@@ -169,7 +170,7 @@
| output_chr "\n" = "\\isanewline\n"
| output_chr c =
(case Symtab.lookup char_table c of
- SOME s => s
+ SOME s => s ^ "{\\kern0pt}"
| NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
fun output_sym sym =