src/Pure/ROOT

clarified exported messages, e.g. suppress "information", "tracing";
export "legacy_feature" as "warning", in accordance to console default output;

chapter Pure

session Pure =
  description {*
    The Pure logical framework
  *}
  options [threads = 1]
  theories
    Pure (global)
    ML_Bootstrap (global)
    Sessions