src/Tools/jEdit/src/document_dockable.scala
Sat, 13 Aug 2022 23:04:53 +0200 wenzelm clarified signature;
Sat, 13 Aug 2022 12:32:38 +0200 wenzelm clarified signature: more explicit types;
Fri, 12 Aug 2022 20:20:53 +0200 wenzelm more GUI elements;
Fri, 12 Aug 2022 12:50:19 +0200 wenzelm basic setup for document build panel;
less more (0) tip