src/Pure/PIDE/protocol_message.scala
Mon, 23 Nov 2020 15:14:58 +0100 wenzelm support for PIDE markup in batch build (inactive due to pide_reports=false);
Mon, 30 Mar 2020 19:39:11 +0200 wenzelm more accurate treatment of errors;
Sun, 29 Mar 2020 21:57:40 +0200 wenzelm clarified signature: more explicit type Protocol_Message.Marker;
Sun, 29 Mar 2020 19:42:59 +0200 wenzelm more explicit type Protocol_Message.Marker;
Mon, 16 Mar 2015 11:07:56 +0100 wenzelm clarified modules;
less more (0) tip