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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
