[isabelle-dev] configuration options

[Makarius]

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