Sat, 04 Jan 2025 16:22:05 +0100 |
wenzelm |
tuned names: more uniform;
|
file |
diff |
annotate
|
Thu, 02 Jan 2025 16:59:42 +0100 |
wenzelm |
misc tuning and clarification: more explicit types;
|
file |
diff |
annotate
|
Tue, 31 Dec 2024 15:29:29 +0100 |
wenzelm |
more accurate indentation: retain (before: Double) until it is materialized as blanks;
|
file |
diff |
annotate
|
Tue, 31 Dec 2024 15:09:36 +0100 |
wenzelm |
misc tuning: more uniform;
|
file |
diff |
annotate
|
Mon, 30 Dec 2024 19:49:50 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
Mon, 30 Dec 2024 14:39:33 +0100 |
wenzelm |
more accurate formatting of open_block: markup only, without affecting layout (e.g. via force_next);
|
file |
diff |
annotate
|
Sun, 29 Dec 2024 15:49:11 +0100 |
wenzelm |
proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
|
file |
diff |
annotate
|
Sun, 29 Dec 2024 15:39:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 29 Dec 2024 15:15:06 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 29 Dec 2024 15:05:16 +0100 |
wenzelm |
tuned: more uniform;
|
file |
diff |
annotate
|
Sun, 29 Dec 2024 14:57:13 +0100 |
wenzelm |
tuned: more uniform;
|
file |
diff |
annotate
|
Sun, 29 Dec 2024 13:16:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 07 Nov 2024 20:29:52 +0100 |
wenzelm |
clarified signature: more robust type XML.Elem;
|
file |
diff |
annotate
|
Mon, 04 Nov 2024 22:05:20 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 04 Nov 2024 20:55:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Mon, 28 Oct 2024 08:48:31 +0100 |
wenzelm |
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
|
file |
diff |
annotate
|
Sun, 06 Oct 2024 18:34:35 +0200 |
wenzelm |
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
|
file |
diff |
annotate
|
Sun, 06 Oct 2024 13:02:33 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 24 Sep 2024 18:17:39 +0200 |
wenzelm |
more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;
|
file |
diff |
annotate
|
Tue, 24 Sep 2024 17:57:42 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 12 Sep 2024 14:38:19 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
Tue, 10 Sep 2024 16:06:38 +0200 |
wenzelm |
tuned comments, following Isabelle/ML;
|
file |
diff |
annotate
|
Wed, 04 Sep 2024 13:55:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 04 Sep 2024 12:50:52 +0200 |
wenzelm |
more accurate Default_Metric;
|
file |
diff |
annotate
|
Mon, 02 Sep 2024 14:36:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Mon, 02 Sep 2024 13:42:38 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
Thu, 08 Sep 2022 16:22:44 +0200 |
wenzelm |
support Pretty.unformatted, similar to ML version;
|
file |
diff |
annotate
|
Mon, 22 Aug 2022 14:48:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
Wed, 22 Apr 2020 17:52:14 +0200 |
wenzelm |
tuned signature -- avoid warnings;
|
file |
diff |
annotate
|
Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
Tue, 05 Mar 2019 18:44:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 17 Mar 2018 20:35:23 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 30 Jan 2018 23:01:38 +0100 |
wenzelm |
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
|
file |
diff |
annotate
|
Mon, 06 Mar 2017 17:05:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 21:54:51 +0200 |
wenzelm |
proper type;
|
file |
diff |
annotate
|
Fri, 01 Apr 2016 14:38:54 +0200 |
wenzelm |
more robust pretty printing: permissive treatment of bad values;
|
file |
diff |
annotate
|
Mon, 21 Dec 2015 13:39:45 +0100 |
wenzelm |
clarified length of block with pre-existant forced breaks;
|
file |
diff |
annotate
|
Sun, 20 Dec 2015 12:50:48 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
Sun, 20 Dec 2015 12:48:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 19 Dec 2015 23:16:47 +0100 |
wenzelm |
more explicit Pretty.Tree, like in ML;
|
file |
diff |
annotate
|
Sat, 19 Dec 2015 19:07:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 19 Dec 2015 15:14:59 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 19 Dec 2015 14:47:52 +0100 |
wenzelm |
support for blocks with consistent breaks;
|
file |
diff |
annotate
|
Thu, 17 Dec 2015 17:32:01 +0100 |
wenzelm |
support pretty break indent, like underlying ML systems;
|
file |
diff |
annotate
|
Tue, 18 Feb 2014 17:03:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 04 Apr 2013 17:16:51 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
Thu, 28 Mar 2013 22:42:18 +0100 |
wenzelm |
ghost bullet via markup, which is painted as bar under text (normally space);
|
file |
diff |
annotate
|
Thu, 28 Mar 2013 15:36:45 +0100 |
wenzelm |
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
|
file |
diff |
annotate
|
Thu, 28 Mar 2013 15:00:27 +0100 |
wenzelm |
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
|
file |
diff |
annotate
|
Thu, 28 Mar 2013 14:47:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 25 Mar 2013 10:37:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 23 Mar 2013 13:57:46 +0100 |
wenzelm |
allow fractional pretty margin -- avoid premature rounding;
|
file |
diff |
annotate
|
Sat, 23 Mar 2013 13:12:39 +0100 |
wenzelm |
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
|
file |
diff |
annotate
|
Thu, 21 Mar 2013 16:58:14 +0100 |
wenzelm |
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
|
file |
diff |
annotate
|
Thu, 21 Mar 2013 16:35:53 +0100 |
wenzelm |
eliminated char_width_int to avoid unclear rounding;
|
file |
diff |
annotate
|
Sat, 12 Jan 2013 19:53:24 +0100 |
wenzelm |
more uniform Pretty.char_width;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 23:38:48 +0200 |
wenzelm |
further refinement of jEdit line range, avoiding lack of final \n;
|
file |
diff |
annotate
|