src/Pure/PIDE/protocol.scala
Tue, 01 Apr 2014 17:29:47 +0200 wenzelm unused;
Tue, 01 Apr 2014 17:26:32 +0200 wenzelm more frugal command_status, which is often used in a tight loop;
Mon, 31 Mar 2014 15:05:24 +0200 wenzelm store blob content within document node: aux. files that were once open are made persistent;
Thu, 27 Mar 2014 19:47:30 +0100 wenzelm back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
Thu, 27 Mar 2014 10:43:43 +0100 wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
Wed, 26 Mar 2014 19:42:16 +0100 wenzelm clarified valid_id: always standardize towards static command.id;
Mon, 03 Mar 2014 12:54:12 +0100 wenzelm tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
Sat, 01 Mar 2014 15:58:47 +0100 wenzelm incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
Sat, 01 Mar 2014 12:07:26 +0100 wenzelm tuned signature -- more explicit Document.Elements;
Thu, 27 Feb 2014 14:07:04 +0100 wenzelm more formal Document.Blobs;
Fri, 21 Feb 2014 12:32:06 +0100 wenzelm tuned signature;
Tue, 18 Feb 2014 14:05:08 +0100 wenzelm more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
Wed, 12 Feb 2014 10:50:49 +0100 wenzelm clarified message_positions: cover alt_id as well;
Tue, 11 Feb 2014 21:58:31 +0100 wenzelm maintain multiple command chunks and markup trees: for main chunk and loaded files;
Tue, 11 Feb 2014 17:44:29 +0100 wenzelm common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
Tue, 11 Feb 2014 15:05:13 +0100 wenzelm report (but ignore) markup within auxiliary files;
Fri, 22 Nov 2013 21:13:44 +0100 wenzelm clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
Wed, 20 Nov 2013 11:55:52 +0100 wenzelm load files that are not provided by PIDE blobs;
Tue, 19 Nov 2013 22:12:54 +0100 wenzelm more explicit indication of missing files;
Tue, 19 Nov 2013 19:33:27 +0100 wenzelm maintain blobs within document state: digest + text in ML, digest-only in Scala;
Tue, 19 Nov 2013 12:57:56 +0100 wenzelm clarified boundary cases of Document.Node.Name;
Mon, 18 Nov 2013 17:16:56 +0100 wenzelm maintain document model for all files, with document view for theory only, and special blob for non-theory files;
Fri, 09 Aug 2013 11:18:36 +0200 wenzelm cancel_query via direct access to the exec_id of the running query process;
Mon, 05 Aug 2013 15:29:10 +0200 wenzelm tuned signature -- more uniform treatment of overlays as command mapping;
Fri, 02 Aug 2013 14:26:09 +0200 wenzelm maintain overlays within node perspective;
Wed, 31 Jul 2013 12:14:13 +0200 wenzelm allow explicit indication of required node: full eval, no prints;
Mon, 29 Jul 2013 13:00:36 +0200 wenzelm obsolete;
Sat, 13 Jul 2013 18:13:09 +0200 wenzelm more rendering for information messages;
Wed, 10 Jul 2013 22:04:57 +0200 wenzelm tuned signature;
Tue, 09 Jul 2013 13:17:22 +0200 wenzelm tuned protocol terminology;
Fri, 05 Jul 2013 16:01:45 +0200 wenzelm tuned signature;
Fri, 05 Jul 2013 15:38:03 +0200 wenzelm explicit module Document_ID as source of globally unique identifiers across ML/Scala;
Thu, 04 Jul 2013 23:51:47 +0200 wenzelm separate exec_id assignment for Command.print states, without affecting result of eval;
Wed, 22 May 2013 14:10:45 +0200 wenzelm explicit management of Session.Protocol_Handlers, with protocol state and functions;
Tue, 14 May 2013 19:30:21 +0200 wenzelm tuned signature;
Mon, 29 Apr 2013 15:47:42 +0200 wenzelm clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
Tue, 26 Mar 2013 11:26:13 +0100 wenzelm dockable window for timing information;
Wed, 27 Feb 2013 16:27:44 +0100 wenzelm discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Fri, 14 Dec 2012 12:09:08 +0100 wenzelm more formal class Command.Results;
Thu, 13 Dec 2012 17:29:23 +0100 wenzelm more careful handling of Dialog_Result, with active area and color feedback;
Thu, 13 Dec 2012 13:52:18 +0100 wenzelm identify dialogs via official serial and maintain as result message;
Wed, 12 Dec 2012 21:50:42 +0100 wenzelm support dialog via document content;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Wed, 21 Nov 2012 20:15:25 +0100 wenzelm tuned whitespace;
Mon, 19 Nov 2012 22:34:17 +0100 wenzelm alternative completion for outer syntax keywords;
Fri, 28 Sep 2012 22:53:18 +0200 wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
Fri, 28 Sep 2012 16:59:53 +0200 wenzelm eliminated dead code;
Wed, 19 Sep 2012 17:07:25 +0200 wenzelm earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
Tue, 18 Sep 2012 17:20:40 +0200 wenzelm more explicit message markup and rendering;
Fri, 31 Aug 2012 15:03:44 +0200 wenzelm clarified command status (again);
Fri, 31 Aug 2012 13:23:25 +0200 wenzelm further refinement of command status, to accomodate forked proofs;
Thu, 30 Aug 2012 15:26:37 +0200 wenzelm refined status of forked goals;
Mon, 20 Aug 2012 14:09:09 +0200 wenzelm added keyword kind "thy_load" (with optional list of file extensions);
Fri, 10 Aug 2012 15:14:45 +0200 wenzelm apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
Tue, 07 Aug 2012 15:01:48 +0200 wenzelm simplified Document.Node.Header -- internalized errors;
Tue, 07 Aug 2012 12:35:24 +0200 wenzelm tuned signature -- slightly more abstract text representation of prover process;
Wed, 18 Apr 2012 20:22:44 +0200 wenzelm more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
Sat, 07 Apr 2012 19:28:44 +0200 wenzelm added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
less more (0) -60 tip