src/Pure/Thy/sessions.scala
11 months ago wenzelm 2018-05-17 clarified signature;
11 months ago wenzelm 2018-05-13 tuned signature;
11 months ago wenzelm 2018-05-05 cleanup session output before starting build job; tuned signature;
12 months ago wenzelm 2018-04-20 support for XZ.Cache;
13 months ago wenzelm 2018-03-22 clarified signature: prefer selective include_sessions;
13 months ago wenzelm 2018-03-16 tuned signature;
13 months ago wenzelm 2018-03-15 support for "session_start";
13 months ago wenzelm 2018-03-13 allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
13 months ago wenzelm 2018-03-13 tuned;
15 months ago wenzelm 2018-01-23 treat sessions as entities with defining position; tuned signature;
15 months ago wenzelm 2018-01-19 formal treatment of documentation names;
16 months ago wenzelm 2017-12-29 formal check of @{cite} bibtex entries -- only in batch-mode session builds;
16 months ago wenzelm 2017-12-28 implicit thy_load context for bibtex files;
16 months ago wenzelm 2017-12-28 avoid clash with special files in HTML output;
16 months ago wenzelm 2017-12-28 tuned signature;
16 months ago wenzelm 2017-12-16 added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
16 months ago wenzelm 2017-12-16 disallow theory name "ROOT";
16 months ago wenzelm 2017-12-16 PIDE markup for session ROOT files;
16 months ago wenzelm 2017-12-16 tuned;
17 months ago wenzelm 2017-11-27 retain files in Pure.thy, notably $POLYML_EXE;
17 months ago wenzelm 2017-11-12 tuned signature;
17 months ago wenzelm 2017-11-12 tuned;
17 months ago wenzelm 2017-11-12 tuned signature;
17 months ago wenzelm 2017-11-07 clarified signature (again);
17 months ago wenzelm 2017-11-07 clarified exclusion: operate on completed selection, as last step;
17 months ago wenzelm 2017-11-07 tuned;
17 months ago wenzelm 2017-11-07 tuned signature;
17 months ago wenzelm 2017-11-07 clarifified selection: always wrt. build_graph structure; tuned signature;
17 months ago wenzelm 2017-11-07 tuned;
17 months ago wenzelm 2017-11-07 tuned signature;
17 months ago wenzelm 2017-11-07 backed out odd "bug fix" 671decd2e627;
17 months ago wenzelm 2017-11-05 uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");
17 months ago wenzelm 2017-11-04 clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
17 months ago wenzelm 2017-11-02 proper deps;
17 months ago wenzelm 2017-11-02 allow unrelated ancestor; clarified error;
17 months ago wenzelm 2017-11-02 support alternative ancestor session;
17 months ago wenzelm 2017-11-02 support focus_session, for much faster startup of Isabelle/jEdit; more options for "isabelle jedit";
17 months ago wenzelm 2017-11-01 init only once (see also c0f776b661fa);
17 months ago wenzelm 2017-11-01 clarified terminology;
17 months ago wenzelm 2017-11-01 tuned signature;
17 months ago wenzelm 2017-11-01 do not store bulky Session.Deps;
17 months ago wenzelm 2017-11-01 avoid duplicate invocation of expensive Sessions.deps on full_sessions; tuned;
17 months ago wenzelm 2017-11-01 clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
17 months ago wenzelm 2017-10-31 removed unused option, which is potentially expensive;
17 months ago wenzelm 2017-10-31 allow to augment session context via explicit session infos; more compact required_session interface;
17 months ago wenzelm 2017-10-31 synthesize session with all required theories from other session imports;
17 months ago wenzelm 2017-10-31 clarified signature;
17 months ago wenzelm 2017-10-31 clarified signature;
17 months ago wenzelm 2017-10-31 clarified signature;
17 months ago wenzelm 2017-10-31 clarified signature;
17 months ago wenzelm 2017-10-31 clarified signature: global_theories is always required;
17 months ago wenzelm 2017-10-31 tuned signature;
17 months ago wenzelm 2017-10-31 clarified modules;
17 months ago wenzelm 2017-10-31 more permissive: db could be empty after hard crash;
18 months ago wenzelm 2017-10-25 uniform system name;
18 months ago wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
18 months ago wenzelm 2017-10-13 tuned signature;
18 months ago wenzelm 2017-10-12 clarified signature;
18 months ago wenzelm 2017-10-11 clarified meta_digest;
18 months ago wenzelm 2017-10-10 tuned signature;