src/Pure/ML/ml_pretty.ML
Wed, 11 Sep 2024 19:59:10 +0200 wenzelm clarified properties;
Wed, 11 Sep 2024 19:53:35 +0200 wenzelm clarified signature and modules;
Tue, 10 Sep 2024 12:22:24 +0200 wenzelm tuned signature;
Fri, 06 Sep 2024 14:34:07 +0200 wenzelm more accurate output: observe depth as in "prune" operation;
Fri, 06 Sep 2024 13:57:06 +0200 wenzelm clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;
Thu, 05 Sep 2024 21:16:53 +0200 wenzelm clarified Pretty.T vs. output tree (following Isabelle/Scala): Output.output_width (via print_mode) happens during formatting, instead of construction;
Thu, 05 Sep 2024 17:39:45 +0200 wenzelm clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
Thu, 06 Sep 2018 14:08:35 +0200 wenzelm simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
Thu, 07 Apr 2016 13:54:02 +0200 wenzelm simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
Thu, 07 Apr 2016 13:35:08 +0200 wenzelm clarified bootstrap of @{make_string} -- avoid query on ML environment;
Tue, 05 Apr 2016 20:51:37 +0200 wenzelm clarified modules -- simplified bootstrap;
Sat, 02 Apr 2016 22:38:26 +0200 wenzelm tuned signature;
Sat, 02 Apr 2016 21:10:07 +0200 wenzelm careful export of type-dependent functions, without losing their special status;
Fri, 01 Apr 2016 11:45:04 +0200 wenzelm adapted to Poly/ML repository version 2e40cadc975a;
Sat, 26 Mar 2016 12:22:15 +0100 wenzelm avoid hardwired values;
Fri, 18 Mar 2016 21:21:09 +0100 wenzelm clarified print depth;
Fri, 18 Mar 2016 16:26:35 +0100 wenzelm clarified modules;
Thu, 17 Mar 2016 16:56:44 +0100 wenzelm @{make_string} is available during Pure bootstrap;
Thu, 17 Mar 2016 13:44:18 +0100 wenzelm clarified modules;
Thu, 03 Mar 2016 21:59:21 +0100 wenzelm discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
less more (0) tip