avoid massive multiplication of reports due to interpretation;

evaluate ML expressions within debugger context;
redirected writeln/warning for ML compiler;

refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;

support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;

prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;

tuned;

support for completion within the formal context;
tuned signature;

provide global operations as well;

tuned signature;

reports with body text, not just markup;

made Context_Position independent from Config;

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

tuned signature;

bulk reports for improved message throughput;

added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);

simplified some internal flags using Config.T instead of full-blown Proof_Data;

tuned signature of (Context_)Position.report variants;

simplified/clarified (Context_)Position.markup/reported_text;

more careful treatment of context visibility flag wrt. spurious warnings;

Output_Position.report_text -- markup with potential "arguments";

prefer Context_Position.report where a proper context is available -- notably for "inner" entities;

adapted Generic_Data, Proof_Data;
tuned;

modernized structure Context_Position;

removed Ids;

renamed report to report_visible;
tuned comments;

Context position visibility.

removed obsolete context_position.ML (superseded by Position.thread_data);

turned into generic context data;

added properties_of;

Context positions.