class-term-antiquotation-implementation #2

Manually merged
adbrucker merged 2 commits from nicolas.meric/Isabelle_DOF:class-term-antiquotation-implementation into master 2021-07-02 15:39:54 +00:00

2 Commits

Author SHA1 Message Date
Achim D. Brucker cfbc3311cd Merge branch 'master' into class-term-antiquotation-implementation 2021-07-02 17:39:42 +02:00
Nicolas Méric 2c01a7118b Add term* cmd and term antiquotations for classes
- Add a term antiquotation for document classes
  and add the term* command which mimics the classical term command
  and adds the possibility to use a term antiquotation
  which references document classes:
  one can use @{A ''A_instance''} to reference
  an instance of the class A in a term* command.
- Reuse and update the ML_isa_check_generic visitor pattern
  to add the function which checks the class instance of a class,
  used by the term antiquotation for document classes.
  Also, the update_isa functions now expect long name
  (See builtin term antiquotations setup)
- The merge of ISA_transformer_tab has been update to avoid conflicts.
  Indeed, the merge is ultra-critical: the transformer tabs were
  just extended by letting *the first* entry
  with the same long-name win.
  Since the range is a (call-back) function, a comparison on its content
  is impossible and some choice has to be made.
  An alternative may be to use Symtab.join
- As classes names as constants are already bound to
  "doc_class Regular_Exp.rexp" constants by add_doc_class_cmd function,
  we use a prefix "doc_class_" when adding
  document classes term antiquotations
2021-06-01 17:32:45 +02:00