2013-07-09 wenzelm 2013-07-09 tuned protocol terminology; tuned signature;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-05-22 wenzelm 2013-05-22 explicit management of Session.Protocol_Handlers, with protocol state and functions; more self-contained ML/Scala module Invoke_Scala;
2013-05-14 wenzelm 2013-05-14 tuned signature;
2013-04-29 wenzelm 2013-04-29 clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
2013-03-26 wenzelm 2013-03-26 dockable window for timing information;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2012-12-14 wenzelm 2012-12-14 more formal class Command.Results;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-12-13 wenzelm 2012-12-13 identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
2012-12-12 wenzelm 2012-12-12 support dialog via document content;
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-21 wenzelm 2012-11-21 tuned whitespace;
2012-11-19 wenzelm 2012-11-19 alternative completion for outer syntax keywords;
2012-09-28 wenzelm 2012-09-28 support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28 wenzelm 2012-09-28 eliminated dead code;
2012-09-19 wenzelm 2012-09-19 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-18 wenzelm 2012-09-18 more explicit message markup and rendering;
2012-08-31 wenzelm 2012-08-31 clarified command status (again);
2012-08-31 wenzelm 2012-08-31 further refinement of command status, to accomodate forked proofs;
2012-08-30 wenzelm 2012-08-30 refined status of forked goals;
2012-08-20 wenzelm 2012-08-20 added keyword kind "thy_load" (with optional list of file extensions);
2012-08-10 wenzelm 2012-08-10 apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-08-07 wenzelm 2012-08-07 tuned signature -- slightly more abstract text representation of prover process;
2012-04-18 wenzelm 2012-04-18 more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
2012-04-07 wenzelm 2012-04-07 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-06 wenzelm 2012-04-06 discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06 wenzelm 2012-04-06 discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-05 wenzelm 2012-04-05 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-03-13 wenzelm 2012-03-13 clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-04 wenzelm 2012-03-04 clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
2012-03-03 wenzelm 2012-03-03 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;
2012-03-01 wenzelm 2012-03-01 Symbol.encode header edits;
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2012-02-26 wenzelm 2012-02-26 include warning messages in node status;
2012-01-15 wenzelm 2012-01-15 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
2012-01-14 wenzelm 2012-01-14 tuned comments;
2012-01-14 wenzelm 2012-01-14 clarified partial restrict operation;
2012-01-09 wenzelm 2012-01-09 command status color via regular markup;
2012-01-05 wenzelm 2012-01-05 prefer raw_message for protocol implementation;
2011-12-01 wenzelm 2011-12-01 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;