src/Pure/Tools/server_commands.scala
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;