Add TODOs to improve the wording

This commit is contained in:
Nicolas Méric 2021-01-28 13:04:29 +01:00
parent 76266fbd5e
commit 4d9de40037
2 changed files with 8 additions and 0 deletions

View File

@ -602,6 +602,9 @@ text\<open>
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
attribute-definition (which is qualified in order to disambiguate;
\autoref{fig:Dogfood-V-attribute}).
% TODO for Burkhart Wolff.
% The last phrase should be completed to make it clearer:
% In this part "hovering over an...in order to disambiguate", something is missing.
\<close>
(* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *)

View File

@ -177,6 +177,9 @@ text\<open>
in \<^boxed_theory_text>\<open> ... \<close> which might contain certain ``quasi-letters'' such
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for
details).
% TODO for Burkhart Wolff.
% This phrase should be reviewed to clarify identifiers.
% Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>".
\<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close>
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"})
@ -282,6 +285,8 @@ text\<open>
representations definition needs to be wrapped in a
\inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context
within Isabelle's \<^LaTeX>-setup.
% TODO:
% For the "(written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>" part, to give some examples should be clearer.
Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|:
\<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\<open>renewisadof@\inlineltx{\renewisadof}\<close> for re-defining