src/Pure/Tools/server_commands.scala
14 months ago wenzelm 2018-03-23 clarified signature -- eliminated somewhat pointless positions;
14 months ago wenzelm 2018-03-23 removed somewhat pointless argument;
15 months ago wenzelm 2018-03-23 field "kind" is always present, with default "writeln";
15 months ago wenzelm 2018-03-22 provide tmp_dir for server session;
15 months ago wenzelm 2018-03-22 clarified exported messages, e.g. suppress "information", "tracing"; export "legacy_feature" as "warning", in accordance to console default output;
15 months ago wenzelm 2018-03-22 clarified signature: prefer selective include_sessions;
15 months ago wenzelm 2018-03-22 clarified signature: more uniform session_id;
15 months ago wenzelm 2018-03-22 clarified signature;
15 months ago wenzelm 2018-03-22 clarified signature: do not expose somewhat accidental internal options;
15 months ago wenzelm 2018-03-21 clarified result;
15 months ago wenzelm 2018-03-21 clarified error result, without JSON object from "session_build"; clarified regular result;
15 months ago wenzelm 2018-03-21 clarified result;
15 months ago wenzelm 2018-03-18 more explicit error messages; clarified signature;
15 months ago wenzelm 2018-03-18 more explicit errors; tuned;
15 months ago wenzelm 2018-03-17 output result messages;
15 months ago wenzelm 2018-03-17 tuned signature;
15 months ago wenzelm 2018-03-16 prefer typed UUID;
15 months ago wenzelm 2018-03-16 unload_theories after consolidation -- reset node_required; proper node_perspective (amending 0d8e4e777973);
15 months ago wenzelm 2018-03-16 support for "use_theories";
15 months ago wenzelm 2018-03-16 clarified signature;
15 months ago wenzelm 2018-03-15 store session: per Server/Context, not Connection; support for "session_stop";
15 months ago wenzelm 2018-03-15 support for "session_start";
15 months ago wenzelm 2018-03-15 clarified default;
15 months ago wenzelm 2018-03-15 tuned;
15 months ago wenzelm 2018-03-14 asynchronous "session_build";
15 months ago wenzelm 2018-03-14 more informative JSON results;
15 months ago wenzelm 2018-03-13 more options;
15 months ago wenzelm 2018-03-13 allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
15 months ago wenzelm 2018-03-13 tuned signature;
15 months ago wenzelm 2018-03-13 added server command "session_build": similar to JEdit_Resources.session_build;