class-term-antiquotation-implementation #2

nicolas.meric · 2021-06-01T15:44:16Z

nicolas.meric commented

2021-06-01 15:44:16 +00:00

Hello,

This branch adds the term* cmd and term antiquotations for classes.

The commmit message gives some insights:

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

Hello, This branch adds the `term*` cmd and term antiquotations for classes. The commmit message gives some insights: > - 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 >

nicolas.meric requested review from adbrucker 2021-06-01 15:44:25 +00:00

nicolas.meric requested review from wolff 2021-06-01 15:44:29 +00:00

adbrucker referenced this issue from a commit

2021-07-02 15:39:53 +00:00

Merge pull request 'class-term-antiquotation-implementation' (#2) from nicolas.meric/Isabelle_DOF:class-term-antiquotation-implementation into master Reviewed-on: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/pulls/2

adbrucker manually merged commit 6c433ed766 into master

2021-07-02 15:39:54 +00:00

adbrucker deleted branch class-term-antiquotation-implementation

2021-07-02 15:40:22 +00:00

Sign in to join this conversation.

No reviewers

No Label

No Milestone

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: Isabelle_DOF/Isabelle_DOF#2