| 2019-01-06 |
wenzelm |
support for isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| 2019-01-04 |
wenzelm |
support for isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| 2019-01-03 |
wenzelm |
support for isabelle update -u inner_syntax_cartouches;
|
file |
diff |
annotate
|
| 2019-01-03 |
wenzelm |
support for "isabelle update -u mixfix_cartouches";
|
file |
diff |
annotate
|
| 2019-01-02 |
wenzelm |
more robust system channel via options that are private to the user;
|
file |
diff |
annotate
|
| 2018-12-27 |
wenzelm |
clarified defaults via system options;
|
file |
diff |
annotate
|
| 2018-12-08 |
wenzelm |
clarified defaults for Windows/Cygwin hybrid;
|
file |
diff |
annotate
|
| 2018-11-27 |
wenzelm |
adjusted to fc221fa79741;
|
file |
diff |
annotate
|
| 2018-10-02 |
wenzelm |
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
|
file |
diff |
annotate
|
| 2018-07-20 |
wenzelm |
added system option "strict_facts";
|
file |
diff |
annotate
|
| 2018-06-24 |
wenzelm |
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
|
file |
diff |
annotate
|
| 2018-06-05 |
wenzelm |
less wasteful consolidation, based on PIDE front-end state and recent changes;
|
file |
diff |
annotate
|
| 2018-06-02 |
wenzelm |
less frequent consolidation: it requires a full Document.update and Document.start_execution;
|
file |
diff |
annotate
|
| 2018-05-19 |
wenzelm |
support for build_database_server (PostgreSQL);
|
file |
diff |
annotate
|
| 2018-05-16 |
wenzelm |
clarified "consolidation" vs. "presentation";
|
file |
diff |
annotate
|
| 2018-05-14 |
wenzelm |
support for dynamic document output while editing;
|
file |
diff |
annotate
|
| 2018-05-11 |
wenzelm |
some export of foundational theory content;
|
file |
diff |
annotate
|
| 2018-05-09 |
wenzelm |
clarified future scheduling parameters, with support for parallel_limit;
|
file |
diff |
annotate
|
| 2018-03-02 |
wenzelm |
avoid hardwired parameters;
|
file |
diff |
annotate
|
| 2018-01-25 |
wenzelm |
more markup: disable spell-checker for raw latex;
|
file |
diff |
annotate
|
| 2018-01-09 |
wenzelm |
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
|
file |
diff |
annotate
|
| 2017-12-24 |
wenzelm |
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
|
file |
diff |
annotate
|
| 2017-12-13 |
wenzelm |
positions as postlude: avoid intrusion of odd %-forms into main tex source;
|
file |
diff |
annotate
|
| 2017-12-12 |
wenzelm |
option document_positions;
|
file |
diff |
annotate
|
| 2017-12-05 |
wenzelm |
system option for default command tags;
|
file |
diff |
annotate
|
| 2017-12-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2017-10-07 |
wenzelm |
theory qualifier is always session name (see also 31e8a86971a8);
|
file |
diff |
annotate
|
| 2017-08-08 |
wenzelm |
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
|
file |
diff |
annotate
|
| 2017-06-21 |
wenzelm |
tuned granularity of parallel tasks;
|
file |
diff |
annotate
|
| 2017-06-21 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 2017-05-08 |
wenzelm |
simplified default;
|
file |
diff |
annotate
|
| 2017-04-27 |
wenzelm |
support for database connection;
|
file |
diff |
annotate
|
| 2017-04-10 |
wenzelm |
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
|
file |
diff |
annotate
|
| 2017-04-09 |
wenzelm |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
file |
diff |
annotate
|
| 2017-03-15 |
wenzelm |
dynamic session_options for tuning parameters and initial prover options;
|
file |
diff |
annotate
|
| 2017-03-07 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 2017-02-26 |
wenzelm |
clarified defaults;
|
file |
diff |
annotate
|
| 2016-11-24 |
wenzelm |
explicit option editor_generated_input_delay, which is more aggressive by default;
|
file |
diff |
annotate
|
| 2016-10-20 |
wenzelm |
prevent sporadic disconnection;
|
file |
diff |
annotate
|
| 2016-10-19 |
wenzelm |
added system option "profiling";
|
file |
diff |
annotate
|
| 2016-10-10 |
wenzelm |
clarified treatment of options;
|
file |
diff |
annotate
|
| 2016-10-01 |
wenzelm |
options for process policy, notably for multiprocessor machines;
|
file |
diff |
annotate
|
| 2016-09-08 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
| 2016-04-06 |
wenzelm |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
file |
diff |
annotate
|
| 2016-04-05 |
wenzelm |
clarified bootstrap environment;
|
file |
diff |
annotate
|
| 2016-04-04 |
wenzelm |
option ML_system_unsafe;
|
file |
diff |
annotate
|
| 2016-04-01 |
wenzelm |
lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
|
file |
diff |
annotate
|
| 2016-04-01 |
wenzelm |
less bulky timing information, e.g. HOL 56913 ~> 672;
|
file |
diff |
annotate
|
| 2016-04-01 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| 2016-03-26 |
wenzelm |
avoid hardwired values;
|
file |
diff |
annotate
|
| 2016-03-02 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| 2016-02-25 |
wenzelm |
proper option process_output_tail, more generous default;
|
file |
diff |
annotate
|
| 2016-01-10 |
wenzelm |
prune old versions more often, to reduce overall heap requirements;
|
file |
diff |
annotate
|
| 2015-12-19 |
wenzelm |
prune old document versions more frequently, for reduced heap usage;
|
file |
diff |
annotate
|
| 2015-11-09 |
wenzelm |
prefer explicit State panel;
|
file |
diff |
annotate
|
| 2015-11-08 |
wenzelm |
added option timeout_scale;
|
file |
diff |
annotate
|
| 2015-11-07 |
wenzelm |
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
|
file |
diff |
annotate
|
| 2015-11-02 |
wenzelm |
clarified completion of Isabelle symbols within document source;
|
file |
diff |
annotate
|
| 2015-09-21 |
wenzelm |
option editor_output_state;
|
file |
diff |
annotate
|
| 2015-09-11 |
wenzelm |
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
|
file |
diff |
annotate
|
| 2015-08-11 |
wenzelm |
init/exit depending on active debugger panels;
|
file |
diff |
annotate
|
| 2015-08-10 |
wenzelm |
eliminated global option: breakpoints control this individually;
|
file |
diff |
annotate
|
| 2015-08-05 |
wenzelm |
more controls;
|
file |
diff |
annotate
|
| 2015-08-05 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-07-21 |
wenzelm |
support for ML debugger;
|
file |
diff |
annotate
|
| 2015-07-16 |
wenzelm |
added option ML_debugger;
|
file |
diff |
annotate
|
| 2015-04-15 |
wenzelm |
GUI controls for ML_statistics, for more digestible protocol dump;
|
file |
diff |
annotate
|
| 2015-01-29 |
wenzelm |
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
|
file |
diff |
annotate
|
| 2015-01-25 |
wenzelm |
discontinued obsolete option "document_graph";
|
file |
diff |
annotate
|
| 2014-12-22 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
file |
diff |
annotate
|
| 2014-10-31 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
file |
diff |
annotate
|
| 2014-08-13 |
wenzelm |
added option editor_syslog_limit;
|
file |
diff |
annotate
|
| 2014-08-05 |
wenzelm |
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
|
file |
diff |
annotate
|
| 2014-05-06 |
wenzelm |
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
|
file |
diff |
annotate
|
| 2014-04-25 |
wenzelm |
suppress potential dangerous option (see 1baa5d19ac44);
|
file |
diff |
annotate
|
| 2014-04-17 |
wenzelm |
tuned option name;
|
file |
diff |
annotate
|
| 2014-03-25 |
wenzelm |
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
|
file |
diff |
annotate
|
| 2014-03-24 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file |
diff |
annotate
|
| 2014-02-22 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
| 2013-08-25 |
wenzelm |
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
|
file |
diff |
annotate
|
| 2013-07-31 |
wenzelm |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
file |
diff |
annotate
|
| 2013-07-31 |
wenzelm |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
file |
diff |
annotate
|
| 2013-07-30 |
wenzelm |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
file |
diff |
annotate
|
| 2013-07-29 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2013-07-29 |
wenzelm |
afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
|
file |
diff |
annotate
|
| 2013-07-29 |
wenzelm |
support declarative editor_execution_range, instead of old-style check/cancel buttons;
|
file |
diff |
annotate
|
| 2013-07-27 |
wenzelm |
discontinued historic document formats;
|
file |
diff |
annotate
|
| 2013-07-20 |
wenzelm |
option editor_execution_priority;
|
file |
diff |
annotate
|
| 2013-07-20 |
wenzelm |
obscure options;
|
file |
diff |
annotate
|
| 2013-07-19 |
wenzelm |
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
|
file |
diff |
annotate
|
| 2013-07-18 |
wenzelm |
proper system options for 'find_theorems';
|
file |
diff |
annotate
|
| 2013-06-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-06-30 |
wenzelm |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
|
file |
diff |
annotate
|
| 2013-05-18 |
wenzelm |
explicit notion of public options, which are shown in the editor options dialog;
|
file |
diff |
annotate
|
| 2013-05-16 |
wenzelm |
more system options as context-sensitive config options;
|
file |
diff |
annotate
|
| 2013-05-16 |
wenzelm |
Thy_Output.modes as proper option;
|
file |
diff |
annotate
|
| 2013-05-13 |
wenzelm |
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
|
file |
diff |
annotate
|
| 2013-05-13 |
wenzelm |
option "goals_limit", with more uniform description;
|
file |
diff |
annotate
|
| 2013-03-27 |
wenzelm |
discontinued obsolete parallel_proofs_reuse_timing;
|
file |
diff |
annotate
|
| 2013-03-27 |
wenzelm |
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
|
file |
diff |
annotate
|
| 2013-03-27 |
wenzelm |
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
|
file |
diff |
annotate
|
| 2013-03-13 |
wenzelm |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
|
file |
diff |
annotate
|
| 2013-02-20 |
wenzelm |
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
|
file |
diff |
annotate
|
| 2013-01-22 |
wenzelm |
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
|
file |
diff |
annotate
|
| 2013-01-03 |
wenzelm |
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
|
file |
diff |
annotate
|
| 2013-01-03 |
wenzelm |
improved Monitor_Dockable, based on ML_Statistics operations;
|
file |
diff |
annotate
|
| 2012-12-13 |
wenzelm |
smarter handling of tracing messages: prover process pauses and enters user dialog;
|
file |
diff |
annotate
|
| 2012-12-10 |
wenzelm |
more generous tracing limit -- rescaled in MB;
|
file |
diff |
annotate
|
| 2012-11-28 |
wenzelm |
some support for ML runtime statistics;
|
file |
diff |
annotate
|
| 2012-11-18 |
wenzelm |
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
|
file |
diff |
annotate
|
| 2012-11-18 |
wenzelm |
more generous tracing_limit, with explicit system option;
|
file |
diff |
annotate
|
| 2012-09-22 |
wenzelm |
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
|
file |
diff |
annotate
|
| 2012-09-11 |
wenzelm |
more precise sections;
|
file |
diff |
annotate
|
| 2012-09-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-09-11 |
wenzelm |
more options;
|
file |
diff |
annotate
|
| 2012-09-11 |
wenzelm |
some support to organize options in sections;
|
file |
diff |
annotate
|
| 2012-08-14 |
wenzelm |
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
|
file |
diff |
annotate
|
| 2012-08-14 |
wenzelm |
clarified format of etc/options: only declarations, not re-definitions;
|
file |
diff |
annotate
|
| 2012-08-03 |
wenzelm |
timeout for session build job;
|
file |
diff |
annotate
|
| 2012-08-01 |
wenzelm |
explicit option skip_proofs;
|
file |
diff |
annotate
|