#
3cb62cf1 |
|
02-Oct-2019 |
wenzelm <none@none> |
more robust: avoid update/interrupt of long-running print_consolidation;
|
#
ac5c3f5b |
|
16-Sep-2019 |
wenzelm <none@none> |
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
|
#
ba0828fb |
|
02-Sep-2019 |
wenzelm <none@none> |
clarified signature: prefer operations without position;
|
#
d8c6845a |
|
10-Mar-2019 |
wenzelm <none@none> |
document markers are formal comments, and may thus occur anywhere in the command-span; clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure; tuned signature;
|
#
67153f22 |
|
09-Mar-2019 |
wenzelm <none@none> |
added semantic document markers; emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?); tuned;
|
#
2b7111f5 |
|
11-Jan-2019 |
wenzelm <none@none> |
more operations;
|
#
c4fc6914 |
|
17-Aug-2018 |
wenzelm <none@none> |
clarified modules;
|
#
2478148c |
|
31-Jul-2018 |
wenzelm <none@none> |
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
|
#
aa9ccd83 |
|
31-Jul-2018 |
wenzelm <none@none> |
tuned signature;
|
#
62ac99b4 |
|
05-Jun-2018 |
wenzelm <none@none> |
less wasteful consolidation, based on PIDE front-end state and recent changes;
|
#
f3689209 |
|
31-May-2018 |
wenzelm <none@none> |
clarified: consolidated result is last command;
|
#
b82b4fe5 |
|
29-May-2018 |
wenzelm <none@none> |
more node status information;
|
#
7ed9bce7 |
|
28-May-2018 |
wenzelm <none@none> |
clarified signature: Known.theories retains Document.Node.Entry (with header);
|
#
13f2055d |
|
08-May-2018 |
wenzelm <none@none> |
more robust: self-export only;
|
#
0ca97edd |
|
07-May-2018 |
wenzelm <none@none> |
store exports within PIDE command state; Markup.Export.unapply: proper NAME;
|
#
cbc1fd22 |
|
11-Mar-2018 |
wenzelm <none@none> |
tuned;
|
#
25a3095d |
|
11-Mar-2018 |
wenzelm <none@none> |
update XML cache for slightly modified messages;
|
#
fa85d10e |
|
11-Mar-2018 |
wenzelm <none@none> |
more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
|
#
963d2784 |
|
16-Jan-2018 |
wenzelm <none@none> |
discontinued old form of marginal comments;
|
#
3fef719d |
|
31-Oct-2017 |
wenzelm <none@none> |
clarified signature;
|
#
0816bf69 |
|
05-Oct-2017 |
wenzelm <none@none> |
completion supports theory header imports; tuned;
|
#
f6ce89c5 |
|
08-Aug-2017 |
wenzelm <none@none> |
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
|
#
1a2ae8bf |
|
20-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
2a5365d0 |
|
16-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
fdd7b52c |
|
03-Apr-2017 |
wenzelm <none@none> |
provide session qualifier via resources;
|
#
d98c47df |
|
01-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
587e1ba4 |
|
20-Mar-2017 |
wenzelm <none@none> |
support to encode/decode command state; support to merge full contents of command state;
|
#
bae69130 |
|
07-Jan-2017 |
wenzelm <none@none> |
more uniform node_header (non-strict); removed dead code;
|
#
63752833 |
|
07-Jan-2017 |
wenzelm <none@none> |
tuned signature;
|
#
60512dcf |
|
07-Jan-2017 |
wenzelm <none@none> |
tuned signature;
|
#
08b0c0d7 |
|
05-Jan-2017 |
wenzelm <none@none> |
suppress empty results;
|
#
d39d0bde |
|
07-Nov-2016 |
wenzelm <none@none> |
more uniform path syntax, as in ML (see 5a7c919a4ada);
|
#
8891b58f |
|
02-Aug-2016 |
wenzelm <none@none> |
tuned signature -- prover-independence is presently theoretical;
|
#
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
#
4691a849 |
|
13-Apr-2016 |
wenzelm <none@none> |
clarified syntax;
|
#
a2ea8657 |
|
04-Nov-2015 |
wenzelm <none@none> |
symbolic syntax "\<comment> text";
|
#
4cab9a1c |
|
19-Sep-2015 |
wenzelm <none@none> |
straight-forward refresh, without special preconditions; eliminated somewhat expensive eq_content;
|
#
94ef994d |
|
12-Aug-2015 |
wenzelm <none@none> |
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
|
#
a1adae4d |
|
04-Apr-2015 |
wenzelm <none@none> |
more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
|
#
0b1d4452 |
|
17-Mar-2015 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
fa0358c5 |
|
16-Mar-2015 |
wenzelm <none@none> |
avoid duplicate header errors, more precise positions; tuned signature;
|
#
7995e7b7 |
|
16-Mar-2015 |
wenzelm <none@none> |
clarified modules;
|
#
da97386c |
|
15-Mar-2015 |
wenzelm <none@none> |
more markup, which helps to create missing imports;
|
#
85bc7c0e |
|
15-Mar-2015 |
wenzelm <none@none> |
proper command id for inlined errors, which is important for Command.State.accumulate;
|
#
9332afeb |
|
15-Mar-2015 |
wenzelm <none@none> |
clarified span position;
|
#
f6c83d3a |
|
15-Mar-2015 |
wenzelm <none@none> |
hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
|
#
301d8d2f |
|
14-Mar-2015 |
wenzelm <none@none> |
tuned;
|
#
4fae97cd |
|
14-Mar-2015 |
wenzelm <none@none> |
value-oriented user error, for well-defined Thy_Syntax.chop_common;
|
#
9d03af49 |
|
12-Mar-2015 |
wenzelm <none@none> |
simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;
|
#
84b44315 |
|
12-Mar-2015 |
wenzelm <none@none> |
clarified command content;
|
#
94b840f9 |
|
30-Dec-2014 |
wenzelm <none@none> |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
#
8206ccc3 |
|
01-Dec-2014 |
wenzelm <none@none> |
tuned signature;
|
#
e0e8cf48 |
|
02-May-2015 |
wenzelm <none@none> |
misc tuning, based on warnings by IntelliJ IDEA;
|
#
268b5fb9 |
|
12-Aug-2014 |
wenzelm <none@none> |
tuned;
|
#
339270d6 |
|
12-Aug-2014 |
wenzelm <none@none> |
clarified Position.Identified: do not require range from prover, default to command position;
|
#
236cf36c |
|
12-Aug-2014 |
wenzelm <none@none> |
maintain Command_Range position as in ML;
|
#
fec16c8c |
|
11-Aug-2014 |
wenzelm <none@none> |
separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
|
#
7b1c5774 |
|
11-Aug-2014 |
wenzelm <none@none> |
tuned signature;
|
#
568a33fb |
|
11-Aug-2014 |
wenzelm <none@none> |
tuned output, in accordance to transaction name in ML;
|
#
dab841c6 |
|
11-Aug-2014 |
wenzelm <none@none> |
more explicit type Span in Scala, according to ML version;
|
#
9dcf6642 |
|
02-Aug-2014 |
wenzelm <none@none> |
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
|
#
6ea51c65 |
|
23-Jul-2014 |
wenzelm <none@none> |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
#
3be931d9 |
|
29-Apr-2014 |
wenzelm <none@none> |
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
|
#
b450dc3e |
|
26-Apr-2014 |
wenzelm <none@none> |
tuned signature;
|
#
41bc3632 |
|
26-Apr-2014 |
wenzelm <none@none> |
tuned signature;
|
#
db858fa4 |
|
10-Apr-2014 |
wenzelm <none@none> |
ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL; silently ignore excessive reports -- no ambition to detect that situation accurately;
|
#
4f734489 |
|
09-Apr-2014 |
wenzelm <none@none> |
tuned;
|
#
de46f140 |
|
08-Apr-2014 |
wenzelm <none@none> |
expose more bad cases;
|
#
28ac0b2c |
|
08-Apr-2014 |
wenzelm <none@none> |
tuned signature;
|
#
a92aafc7 |
|
08-Apr-2014 |
wenzelm <none@none> |
simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway;
|
#
d64f2f83 |
|
08-Apr-2014 |
wenzelm <none@none> |
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
|
#
39d3493f |
|
08-Apr-2014 |
wenzelm <none@none> |
avoid data redundancy;
|
#
dfdc7b48 |
|
08-Apr-2014 |
wenzelm <none@none> |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
#
c9855b98 |
|
07-Apr-2014 |
wenzelm <none@none> |
more uniform Command.Chunk operations;
|
#
38f7f406 |
|
07-Apr-2014 |
wenzelm <none@none> |
more explicit Command.Chunk types, less ooddities; tuned;
|
#
ecb3fc1e |
|
03-Apr-2014 |
wenzelm <none@none> |
more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned;
|
#
4f51da4c |
|
02-Apr-2014 |
wenzelm <none@none> |
more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;
|
#
e1b43ec5 |
|
01-Apr-2014 |
wenzelm <none@none> |
persistent protocol_status, to improve performance of node_status a little;
|
#
ae2ec935 |
|
31-Mar-2014 |
wenzelm <none@none> |
store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index;
|
#
aff45da1 |
|
26-Mar-2014 |
wenzelm <none@none> |
more frugal merge of markup trees: filter wrt. subsequent query;
|
#
e5bc4603 |
|
27-Mar-2014 |
wenzelm <none@none> |
more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;
|
#
c5b8da2c |
|
26-Mar-2014 |
wenzelm <none@none> |
clarified valid_id: always standardize towards static command.id;
|
#
1447d8e0 |
|
02-Mar-2014 |
wenzelm <none@none> |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
#
9b664ef4 |
|
01-Mar-2014 |
wenzelm <none@none> |
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;
|
#
0806ca6d |
|
27-Feb-2014 |
wenzelm <none@none> |
reparse only for actually changed blobs; tuned signature;
|
#
429844ae |
|
26-Feb-2014 |
wenzelm <none@none> |
tuned output;
|
#
3b52ddc2 |
|
21-Feb-2014 |
wenzelm <none@none> |
tuned signature;
|
#
bc4bd17f |
|
21-Feb-2014 |
wenzelm <none@none> |
more general / abstract Command.Markups, with separate index for status elements; slightly faster Rendering.overview_color;
|
#
f19adf4e |
|
21-Feb-2014 |
wenzelm <none@none> |
tuned signature -- avoid obscure default arguments;
|
#
950ff753 |
|
20-Feb-2014 |
wenzelm <none@none> |
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
|
#
ffd59da7 |
|
20-Feb-2014 |
wenzelm <none@none> |
tuned imports;
|
#
0ff8715e |
|
18-Feb-2014 |
wenzelm <none@none> |
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
|
#
c435fac6 |
|
12-Feb-2014 |
wenzelm <none@none> |
more accurate eq_content;
|
#
eff64a37 |
|
12-Feb-2014 |
wenzelm <none@none> |
clarified message_positions: cover alt_id as well; tuned;
|
#
f08475a6 |
|
11-Feb-2014 |
wenzelm <none@none> |
maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;
|
#
972d63f1 |
|
11-Feb-2014 |
wenzelm <none@none> |
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content); more informative type Blob, to allow markup reports;
|
#
e67407de |
|
11-Feb-2014 |
wenzelm <none@none> |
tuned signature;
|
#
500182e7 |
|
11-Feb-2014 |
wenzelm <none@none> |
report (but ignore) markup within auxiliary files;
|
#
0d2c8425 |
|
20-Nov-2013 |
wenzelm <none@none> |
ranges of thy_load commands count as visible within perspective; convert ranges wrt. snapshot -- relevant for outdated situation;
|
#
2352f225 |
|
19-Nov-2013 |
wenzelm <none@none> |
more explicit indication of missing files;
|
#
884c6561 |
|
19-Nov-2013 |
wenzelm <none@none> |
maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
|
#
a814f441 |
|
19-Nov-2013 |
wenzelm <none@none> |
proper Thy_Load.append of auxiliary file names; inlined errors;
|
#
99202eab |
|
18-Nov-2013 |
wenzelm <none@none> |
inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;
|
#
f26b7055 |
|
17-Nov-2013 |
wenzelm <none@none> |
explicit indication of thy_load commands;
|
#
b30e322f |
|
09-Aug-2013 |
wenzelm <none@none> |
retain original messages properties, e.g. for retrieval via Command.Results;
|
#
c106f8f8 |
|
02-Aug-2013 |
wenzelm <none@none> |
maintain overlays within node perspective; tuned signature;
|
#
92c95897 |
|
12-Jul-2013 |
wenzelm <none@none> |
full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
|
#
96559435 |
|
05-Jul-2013 |
wenzelm <none@none> |
tuned signature; tuned comments;
|
#
0f5e43f5 |
|
05-Jul-2013 |
wenzelm <none@none> |
tuned signature -- eliminated pointless type synonym;
|
#
214e6101 |
|
05-Jul-2013 |
wenzelm <none@none> |
tuned signature;
|
#
328dbab6 |
|
05-Jul-2013 |
wenzelm <none@none> |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
#
4f5ef9b1 |
|
04-Jul-2013 |
wenzelm <none@none> |
separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
|
#
a3c0dc0a |
|
03-Jul-2013 |
wenzelm <none@none> |
tuned;
|
#
22226e0f |
|
03-Jul-2013 |
wenzelm <none@none> |
tuned signature;
|
#
c4be8868 |
|
03-Jul-2013 |
wenzelm <none@none> |
tuned signature;
|
#
77a337b7 |
|
23-Mar-2013 |
wenzelm <none@none> |
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
|
#
c9dd6b84 |
|
23-Mar-2013 |
wenzelm <none@none> |
structural equality for Command.Results; more general Command.State.eq_content;
|
#
70c2b141 |
|
25-Jan-2013 |
wenzelm <none@none> |
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally; reverted f3588e59aeaa accordingly;
|
#
45bb15c2 |
|
14-Dec-2012 |
wenzelm <none@none> |
tuned;
|
#
0bf00ee3 |
|
13-Dec-2012 |
wenzelm <none@none> |
tuned implementation according to Library.insert/merge in ML;
|
#
3bb096ea |
|
13-Dec-2012 |
wenzelm <none@none> |
more formal class Command.Results;
|
#
48a4815f |
|
13-Dec-2012 |
wenzelm <none@none> |
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;
|
#
ac81bbc5 |
|
13-Dec-2012 |
wenzelm <none@none> |
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;
|
#
1e388b89 |
|
12-Dec-2012 |
wenzelm <none@none> |
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
|
#
95d64a2f |
|
25-Nov-2012 |
wenzelm <none@none> |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
#
4b9ea399 |
|
22-Nov-2012 |
wenzelm <none@none> |
more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;
|
#
36974f03 |
|
21-Nov-2012 |
wenzelm <none@none> |
always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
|
#
59878eba |
|
28-Sep-2012 |
wenzelm <none@none> |
tuned signature;
|
#
ada189af |
|
27-Sep-2012 |
wenzelm <none@none> |
operations to turn markup into XML; tuned;
|
#
ff4caf34 |
|
22-Sep-2012 |
wenzelm <none@none> |
accumulate under exec_id as well;
|
#
15166850 |
|
22-Sep-2012 |
wenzelm <none@none> |
more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
|
#
dc68f0f8 |
|
21-Sep-2012 |
wenzelm <none@none> |
more realistic sendback: pick exec_id from message position and text from buffer;
|
#
0a23cda4 |
|
20-Sep-2012 |
wenzelm <none@none> |
tuned signature;
|
#
8a52b34a |
|
19-Sep-2012 |
wenzelm <none@none> |
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
|
#
6cec8932 |
|
18-Sep-2012 |
wenzelm <none@none> |
more explicit message markup and rendering;
|
#
603e40fa |
|
18-Sep-2012 |
wenzelm <none@none> |
some actual rich text markup via XML.content_markup; tuned signature;
|
#
81c0cb97 |
|
18-Sep-2012 |
wenzelm <none@none> |
some support for inital command markup; tuned signature;
|
#
05c4db3a |
|
14-Sep-2012 |
wenzelm <none@none> |
refined output panel: more value-oriented approach to update and caret focus;
|
#
e447a450 |
|
31-Aug-2012 |
wenzelm <none@none> |
more markup for failed goal forks, reusing "bad";
|
#
d081821f |
|
24-Aug-2012 |
wenzelm <none@none> |
more precise counting of line/column;
|
#
33306573 |
|
10-Aug-2012 |
wenzelm <none@none> |
clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;
|
#
767a6e3a |
|
09-Aug-2012 |
wenzelm <none@none> |
tuned signature;
|
#
26fbb647 |
|
07-Aug-2012 |
wenzelm <none@none> |
more structural parsing for minor modes; tuned signatures;
|
#
088246e6 |
|
30-Jul-2012 |
wenzelm <none@none> |
tuned signature;
|
#
6ad3e6f7 |
|
13-Apr-2012 |
wenzelm <none@none> |
include trailing comments in proper_command range;
|
#
33d04ee1 |
|
19-Mar-2012 |
wenzelm <none@none> |
clarified command span classification: strict Command.is_command, permissive Command.name;
|
#
bda60719 |
|
13-Mar-2012 |
wenzelm <none@none> |
clarified command state -- markup within proper_range, excluding trailing whitespace;
|
#
b9858340 |
|
04-Mar-2012 |
wenzelm <none@none> |
added Command.proper_range (still unused);
|
#
78b39fdb |
|
27-Feb-2012 |
wenzelm <none@none> |
prefer final ADTs -- prevent ooddities;
|
#
350d6609 |
|
09-Jan-2012 |
wenzelm <none@none> |
tuned;
|
#
113875f2 |
|
06-Jan-2012 |
wenzelm <none@none> |
accumulate status as regular markup for command range; tuned signature;
|
#
0c7f4273 |
|
01-Dec-2011 |
wenzelm <none@none> |
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover; --HG-- rename : src/Pure/PIDE/isabelle_document.ML => src/Pure/PIDE/protocol.ML rename : src/Pure/PIDE/isabelle_document.scala => src/Pure/PIDE/protocol.scala
|
#
23e33658 |
|
29-Nov-2011 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/PIDE/isar_document.ML => src/Pure/PIDE/isabelle_document.ML rename : src/Pure/PIDE/isar_document.scala => src/Pure/PIDE/isabelle_document.scala
|
#
99fd6f8e |
|
28-Nov-2011 |
wenzelm <none@none> |
separate module for concrete Isabelle markup; --HG-- rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala
|
#
4532f034 |
|
26-Nov-2011 |
wenzelm <none@none> |
sharing of token source with span source;
|
#
b35bf5c7 |
|
11-Nov-2011 |
wenzelm <none@none> |
prefer statically typed Text.Markup;
|
#
ceea376b |
|
17-Sep-2011 |
wenzelm <none@none> |
Document.Node.Name convenience;
|
#
5bc0b7a6 |
|
01-Sep-2011 |
wenzelm <none@none> |
more abstract Document.Node.Name; tuned signature;
|
#
5699f5dd |
|
31-Aug-2011 |
wenzelm <none@none> |
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
|
#
0ad342b9 |
|
25-Aug-2011 |
wenzelm <none@none> |
slightly more abstract Command.Perspective;
|
#
1fe53e5f |
|
22-Aug-2011 |
wenzelm <none@none> |
propagate editor perspective through document model;
|
#
dce0667a |
|
22-Aug-2011 |
wenzelm <none@none> |
some support for editor perspective;
|
#
16933a60 |
|
08-Jul-2011 |
wenzelm <none@none> |
tuned signature;
|
#
6505c43a |
|
04-Jul-2011 |
wenzelm <none@none> |
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
|
#
80be4c97 |
|
23-Jun-2011 |
wenzelm <none@none> |
explicit import java.lang.System to prevent odd scope problems;
|
#
1919631e |
|
16-Nov-2010 |
wenzelm <none@none> |
avoid spam;
|
#
1f34d8ae |
|
10-Nov-2010 |
wenzelm <none@none> |
some support for nested source structure, based on section headings;
|
#
53d76953 |
|
22-Sep-2010 |
wenzelm <none@none> |
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
|
#
81026577 |
|
17-Sep-2010 |
wenzelm <none@none> |
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
|
#
5911d102 |
|
07-Sep-2010 |
wenzelm <none@none> |
Command.State.accumulate: check actual source range;
|
#
a1b7f174 |
|
07-Sep-2010 |
wenzelm <none@none> |
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
|
#
fdda0ab8 |
|
31-Aug-2010 |
wenzelm <none@none> |
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;
|
#
64d1e237 |
|
30-Aug-2010 |
wenzelm <none@none> |
Command.newlines: account for physical newlines;
|
#
6dbb6870 |
|
30-Aug-2010 |
wenzelm <none@none> |
Command.results: ordered by serial number;
|
#
0648b9d4 |
|
25-Aug-2010 |
wenzelm <none@none> |
tuned;
|
#
386a6d44 |
|
25-Aug-2010 |
wenzelm <none@none> |
organized markup properties via apply/unapply patterns;
|
#
9ccceb67 |
|
25-Aug-2010 |
wenzelm <none@none> |
more precise Command.State accumulation;
|
#
33605df2 |
|
24-Aug-2010 |
wenzelm <none@none> |
tuned root markup;
|
#
608852a1 |
|
23-Aug-2010 |
wenzelm <none@none> |
tuned;
|
#
d7270883 |
|
22-Aug-2010 |
wenzelm <none@none> |
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
|
#
fab50630 |
|
22-Aug-2010 |
wenzelm <none@none> |
tuned signature;
|
#
0c8441ec |
|
22-Aug-2010 |
wenzelm <none@none> |
renamed Markup_Tree.Node to Text.Info; Markup_Tree.select: body may depend on full Text.Info, including range; tuned;
|
#
d4b0570b |
|
22-Aug-2010 |
wenzelm <none@none> |
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
|
#
dc925c0f |
|
22-Aug-2010 |
wenzelm <none@none> |
Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
|
#
37f3a0f9 |
|
21-Aug-2010 |
wenzelm <none@none> |
Command.State: accumulate markup reports uniformly; Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo; tuned;
|
#
a6fec303 |
|
19-Aug-2010 |
wenzelm <none@none> |
parameterized type Markup_Tree.Node; Markup_Tree.select: allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;
|
#
dea8d8a9 |
|
19-Aug-2010 |
wenzelm <none@none> |
Command.status: full XML.Tree, i.e. Markup with potential "arguments";
|
#
33051fbd |
|
18-Aug-2010 |
wenzelm <none@none> |
more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned; --HG-- rename : src/Pure/PIDE/markup_node.scala => src/Pure/PIDE/markup_tree.scala
|
#
60a48f10 |
|
18-Aug-2010 |
wenzelm <none@none> |
decode Isabelle symbol positions in one spot;
|
#
364bfe13 |
|
15-Aug-2010 |
wenzelm <none@none> |
simplified command status: interpret stacked markup on demand;
|
#
77b4012b |
|
15-Aug-2010 |
wenzelm <none@none> |
some derived operations on Text.Range;
|
#
cdd2dbd0 |
|
15-Aug-2010 |
wenzelm <none@none> |
specific types Text.Offset and Text.Range; minor tuning;
|
#
e48ffdcf |
|
14-Aug-2010 |
wenzelm <none@none> |
Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
|
#
5de80cbe |
|
14-Aug-2010 |
wenzelm <none@none> |
tuned;
|
#
dd050010 |
|
13-Aug-2010 |
wenzelm <none@none> |
explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;
|
#
4b67ce4d |
|
12-Aug-2010 |
wenzelm <none@none> |
more basic notion of unparsed input;
|
#
59aa9793 |
|
12-Aug-2010 |
wenzelm <none@none> |
clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;
|
#
94077aa1 |
|
12-Aug-2010 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
b7e2c404 |
|
12-Aug-2010 |
wenzelm <none@none> |
specific command state;
|
#
ce57bd98 |
|
12-Aug-2010 |
wenzelm <none@none> |
specific Session.Commands_Changed;
|
#
991ea1c1 |
|
11-Aug-2010 |
wenzelm <none@none> |
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
|
#
46e35a95 |
|
06-Aug-2010 |
wenzelm <none@none> |
avoid null in Scala; tuned comments;
|
#
ef07e3b5 |
|
05-Aug-2010 |
wenzelm <none@none> |
simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;
|
#
69db20f2 |
|
13-Jun-2010 |
wenzelm <none@none> |
tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
|
#
28704e0a |
|
30-May-2010 |
wenzelm <none@none> |
more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;
|
#
db9ed1d8 |
|
29-May-2010 |
wenzelm <none@none> |
tuned messages;
|
#
cf7b6203 |
|
28-May-2010 |
wenzelm <none@none> |
accumulate only local results -- no proper history support yet;
|
#
0dffbb6d |
|
26-May-2010 |
wenzelm <none@none> |
Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);
|
#
e534e28c |
|
20-May-2010 |
wenzelm <none@none> |
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
|
#
82d4d541 |
|
05-May-2010 |
wenzelm <none@none> |
some rearrangement of Scala sources; --HG-- rename : src/Pure/Thy/change.scala => src/Pure/PIDE/change.scala rename : src/Pure/Thy/command.scala => src/Pure/PIDE/command.scala rename : src/Pure/Thy/document.scala => src/Pure/PIDE/document.scala rename : src/Pure/General/event_bus.scala => src/Pure/PIDE/event_bus.scala rename : src/Pure/Thy/markup_node.scala => src/Pure/PIDE/markup_node.scala rename : src/Pure/Thy/state.scala => src/Pure/PIDE/state.scala rename : src/Pure/Thy/text_edit.scala => src/Pure/PIDE/text_edit.scala rename : src/Pure/General/download.scala => src/Pure/System/download.scala rename : src/Pure/General/swing_thread.scala => src/Pure/System/swing_thread.scala
|