| 2014-03-26 |
wenzelm |
2014-03-26 |
clarified valid_id: always standardize towards static command.id;
|
file | diff | annotate |
| 2014-03-03 |
wenzelm |
2014-03-03 |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
file | diff | annotate |
| 2014-03-01 |
wenzelm |
2014-03-01 |
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
tuned signature;
|
file | diff | annotate |
| 2014-03-01 |
wenzelm |
2014-03-01 |
tuned signature -- more explicit Document.Elements;
|
file | diff | annotate |
| 2014-02-27 |
wenzelm |
2014-02-27 |
more formal Document.Blobs;
removed junk;
|
file | diff | annotate |
| 2014-02-21 |
wenzelm |
2014-02-21 |
tuned signature;
|
file | diff | annotate |
| 2014-02-18 |
wenzelm |
2014-02-18 |
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
|
file | diff | annotate |
| 2014-02-12 |
wenzelm |
2014-02-12 |
clarified message_positions: cover alt_id as well;
tuned;
|
file | diff | annotate |
| 2014-02-11 |
wenzelm |
2014-02-11 |
maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;
|
file | diff | annotate |
| 2014-02-11 |
wenzelm |
2014-02-11 |
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
|
file | diff | annotate |
| 2014-02-11 |
wenzelm |
2014-02-11 |
report (but ignore) markup within auxiliary files;
|
file | diff | annotate |
| 2013-11-22 |
wenzelm |
2013-11-22 |
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
|
file | diff | annotate |
| 2013-11-20 |
wenzelm |
2013-11-20 |
load files that are not provided by PIDE blobs;
uniform resolve_files via Command.read;
|
file | diff | annotate |
| 2013-11-19 |
wenzelm |
2013-11-19 |
more explicit indication of missing files;
|
file | diff | annotate |
| 2013-11-19 |
wenzelm |
2013-11-19 |
maintain blobs within document state: digest + text in ML, digest-only in Scala;
resolve files for command span, based on defined blobs;
tuned;
|
file | diff | annotate |
| 2013-11-19 |
wenzelm |
2013-11-19 |
clarified boundary cases of Document.Node.Name;
|
file | diff | annotate |
| 2013-11-18 |
wenzelm |
2013-11-18 |
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
|
file | diff | annotate |
| 2013-08-09 |
wenzelm |
2013-08-09 |
cancel_query via direct access to the exec_id of the running query process;
|
file | diff | annotate |
| 2013-08-05 |
wenzelm |
2013-08-05 |
tuned signature -- more uniform treatment of overlays as command mapping;
|
file | diff | annotate |
| 2013-08-02 |
wenzelm |
2013-08-02 |
maintain overlays within node perspective;
tuned signature;
|
file | diff | annotate |
| 2013-07-31 |
wenzelm |
2013-07-31 |
allow explicit indication of required node: full eval, no prints;
|
file | diff | annotate |
| 2013-07-29 |
wenzelm |
2013-07-29 |
obsolete;
|
file | diff | annotate |
| 2013-07-13 |
wenzelm |
2013-07-13 |
more rendering for information messages;
|
file | diff | annotate |
| 2013-07-10 |
wenzelm |
2013-07-10 |
tuned signature;
|
file | diff | annotate |
| 2013-07-09 |
wenzelm |
2013-07-09 |
tuned protocol terminology;
tuned signature;
|
file | diff | annotate |
| 2013-07-05 |
wenzelm |
2013-07-05 |
tuned signature;
|
file | diff | annotate |
| 2013-07-05 |
wenzelm |
2013-07-05 |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file | diff | annotate |
| 2013-07-04 |
wenzelm |
2013-07-04 |
separate exec_id assignment for Command.print states, without affecting result of eval;
tuned signature;
tuned;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2013-05-14 |
wenzelm |
2013-05-14 |
tuned signature;
|
file | diff | annotate |
| 2013-04-29 |
wenzelm |
2013-04-29 |
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
|
file | diff | annotate |
| 2013-03-26 |
wenzelm |
2013-03-26 |
dockable window for timing information;
|
file | diff | annotate |
| 2013-02-27 |
wenzelm |
2013-02-27 |
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
|
file | diff | annotate |
| 2013-02-27 |
wenzelm |
2013-02-27 |
discontinued obsolete 'uses' within theory header;
|
file | diff | annotate |
| 2012-12-14 |
wenzelm |
2012-12-14 |
more formal class Command.Results;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2012-12-12 |
wenzelm |
2012-12-12 |
support dialog via document content;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2012-11-25 |
wenzelm |
2012-11-25 |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file | diff | annotate |
| 2012-11-21 |
wenzelm |
2012-11-21 |
tuned whitespace;
|
file | diff | annotate |
| 2012-11-19 |
wenzelm |
2012-11-19 |
alternative completion for outer syntax keywords;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2012-09-28 |
wenzelm |
2012-09-28 |
eliminated dead code;
|
file | diff | annotate |
| 2012-09-19 |
wenzelm |
2012-09-19 |
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
|
file | diff | annotate |
| 2012-09-18 |
wenzelm |
2012-09-18 |
more explicit message markup and rendering;
|
file | diff | annotate |
| 2012-08-31 |
wenzelm |
2012-08-31 |
clarified command status (again);
|
file | diff | annotate |
| 2012-08-31 |
wenzelm |
2012-08-31 |
further refinement of command status, to accomodate forked proofs;
|
file | diff | annotate |
| 2012-08-30 |
wenzelm |
2012-08-30 |
refined status of forked goals;
|
file | diff | annotate |
| 2012-08-20 |
wenzelm |
2012-08-20 |
added keyword kind "thy_load" (with optional list of file extensions);
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2012-08-07 |
wenzelm |
2012-08-07 |
simplified Document.Node.Header -- internalized errors;
|
file | diff | annotate |
| 2012-08-07 |
wenzelm |
2012-08-07 |
tuned signature -- slightly more abstract text representation of prover process;
|
file | diff | annotate |
| 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);
|
file | diff | annotate |
| 2012-04-07 |
wenzelm |
2012-04-07 |
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
|
file | diff | annotate |
| 2012-04-06 |
wenzelm |
2012-04-06 |
discontinued obsolete last_execs (cf. cd3ab7625519);
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2012-04-05 |
wenzelm |
2012-04-05 |
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
|
file | diff | annotate |
| 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.;
|
file | diff | annotate |
| 2012-03-13 |
wenzelm |
2012-03-13 |
clarified command state -- markup within proper_range, excluding trailing whitespace;
|
file | diff | annotate |