Add TODOs to delete references to where clause

The where clause for ontology classes is deprecated
in favor of the accepts and rejects clauses.
This commit is contained in:
Nicolas Méric 2021-01-28 12:48:54 +01:00
parent 5b618562a2
commit 1fb97c8fb0
2 changed files with 13 additions and 0 deletions

View File

@ -559,6 +559,9 @@ text\<open>
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
bibliography)"
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
\<close>}
In a integrated document source, the body of the content can be paranthesized into:
@ -664,6 +667,10 @@ doc_class requirement = long_name :: "string option"
doc_class requirement_analysis = no :: "nat"
where "requirement_item +"
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *)

View File

@ -114,6 +114,9 @@ text\<open>
\<^emph>\<open>is-a\<close> relation between classes;
\<^item> classes may refer to other classes via a regular expression in a
\<^emph>\<open>where\<close> clause;
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
\<^item> attributes may have default values in order to facilitate notation.
\<close>
@ -146,6 +149,9 @@ text\<open>
classes and their inheritance relation structure meta-data of text-elements in an object-oriented
manner, monitor classes enforce structural organization of documents via the language specified
by the regular expression enforcing a sequence of text-elements.
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types.
Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>,