src/Pure/PIDE/document.scala
12 months ago wenzelm 2018-06-11 clarified signature: persistent results;
12 months ago wenzelm 2018-06-05 less wasteful consolidation, based on PIDE front-end state and recent changes;
12 months ago wenzelm 2018-06-03 clarified signature: prefer Document.Snapshot;
13 months ago wenzelm 2018-05-31 clarified: consolidated result is last command;
13 months ago wenzelm 2018-05-29 more node status information;
13 months ago wenzelm 2018-05-29 tuned signature;
13 months ago wenzelm 2018-05-29 tuned signature;
13 months ago wenzelm 2018-05-28 clarified signature: Known.theories retains Document.Node.Entry (with header);
13 months ago wenzelm 2018-05-27 retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
13 months ago wenzelm 2018-05-27 clarified signature -- avoid confusion with Resources.is_hidden;
13 months ago wenzelm 2018-05-08 more robust: self-export only;
13 months ago wenzelm 2018-05-07 store exports within PIDE command state; Markup.Export.unapply: proper NAME;
14 months ago wenzelm 2018-05-02 purge history more thoroughly (see also 3156faac30a7);
15 months ago wenzelm 2018-03-24 clarified theory node name; purge_theories: return purged, retained; tuned documentation;
15 months ago wenzelm 2018-03-17 more position information;
15 months ago wenzelm 2018-03-11 update XML cache for slightly modified messages;
18 months ago wenzelm 2018-01-01 tuned signature;
18 months ago wenzelm 2017-12-28 tuned signature;
18 months ago wenzelm 2017-12-28 implicit thy_load context for bibtex files;
18 months ago wenzelm 2017-12-22 store full blob source for the sake of markup_to_XML;
18 months ago wenzelm 2017-12-22 PIDE markup for non-theory nodes;
18 months ago wenzelm 2017-12-22 tuned signature;
18 months ago wenzelm 2017-12-21 clarified signature;
19 months ago wenzelm 2017-12-01 tuned output;
19 months ago wenzelm 2017-12-01 removed inaccessible blobs from Document.Nodes;
19 months ago wenzelm 2017-12-01 purge hidden nodes more thoroughly: is_hidden may become true only later;
19 months ago wenzelm 2017-11-06 tuned signature;
20 months ago wenzelm 2017-10-12 more robust: allow Windows file names;
20 months ago wenzelm 2017-10-06 tuned signature;
21 months ago wenzelm 2017-09-29 tuned signature;
21 months ago wenzelm 2017-09-29 tuned signature;
22 months ago wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-06-26 wenzelm 2017-06-26 proper bootstrap_name (amending b42743f5b595);
2017-06-21 wenzelm 2017-06-21 tuned signature;
2017-06-19 wenzelm 2017-06-19 clarified signature;
2017-06-08 wenzelm 2017-06-08 tuned signature;
2017-06-08 wenzelm 2017-06-08 clarified signature;
2017-06-08 wenzelm 2017-06-08 HTML preview based on PIDE markup;
2017-04-12 wenzelm 2017-04-12 clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;
2017-04-08 wenzelm 2017-04-08 more qualifier treatment, but in the end it is still ignored;
2017-04-08 wenzelm 2017-04-08 more operations;
2017-04-08 wenzelm 2017-04-08 tuned signature;
2017-04-06 wenzelm 2017-04-06 tuned signature;
2017-04-03 wenzelm 2017-04-03 tuned signature;
2017-04-03 wenzelm 2017-04-03 simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
2017-04-03 wenzelm 2017-04-03 tuned;
2017-04-03 wenzelm 2017-04-03 tuned signature;
2017-03-20 wenzelm 2017-03-20 tuned signature;
2017-03-14 wenzelm 2017-03-14 more abstract module Document;
2017-03-12 wenzelm 2017-03-12 clarified current_command: index refers to node content, negative index means first command;
2017-03-12 wenzelm 2017-03-12 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
2017-03-12 wenzelm 2017-03-12 tuned;
2017-03-11 wenzelm 2017-03-11 tuned;
2017-01-10 wenzelm 2017-01-10 support "purge" operation on document model;
2017-01-09 wenzelm 2017-01-09 tuned signature;
2017-01-07 wenzelm 2017-01-07 uniform Document.Model.node_edits (without void edits);
2017-01-07 wenzelm 2017-01-07 obsolete;
2017-01-07 wenzelm 2017-01-07 tuned;
2017-01-06 wenzelm 2017-01-06 tuned;
2017-01-05 wenzelm 2017-01-05 misc tuning and clarification;