Id in instance datatype entry
and name, id and thy_name in onto_class datatype entry are now
useless, as this information is given by the name space.
Remove them
- Use a name space table to store ML inariants objects
- Remove docclass_inv_tab, docclass_eager_inv_tab,
and docclass_lazy_inv_tab tables and accesses
- Name spaces offer the possibility to make reporting
by embedding entries position. Use this possibility
for instances (docitems) reporting
- Position and theory entries in an Instance record are now
useless, as this information is given by the name space.
Remove them
- Use a name space table to store monitor infos objects
- Remove monitor_tab table, as monitor infos were moved
to the name space table
- It offers the possibility to define scoped versions
of monitors
- Use a name space table to store docitem (instance) objects
- Remove docobj table, as instances were moved to the name space table
- It offers the possibility to define scoped versions
of docitems declaration
for text* (and others docitems definition command like value*)
and declare_reference*.
Avoid reporting for meta arguments attributes of isabelle_DOF
commands and for text input of text*
The last reporting duplication not resolved comes
from the document_command command in Isa_DOF,
which parses the meta arguments twice,
one time for the creation of the docitem
with create_and_check_docitem which will add reporting
for the attributes value
(see conv_attrs whichs calls Syntax.read_term_global,
which iwill add reporting)
and the other for the document output
with document_output which also adds reporting
(see meta_args_2_latex which calls
(Syntax.check_term ctxt o Syntax.parse_term ctxt) with
ltx_of_markup and Syntax.parse_term also adds reporting)
- Make optional meta arguments completely optional
- Make meta arguments context of ML* available in its ML context
- Make meta arguments of ML* mandatory to mimic text*.
Without meta arguments, its behavior is already captured by
the ML command