Hi Makarius, You wrote:
> Mixfix annotations have gained a more formal status recently, with PIDE > markup reports that lead to some highlighting and tooltips in the IDE. > [...] > BNF datatypes are a notable exception. E.g. this example produces duplicate > "bad" markup about Unicode in mixfix notation: > > datatype foobar ("ä") = Foobar ("ö") > > I did not dare to enter that highly complex implementation. 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"): fun add_fake_type spec = Typedecl.basic_typedecl {final = true} (type_binding_of_spec spec, num_As, Mixfix.reset_pos (mixfix_of_spec spec)); (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: val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy |> Local_Theory.open_target |> snd |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs => Local_Theory.define ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs)) #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss ||> `Local_Theory.close_target; 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: datatype (plugins only:) foobar = Foobar ("ö") (* 9 occurrences *) datatype (plugins only: code) foobar = Foobar ("ö") (* 11 occurrences *) datatype (plugins only: size) foobar = Foobar ("ö") (* 14 occurrences *) 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? As another data point, adding more constructors yields odd effects: datatype (plugins only:) foobar = Foobar1 ("ö") (* 17 occurrences *) | Foobar2 ("ö") (* 13 occurrences *) | Foobar3 ("ö") (* 9 occurrences *) Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev