<html><head></head><body class="ApplePlainTextBody" dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Hi Makarius,<br><br>You wrote:<br><br><blockquote type="cite">Mixfix annotations have gained a more formal status recently, with PIDE markup reports that lead to some highlighting and tooltips in the IDE.<br>[...]<br>BNF datatypes are a notable exception. E.g. this example produces duplicate "bad" markup about Unicode in mixfix notation:<br><br> datatype foobar ("ä") = Foobar ("ö")<br><br>I did not dare to enter that highly complex implementation.<br></blockquote><br>When entering this command at the end of "BNF_Least_Fixpoint.thy", I get 2 markup occurrences occurrences for ä and 16 for ö. The 2 for ä are easily accounted for: Like in the old Berghofer-Wenzel package, the new BNF package creates a fake context (bzw. theory) extended with the type constructor to be introduced, to allow recursive occurrences of the type under definition. Specifically, "Mixfix.reset_pos" must be added here (in "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML" -- the main entry point for "(co)datatype"):<br><br> fun add_fake_type spec =<br> Typedecl.basic_typedecl {final = true}<br> (type_binding_of_spec spec, num_As, Mixfix.reset_pos (mixfix_of_spec spec));<br><br>(I will push this change later.) That takes care of the ä. As for the ö, I am out of my depth. The constructors are defined here:<br><br> val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy<br> |> Local_Theory.open_target |> snd<br> |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =><br> Local_Theory.define<br> ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))<br> #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss<br> ||> `Local_Theory.close_target;<br><br>This call to "Local_Theory.define" is the only place where the mixfix is effectively used (as one can convince oneself by grepping for "ctr_mixfix") -- elsewhere the mixfix is just threaded through. Now what's quite fascinating is that the number of duplicates one gets depends on various factors, notably the number of plugins:<br><br> datatype (plugins only:) foobar = Foobar ("ö") (* 9 occurrences *)<br> datatype (plugins only: code) foobar = Foobar ("ö") (* 11 occurrences *)<br> datatype (plugins only: size) foobar = Foobar ("ö") (* 14 occurrences *)<br><br>I suspect this is related to the local theory handling (i.e. the calls to "Local_Theory.{open,close}_target" throughout the BNF package and the plugins,"Local_Theory.background_theory_result" and "Local_Theory.declaration" in the plugins, etc.). Do you have any idea on how to proceed from here, e.g. how to debug this?<div><br></div><div>As another data point, adding more constructors yields odd effects:<br><br>datatype (plugins only:) foobar =<br> Foobar1 ("ö") (* 17 occurrences *)<br>| Foobar2 ("ö") (* 13 occurrences *)<br>| Foobar3 ("ö") (* 9 occurrences *)<br><br></div><div>Jasmin<br><br></div></body></html>