src/Pure/PIDE/protocol.scala
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);
Fri, 06 Apr 2012 23:34:38 +0200 wenzelm discontinued obsolete last_execs (cf. cd3ab7625519);
Fri, 06 Apr 2012 11:49:08 +0200 wenzelm discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
Thu, 05 Apr 2012 14:14:51 +0200 wenzelm less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
Thu, 15 Mar 2012 00:10:45 +0100 wenzelm some support for outer syntax keyword declarations within theory header;
Tue, 13 Mar 2012 21:17:37 +0100 wenzelm clarified command state -- markup within proper_range, excluding trailing whitespace;
Sun, 04 Mar 2012 18:15:45 +0100 wenzelm clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
Sat, 03 Mar 2012 14:04:49 +0100 wenzelm retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
Thu, 01 Mar 2012 22:26:29 +0100 wenzelm Symbol.encode header edits;
Wed, 29 Feb 2012 23:09:06 +0100 wenzelm clarified module Thy_Load;
Sun, 26 Feb 2012 20:05:14 +0100 wenzelm include warning messages in node status;
Sun, 15 Jan 2012 19:09:03 +0100 wenzelm more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
Sat, 14 Jan 2012 15:30:54 +0100 wenzelm tuned comments;
Sat, 14 Jan 2012 14:34:42 +0100 wenzelm clarified partial restrict operation;
Mon, 09 Jan 2012 23:11:28 +0100 wenzelm command status color via regular markup;
Thu, 05 Jan 2012 14:15:37 +0100 wenzelm prefer raw_message for protocol implementation;
Thu, 01 Dec 2011 14:29:14 +0100 wenzelm clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
less more (0) tip