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

[Makarius]

Mixfix annotations have gained a more formal status recently, with PIDE 
markup reports that lead to some highlighting and tooltips in the IDE.

In order to make this work cleanly, there needs to be exactly one 
"interning" of the input given by the user. E.g. for the term language 
this is done via Syntax.read_term: input source is turned into a term, so 
the direction is clear from the types. For type mixfix, this is done more 
implicitly: the original source positions are used once for the report and 
then reset via Mixfix.reset_pos; the result can be passed on without 
causing more reports. Omitting Mixfix.reset_pos or using the input several 
times may lead to SPAM in the IDE.


For example, see Proof_Context.read_var which is at the bottom 
of many more term specification packages: 
http://isabelle.in.tum.de/repos/isabelle/annotate/5f5f11ee4d37/src/Pure/Isar/proof_context.ML#l1079

Type notation (e.g. for 'typedecl', 'typedef') is taken care of here:
http://isabelle.in.tum.de/repos/isabelle/annotate/eeea384cafc8/src/Pure/Isar/local_theory.ML#l309

I have already checked some major specifications elements: definition, 
abbreviation, function, inductive, typedecl, typedef.


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.

(The reports on the type name could be also reduced to the core 
information.)


 	Makarius