Ref maintenance notes: Tools for scenario improvement and for documentation update
renumber_scenario.stl
[TO BE FILLED IN]
collect_symbols.stl
This tool constructs a cross-reference table of the definitions appearing in the shared common scenario;
moreover, it builds many catalogs, one for each symbol whose definition appears in that scenario, containing the
claims of the theorems regarding that symbol. Such catalogs form a folder of HTML files, which will complements the Ref's
user manual, while the cross-reference table will become a section of that manual.
Here is how the symbol collector is used:
- Prepare as input for the tool
collect_symbs.stl
the two files
keep_definition_summary2
keep_theorem_summary2
by:
- running a standalone EtnaNova on the whole scenario, with the range set to "1" (one);
- suitably renaming the files produced by that run, which are:
definition_summary2
theorem_summary2;
- manually removing from the file keep_theorem_summary2 into which the latter of these
has been renamed all the "<P>"s suffixing the theorems' claims.
- Perform a SETL compilation of collect_symbs.stl, after re-adjusting
the path indicated within it in the open and get_lines instructions, and in the
assignments to input_file, output_file, error_file, so that it
corresponds to the wanted folder, e.g. "./", referred to in what follows as
_folder.
- Insert a copy of the file common_scenario.txt into
_folder.
- Create a subdirectory of _folder, naming it user_manual_xref.
- Launch a SETL execution of the program test: this will
- print a series of table-entry lines which, once placed with an HTML file, produce a nice-looking table,
which you should save, e.g. by the name
myTable.html,
to then supersede by it the "Cross-reference table of Ref scenario definitions" within the manual
Ref_user_manual.html;
- generate and insert into _folder/user_manual_xref, corresponding to each symbol "Sy"
defined within common_scenario.txt,
a file named Sy.html constituted by all theorems' claims that involve "Sy" within common_scenario.txt.
pretty printer
[TO BE FILLED IN]