Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update output latex macros name 

Allow instance names compatible with binding names,
including names with subscripts
This commit is contained in:
Nicolas Méric 2024-02-29 10:09:45 +01:00
parent f44b5458f2
commit 41dd3e4949
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -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_"