From 41dd3e49497246dea92878391300f51d565238e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 29 Feb 2024 10:09:45 +0100 Subject: [PATCH] Update output latex macros name Allow instance names compatible with binding names, including names with subscripts --- Isabelle_DOF/thys/Isa_DOF.thy | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 56f4a0b..0c7dc2c 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -856,8 +856,13 @@ val check_closing_ml_invs = check_invs get_closing_ml_invariants closing_ml_invariant_class_of closing_ml_invariant_check_of (* Output name for LaTeX macros. - Also rewrite "." to allow macros with objects long names *) -val output_name = Latex.output_name o translate_string (fn "." => "DOT" | s => s) + Also rewrite "." to allow macros with objects long names + and "\<^sub>" allowed in name bindings and then in instance names *) +val output_name = Symbol.explode + #> map (fn s => if equal s Symbol.sub then "SUB" else s) + #> implode + #> translate_string (fn "." => "DOT" | s => s) + #> Latex.output_name val ISA_prefix = "Isabelle_DOF_"