src/Pure/PIDE/rendering.scala
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;
less more (0) -30 -10 -7 tip