In the past few months there has been pretty good progress in eliminating
global references in favour of configuration options, which are managed
robustly in the context. (This also covers ancients things like
show_sorts.)
The output of 'print_config' gives an overview of options that are visible
within the Isar source language (via the attribute name space).
This also reveals a mismatch between some traditional and some newer
names, e.g. trace_simp vs. smt_trace. My feeling is that it makes more
sense to follow the newer movement here, where the tool name comes first,
followed by the aspect being controlled. Thus users see the options of
each tool grouped in the sorted output of 'print_config' immediately.
This means the longstanding trace_simp and debug_simp would become
simp_trace and simp_debug, respectively. Similar for trace_meson,
trace_metis and a few others.
Any further considerations?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
