src/Pure/PIDE/protocol.scala
2014-08-12 wenzelm 2014-08-12 generic process wrapping in Prover; clarified module arrangement;
2014-08-12 wenzelm 2014-08-12 clarified Position.Identified: do not require range from prover, default to command position;
2014-08-02 wenzelm 2014-08-02 proper priority for error over warning also for node_status (see 9c5220e05e04);
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-17 wenzelm 2014-04-17 added protocol command "use_theories", with core functionality of batch build;
2014-04-09 wenzelm 2014-04-09 more explicit message discrimination;
2014-04-08 wenzelm 2014-04-08 more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
2014-04-08 wenzelm 2014-04-08 accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
2014-04-08 wenzelm 2014-04-08 avoid data redundancy;
2014-04-08 wenzelm 2014-04-08 tuned signature -- moved Command.Chunk to Text.Chunk;
2014-04-08 wenzelm 2014-04-08 more explicit Command.Chunk types, less ooddities; tuned;
2014-04-07 wenzelm 2014-04-07 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
2014-04-07 wenzelm 2014-04-07 support for URL as file name, similar to treatment in jEdit.java;
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;