tuned signature: more operations;

clarified 'unbundle' polarity, according to algebraic group laws;

tuned signature: more operations;

tuned: more direct use of Name.context operations;

tuned;

misc tuning and clarification: more direct use of Name.context operations;

tuned signature: more operations;

tuned: more direct use of Name.context operations;

clarified signature: shorten common cases;

tuned: more standard Name.build_context, although that is a bit longer;

clarified signature: more uniform;

omit redundant combinators (amending 7456a64bc4f6);

tuned signature;

fixed bugs found by Stepan Holub

merged

added lemmas

merged

more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);

clarified signature and object initialization;

clarified default: avoid copies;

suppress odd icons for documents and folders;

support for modified tree cell renderer;

clarified signature: avoid implicit functionality;

re-use Output_Area;

re-use Output_Area;

re-use Output_Area;

re-use Output_Area with search results;

re-use Output_Area with search results;

more thorough init;

clarified signature: prefer defaults for Output_Dockable (and its variants);

unused;

tuned output: formatting is pointless for proportional font;