# HG changeset patch
# User wenzelm
# Date 1601240545 -7200
# Node ID 8162ca81ea8ad29bf087601fca20d934fd113061
# Parent  684f14b1e7fcc159250c9935128b28627a05eeae
suppress ligatures more robustly, notably for lualatex;

diff -r 684f14b1e7fc -r 8162ca81ea8a src/Doc/Prog_Prove/Logic.thy
--- 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{|}\\
diff -r 684f14b1e7fc -r 8162ca81ea8a src/Pure/Thy/latex.ML
--- 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 =