src/Pure/PIDE/document.scala
Sun, 10 Nov 2024 13:40:28 +0100 wenzelm minor performance tuning: avoid concatenation of existing string material;
Sat, 09 Nov 2024 21:34:38 +0100 wenzelm Document.Snapshot: support for multiple snippet_commands;
Tue, 29 Aug 2023 12:53:28 +0200 wenzelm misc tuning: support "scalac -source 3.3";
Sun, 19 Feb 2023 13:47:10 +0100 wenzelm proper Nodes.init (amending 9b35c1171d9a);
Sun, 19 Feb 2023 13:43:38 +0100 wenzelm unused;
Sun, 19 Feb 2023 13:37:38 +0100 wenzelm tuned;
less more (0) -300 -100 -30 -10 -6 tip