be more precise: also merge option values

only print warning in a visible context (previously, the warning was printed more than once)

dropped superfluous error message

removed obsolete make target (now in doc-src, cf. 28b487cd9e15)

updated for polyml-5.4.0; discontinued old-fashioned POLY_HOME via path; more robust handling of polyml-version, preferably provided by Poly/ML distribution itself;

made SML/NJ happy;

added merge_options convenience;

tuned string_of_int to avoid allocation for small integers;

eliminated Int.toString;

eliminated obsolete LargeInt -- Int is unbounded;

standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;

removing dead code; tuned

made SML/NJ happy

reverted 08240feb69c7 -- breaks positions of reports;

ML_trace: observe context visibility flag (import for Latex mode, for example);

more direct treatment of Position.end_offset; tuned;

discontinued unused end_line, end_column;

more scalable HTML.output_width;

refined comment (again);

merged

use proper syntactic types for 'syntax' commands

make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion

use full path for library imports

types -> type_synonym

updated NEOS_SERVER, which is now provided via settings;

renamed Sum_Of_Squares to Sum_of_Squares;

Ord_List.merge convenience;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

modernized structure Prop_Logic; avoid ML structure aliases;

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