[isabelle-dev] PIDE reports on mixfix annotations (notably for datatype)

[Jasmin Blanchette]

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