src/Pure/PIDE/protocol.scala
2014-04-07 wenzelm 2014-04-07 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-04-03 wenzelm 2014-04-03 more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned;
2014-04-03 wenzelm 2014-04-03 more general prover operations;
2014-04-02 wenzelm 2014-04-02 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;
2014-04-02 wenzelm 2014-04-02 persistent protocol_status, to improve performance of node_status a little;
2014-04-01 wenzelm 2014-04-01 tuned for-comprehensions -- less structure mapping;
2014-04-01 wenzelm 2014-04-01 some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
2014-04-01 wenzelm 2014-04-01 unused;
2014-04-01 wenzelm 2014-04-01 more frugal command_status, which is often used in a tight loop;
2014-03-31 wenzelm 2014-03-31 store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index;
2014-03-27 wenzelm 2014-03-27 back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
2014-03-27 wenzelm 2014-03-27 more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;
2014-03-26 wenzelm 2014-03-26 clarified valid_id: always standardize towards static command.id;
2014-03-03 wenzelm 2014-03-03 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
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;
2014-03-01 wenzelm 2014-03-01 tuned signature -- more explicit Document.Elements;
2014-02-27 wenzelm 2014-02-27 more formal Document.Blobs; removed junk;
2014-02-21 wenzelm 2014-02-21 tuned signature;
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;
2014-02-12 wenzelm 2014-02-12 clarified message_positions: cover alt_id as well; tuned;
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;
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;
2014-02-11 wenzelm 2014-02-11 report (but ignore) markup within auxiliary files;
2013-11-22 wenzelm 2013-11-22 clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-20 wenzelm 2013-11-20 load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;
2013-11-19 wenzelm 2013-11-19 more explicit indication of missing files;
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;
2013-11-19 wenzelm 2013-11-19 clarified boundary cases of Document.Node.Name;
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;
2013-08-09 wenzelm 2013-08-09 cancel_query via direct access to the exec_id of the running query process;
2013-08-05 wenzelm 2013-08-05 tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-02 wenzelm 2013-08-02 maintain overlays within node perspective; tuned signature;
2013-07-31 wenzelm 2013-07-31 allow explicit indication of required node: full eval, no prints;
2013-07-29 wenzelm 2013-07-29 obsolete;
2013-07-13 wenzelm 2013-07-13 more rendering for information messages;
2013-07-10 wenzelm 2013-07-10 tuned signature;
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;