nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
1,724 Commits 32 Branches 0 Tags 62 MiB
Commit Graph

1724 Commits

Author SHA1 Message Date
Achim D. Brucker 2481603ce1 Temporarily disabled release creation. 2023-02-22 06:52:12 +00:00
Achim D. Brucker b9eeb9e9b8 Temporarily disabled release creation. 2023-02-22 06:30:47 +00:00
Achim D. Brucker fa27d2425e Retired dof_mkroot. 2023-02-21 23:03:12 +00:00
Achim D. Brucker f66b6187f8 Introduced use_ontology_unchecked (for internal use only). 2023-02-21 22:34:30 +00:00
Achim D. Brucker cf386892fc Implemented support for using full-qualfied names for ontologies, allowing for user-defined ontology styles in custom sessions. 2023-02-21 21:32:23 +00:00
Achim D. Brucker f8399e0fb2 Exclude proof session from default build. 2023-02-21 08:30:07 +00:00
Achim D. Brucker 0c064b1c8a Update. 2023-02-21 08:30:02 +00:00
Achim D. Brucker 1e0eeea6f9 Update. 2023-02-21 08:18:05 +00:00
Achim D. Brucker 080d867587 Exclude proof session from default build. 2023-02-21 08:17:18 +00:00
Achim D. Brucker 3e41871b17 Added bib file. 2023-02-21 08:11:35 +00:00
Achim D. Brucker be9ef5a122 Update. 2023-02-21 08:01:43 +00:00
Achim D. Brucker 47fa3590aa Moved CENELEC ontology (and its LaTeX style) to the session Isabelle_DOF-Ontologies. 2023-02-20 23:34:54 +00:00
Achim D. Brucker fba9ca78e9 Restructured examples. 2023-02-19 22:40:11 +00:00
Achim D. Brucker 30eb47d80c Fixed section structure. 2023-02-19 22:26:18 +00:00
Achim D. Brucker 00eff9f819 Initial document setup. 2023-02-19 22:15:37 +00:00
Achim D. Brucker 73e3cb1098 Marked session as AFP candidate. 2023-02-19 20:57:06 +00:00
Achim D. Brucker e4a8ad4227 Exclude proof session from default build. 2023-02-19 20:51:28 +00:00
Achim D. Brucker f7b4cf67f7 Cleanup. 2023-02-19 18:48:37 +00:00
Achim D. Brucker 97bf5aa1e3 Fine tuning. 2023-02-19 18:20:26 +00:00
Achim D. Brucker d766ac22df Initial commit. 2023-02-19 18:12:14 +00:00
Achim D. Brucker ba90433700 Removed links to files outside of the current session. 2023-02-19 17:46:16 +00:00
Achim D. Brucker 762225d20d Added check for file references to different sessions. 2023-02-19 17:28:47 +00:00
Achim D. Brucker aaeb793a51 Moved ontologies into session Isabelle_DOF-Ontologies. 2023-02-19 16:41:16 +00:00
Achim D. Brucker 38628c37dc Integrated manual into Isabelle/DOF session. 2023-02-19 15:49:07 +00:00
Achim D. Brucker 43ccaf43f7 Refactoring of session setup. 2023-02-19 13:06:00 +00:00
Nicolas Méric 848ce311e2 Re-add name field to onto_class 
To keep the abstract syntax information
of the onto_class name, re-add it to the field
of the onto_class structure
 2023-02-17 12:56:45 +01:00
Nicolas Méric 6115f0de4a Some cleanup 2023-02-17 11:35:51 +01:00
Nicolas Méric bdfea3ddb1 Some cleanup 2023-02-17 09:08:34 +01:00
Nicolas Méric 9de18b148a Remove some instance and onto_class datatypes entries 
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
 2023-02-16 10:41:04 +01:00
Nicolas Méric 1459b8cfc3 Use name space markup for onto_class entries reporting 2023-02-16 10:07:56 +01:00
Nicolas Méric 234ff18ec0 Use a name space for Onto Classes 
- Use a name space table to store ontological class objects
- Remove docclass_tab table and accesses
 2023-02-15 17:49:29 +01:00
Nicolas Méric 55690bba33 Homogenize instance getters names 2023-02-14 09:21:11 +01:00
Nicolas Méric 93509ab17d Update file to match the new name space implementation 2023-02-14 09:20:21 +01:00
Nicolas Méric 1e09598d81 Fix typo 2023-02-14 09:20:21 +01:00
Nicolas Méric e01ec9fc21 Use a name space for ML invariants 
- 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
 2023-02-14 09:20:13 +01:00
Nicolas Méric 7c16d02979 Use a name space for Isabelle_DOF transformers 
- Use a name space table to store Isabelle_DOF transformers objects
- Remove ISA_transformer_tab table and accesses
 2023-02-12 16:49:53 +01:00
Nicolas Méric 4a77347e40 Simplify reporting of monitors 2023-02-12 11:20:13 +01:00
Nicolas Méric 2398fc579a Use name space markup for instances entries reporting 
- 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
 2023-02-11 22:48:11 +01:00
Nicolas Méric 821eefb230 Fix some markups 2023-02-10 15:23:23 +01:00
Nicolas Méric 9b51844fad Use a name space for monitors infos 
- 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
 2023-02-10 13:07:17 +01:00
Nicolas Méric c440f9628f Fix typo 2023-02-09 16:40:05 +01:00
Nicolas Méric 5b3086bbe5 Use a name space for docitems (instances) 
- 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*.
 2023-02-09 16:07:16 +01:00
Nicolas Méric 7c0d2cee55 Add docitem_name text and ML antiquotations 
Add the possibility to reference the name of instances
in text and ML code
 2023-01-30 07:43:44 +01:00
Nicolas Méric 7c6150affa Make input_term available with theory option 
The raw value term of docitems is now processed and
available when setting the theory attribute object_value_debug
 2023-01-27 15:09:34 +01:00
Nicolas Méric ad4ad52b4e Avoid reporting duplication when possible 
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)
 2023-01-27 10:32:38 +01:00
Nicolas Méric ba8227e6ab Cleanup and add position to docitem ML antiqutation 2023-01-26 09:43:51 +01:00
Nicolas Méric 20b0af740d Update meta args syntax and ML* command 
- 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
 2023-01-23 09:03:59 +01:00
Nicolas Méric 1379f8a671 Add test of invariants of an inherited attribute of an attribute 2023-01-20 09:41:19 +01:00
Achim D. Brucker 8fdaafa295 Experimental session with enabled proof objects: Isabelle_DOF-Proofs. 2023-01-19 22:00:53 +00:00
Nicolas Méric 8513f7d267 Update doc_class rails to match accepts clause 2023-01-17 09:01:55 +01:00