src/Pure/PIDE/command.scala
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Sun, 10 Mar 2019 00:21:34 +0100 wenzelm added semantic document markers;
Fri, 11 Jan 2019 22:34:28 +0100 wenzelm more operations;
Sat, 18 Aug 2018 12:41:05 +0200 wenzelm clarified modules;
Tue, 31 Jul 2018 21:11:24 +0200 wenzelm clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
Tue, 31 Jul 2018 21:06:09 +0200 wenzelm tuned signature;
Tue, 05 Jun 2018 16:12:26 +0200 wenzelm less wasteful consolidation, based on PIDE front-end state and recent changes;
Thu, 31 May 2018 22:10:06 +0200 wenzelm clarified: consolidated result is last command;
Tue, 29 May 2018 22:25:59 +0200 wenzelm more node status information;
Mon, 28 May 2018 17:40:34 +0200 wenzelm clarified signature: Known.theories retains Document.Node.Entry (with header);
Tue, 08 May 2018 11:47:41 +0200 wenzelm more robust: self-export only;
Mon, 07 May 2018 17:11:01 +0200 wenzelm store exports within PIDE command state;
Sun, 11 Mar 2018 20:56:42 +0100 wenzelm tuned;
Sun, 11 Mar 2018 20:47:17 +0100 wenzelm update XML cache for slightly modified messages;
Sun, 11 Mar 2018 20:31:25 +0100 wenzelm more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
less more (0) -100 -15 tip