src/Pure/PIDE/rendering.scala
Fri, 01 Nov 2024 18:17:03 +0100 wenzelm clarified rendering: entity acts as atomic notation / expression;
Fri, 01 Nov 2024 18:12:40 +0100 wenzelm more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
Fri, 01 Nov 2024 16:53:10 +0100 wenzelm support Isabelle/jEdit action isabelle.select_structure;
Sat, 19 Oct 2024 22:38:51 +0200 wenzelm clarified order of tooltips: make it less dependent on report order from ML (which differs for input vs. output);
Sat, 19 Oct 2024 22:20:05 +0200 wenzelm clarified signature (see also 1de8a8b1ae79);
Sat, 19 Oct 2024 22:01:36 +0200 wenzelm clarified signature;
Sun, 06 Oct 2024 21:55:31 +0200 wenzelm tuned output;
Fri, 23 Aug 2024 15:30:09 +0200 Fabian Huch add comments to rendering, e.g. to collect them from build database;
Fri, 20 Sep 2024 15:35:16 +0200 wenzelm block markup for specific notation, notably infix and binder;
Mon, 16 Sep 2024 19:58:28 +0200 wenzelm more formal Markup.expression;
Tue, 29 Aug 2023 12:53:28 +0200 wenzelm misc tuning: support "scalac -source 3.3";
Fri, 20 Jan 2023 20:26:42 +0100 wenzelm dismantle special treatment of citations in Isabelle/Scala;
Fri, 13 Jan 2023 17:14:59 +0100 wenzelm clarified signature: more explicit types;
Sun, 01 Jan 2023 22:54:40 +0100 wenzelm tuned signature, following Url.append_path;
Sat, 17 Dec 2022 11:33:13 +0100 wenzelm clarified signature;
Sat, 01 Oct 2022 15:42:52 +0200 wenzelm clarified signature, to support external tools like "isabelle narration";
Mon, 22 Aug 2022 14:48:14 +0200 wenzelm tuned signature;
Sat, 13 Aug 2022 14:29:59 +0200 wenzelm more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
Fri, 08 Apr 2022 15:56:14 +0200 wenzelm tuned -- avoid warnings for scala3;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Sun, 14 Nov 2021 15:21:40 +0100 wenzelm clarified signature;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Wed, 16 Dec 2020 13:22:38 +0100 wenzelm tuned signature;
Mon, 14 Dec 2020 22:01:54 +0100 wenzelm clarified caret focus modifier, depending on option "jedit_focus_modifier";
Mon, 14 Dec 2020 16:51:12 +0100 wenzelm tuned;
Mon, 14 Dec 2020 16:40:33 +0100 wenzelm tuned;
Sun, 13 Dec 2020 23:11:41 +0100 wenzelm unused (see 29566b6810f7);
Sun, 13 Dec 2020 23:06:33 +0100 wenzelm proper argument --- amending 908d8be90533;
Sun, 13 Dec 2020 22:54:27 +0100 wenzelm tuned;
less more (0) -100 -50 -30 tip