#
4accdc79 |
|
26-Jun-2018 |
wenzelm <none@none> |
clarified default tag;
|
#
76687af0 |
|
09-May-2018 |
wenzelm <none@none> |
clarified future scheduling parameters, with support for parallel_limit;
|
#
c30e7616 |
|
23-Mar-2018 |
wenzelm <none@none> |
clarified signature;
|
#
ce46cbd0 |
|
17-Feb-2018 |
wenzelm <none@none> |
clarified apply_transaction: always continue without presentation context;
|
#
681db600 |
|
17-Feb-2018 |
wenzelm <none@none> |
more tight presentation context: avoid storing full Toplevel.state;
|
#
dd95e644 |
|
17-Feb-2018 |
wenzelm <none@none> |
tuned;
|
#
d76dbb2f |
|
09-Jan-2018 |
wenzelm <none@none> |
tuned;
|
#
4a7359d1 |
|
09-Jan-2018 |
wenzelm <none@none> |
clarified signature;
|
#
0818907f |
|
09-Jan-2018 |
wenzelm <none@none> |
clarified presentation_state with provide presentation_context;
|
#
e426fcb2 |
|
08-Jan-2018 |
wenzelm <none@none> |
theory Pure is default presentation context;
|
#
adde51ce |
|
08-Jan-2018 |
wenzelm <none@none> |
more operations;
|
#
d0b0dba4 |
|
08-Dec-2017 |
wenzelm <none@none> |
uniform use of original theory;
|
#
55072b15 |
|
07-Dec-2017 |
wenzelm <none@none> |
clarified document preparation vs. skip_proofs;
|
#
75cec52e |
|
22-Jun-2017 |
wenzelm <none@none> |
keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
|
#
0cd99dde |
|
27-May-2017 |
wenzelm <none@none> |
clarified build errors; tuned signature;
|
#
37144cf5 |
|
27-Feb-2017 |
wenzelm <none@none> |
clarified priority: zero can mean unknown/long or irrelevant/short time;
|
#
52f6df00 |
|
27-Feb-2017 |
wenzelm <none@none> |
absent timing information means zero, according to 0070053570c4, f235646b1b73;
|
#
c04afceb |
|
26-Feb-2017 |
wenzelm <none@none> |
tuned;
|
#
b7f74ad2 |
|
06-Apr-2016 |
wenzelm <none@none> |
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
|
#
85397651 |
|
06-Apr-2016 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
185dcd47 |
|
02-Apr-2016 |
wenzelm <none@none> |
prefer infix operations;
|
#
fd5f3b5a |
|
02-Apr-2016 |
wenzelm <none@none> |
careful export of type-dependent functions, without losing their special status;
|
#
13be7d54 |
|
18-Mar-2016 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
dccdabe3 |
|
03-Mar-2016 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
8560932a |
|
24-Jan-2016 |
wenzelm <none@none> |
tuned;
|
#
888c8f12 |
|
21-Dec-2015 |
wenzelm <none@none> |
discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
|
#
5c547f6f |
|
21-Sep-2015 |
wenzelm <none@none> |
separate panel for proof state output;
|
#
9804fe0f |
|
11-Aug-2015 |
wenzelm <none@none> |
default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
|
#
2aaba9d6 |
|
08-Jul-2015 |
wenzelm <none@none> |
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
|
#
4a6b649b |
|
08-Jun-2015 |
wenzelm <none@none> |
tuned signature;
|
#
28f987ab |
|
03-May-2015 |
wenzelm <none@none> |
tuned output;
|
#
3a3f0be1 |
|
16-Apr-2015 |
wenzelm <none@none> |
discontinued pointless warnings: commands are only defined inside a theory context;
|
#
e987af3c |
|
16-Apr-2015 |
wenzelm <none@none> |
explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
|
#
84201dd7 |
|
15-Apr-2015 |
wenzelm <none@none> |
tuned messages;
|
#
886ea47b |
|
09-Apr-2015 |
wenzelm <none@none> |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
#
078f3395 |
|
06-Apr-2015 |
wenzelm <none@none> |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
#
cc8cd554 |
|
04-Apr-2015 |
wenzelm <none@none> |
support private scope for individual local theory commands; tuned signature;
|
#
fd61f512 |
|
29-Jan-2015 |
wenzelm <none@none> |
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
|
#
986c7f6c |
|
23-Dec-2014 |
wenzelm <none@none> |
explicit message channels for "state", "information"; separate state_message_color;
|
#
2c211c06 |
|
18-Dec-2014 |
wenzelm <none@none> |
tuned;
|
#
8560c674 |
|
26-Nov-2014 |
wenzelm <none@none> |
more informative failure of protocol commands, with exception trace; eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
|
#
fc752d1a |
|
22-Nov-2014 |
wenzelm <none@none> |
tuned;
|
#
5c6dcf99 |
|
22-Apr-2015 |
wenzelm <none@none> |
allow diagnostic proof commands with skip_proofs;
|
#
d552e1f7 |
|
22-Apr-2015 |
wenzelm <none@none> |
tuned signature;
|
#
8acf1ce1 |
|
13-Nov-2014 |
wenzelm <none@none> |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
|
#
7ecf819b |
|
06-Nov-2014 |
wenzelm <none@none> |
more explicit Keyword.keywords;
|
#
7ee8e540 |
|
03-Nov-2014 |
wenzelm <none@none> |
eliminated unused int_only flag (see also c12484a27367); just proper commands;
|
#
0af3db43 |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued pointless option: timing is always on (overall theory only);
|
#
6a91b9f6 |
|
31-Oct-2014 |
wenzelm <none@none> |
eliminated odd flags and hook;
|
#
5d6e2a9a |
|
28-Oct-2014 |
wenzelm <none@none> |
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
|
#
cecfb7c0 |
|
28-Oct-2014 |
wenzelm <none@none> |
tuned;
|
#
8fd9cfb1 |
|
02-Jul-2014 |
haftmann <none@none> |
centralized (ad-hoc) switching of targets in named_target.ML
|
#
a4e8c0bc |
|
07-Jun-2014 |
haftmann <none@none> |
avoid odd Named_Target.reinit altogether
|
#
92967cd1 |
|
07-Jun-2014 |
haftmann <none@none> |
clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
|
#
3497efa5 |
|
11-May-2014 |
wenzelm <none@none> |
smarter recovery from toplevel type error;
|
#
215ced67 |
|
07-May-2014 |
wenzelm <none@none> |
print results as "state", to avoid intrusion into the source text; print new local theory (again);
|
#
5a8ba8c2 |
|
06-May-2014 |
wenzelm <none@none> |
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
|
#
5e76789a |
|
07-May-2014 |
wenzelm <none@none> |
tuned;
|
#
da822448 |
|
06-May-2014 |
wenzelm <none@none> |
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
|
#
82b8eca8 |
|
05-May-2014 |
wenzelm <none@none> |
more print operations; preserve declaration order;
|
#
c33d72e8 |
|
30-Mar-2014 |
wenzelm <none@none> |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
#
52dd9fc9 |
|
27-Mar-2014 |
wenzelm <none@none> |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
#
14f462d6 |
|
23-Mar-2014 |
wenzelm <none@none> |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
#
538e72a6 |
|
14-Mar-2014 |
wenzelm <none@none> |
prefer more robust Synchronized.var;
|
#
f5271040 |
|
12-Mar-2014 |
wenzelm <none@none> |
more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);
|
#
cf6a018b |
|
11-Mar-2014 |
wenzelm <none@none> |
slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;
|
#
fa0c0017 |
|
13-Feb-2014 |
wenzelm <none@none> |
tuned whitespace;
|
#
abf17c72 |
|
05-Dec-2013 |
wenzelm <none@none> |
more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash; tuned signature;
|
#
38b673d6 |
|
11-Nov-2013 |
wenzelm <none@none> |
tuned signature;
|
#
a5c5c033 |
|
18-Sep-2013 |
wenzelm <none@none> |
improved printing of exception trace in Poly/ML 5.5.1;
|
#
cbc61f82 |
|
04-Sep-2013 |
wenzelm <none@none> |
some explicit indication of Proof General legacy;
|
#
72d291e6 |
|
25-Aug-2013 |
wenzelm <none@none> |
maintain goal forks as part of global execution; tuned;
|
#
41e5cc9f |
|
25-Aug-2013 |
wenzelm <none@none> |
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;
|
#
42e9b2b9 |
|
30-Jul-2013 |
wenzelm <none@none> |
type theory is purely value-oriented;
|
#
f9d3edb3 |
|
18-Jul-2013 |
wenzelm <none@none> |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
#
d36e9fa6 |
|
09-Jul-2013 |
wenzelm <none@none> |
tuned message;
|
#
96559435 |
|
05-Jul-2013 |
wenzelm <none@none> |
tuned signature; tuned comments;
|
#
4f5ef9b1 |
|
04-Jul-2013 |
wenzelm <none@none> |
separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
|
#
709e149c |
|
02-Jul-2013 |
wenzelm <none@none> |
clarified Proofterm.proofs vs. Goal.skip_proofs;
|
#
d01ca9c0 |
|
22-May-2013 |
haftmann <none@none> |
mark local theory as brittle also after interpretation inside locales; more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1; check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory
|
#
a3273c1a |
|
23-Apr-2013 |
haftmann <none@none> |
brittleness stamping for local theories
|
#
e5854438 |
|
09-Apr-2013 |
wenzelm <none@none> |
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
|
#
844a3500 |
|
09-Apr-2013 |
wenzelm <none@none> |
clarified protocol_message undefinedness;
|
#
59410e28 |
|
09-Apr-2013 |
wenzelm <none@none> |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
|
#
0a822a6c |
|
03-Apr-2013 |
wenzelm <none@none> |
more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);
|
#
546881d7 |
|
02-Apr-2013 |
wenzelm <none@none> |
more centralized command timing; clarified old-style timing message;
|
#
c30035b6 |
|
27-Mar-2013 |
wenzelm <none@none> |
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
|
#
78cb32ef |
|
27-Mar-2013 |
wenzelm <none@none> |
explicit Toplevel.is_skipped_proof; tuned;
|
#
6c1c54c1 |
|
27-Mar-2013 |
wenzelm <none@none> |
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);
|
#
a51e1a99 |
|
13-Mar-2013 |
wenzelm <none@none> |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
|
#
62aa686d |
|
04-Mar-2013 |
wenzelm <none@none> |
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
|
#
317de656 |
|
03-Mar-2013 |
wenzelm <none@none> |
uniform treatment of global/local proofs; tuned;
|
#
54b08062 |
|
03-Mar-2013 |
wenzelm <none@none> |
tuned;
|
#
d7e2ac96 |
|
03-Mar-2013 |
wenzelm <none@none> |
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
|
#
39dac1c0 |
|
03-Mar-2013 |
wenzelm <none@none> |
more Thy_Syntax.element operations;
|
#
0222c19f |
|
28-Feb-2013 |
wenzelm <none@none> |
simplified Proof.future_proof;
|
#
8c5f0726 |
|
26-Feb-2013 |
wenzelm <none@none> |
tuned signature;
|
#
78d2aea3 |
|
26-Feb-2013 |
wenzelm <none@none> |
fork diagnostic commands (theory loader and PIDE interaction); explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions; clarified Toplevel.command_exception vs. Toplevel.command_errors;
|
#
3cd6b4e8 |
|
26-Feb-2013 |
wenzelm <none@none> |
tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;
|
#
69c4457f |
|
26-Feb-2013 |
wenzelm <none@none> |
tuned;
|
#
78ed9be7 |
|
25-Feb-2013 |
wenzelm <none@none> |
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
|
#
805825a8 |
|
24-Feb-2013 |
wenzelm <none@none> |
clarified Toplevel.element_result: scheduling policies happen here; tuned;
|
#
2e1647c0 |
|
24-Feb-2013 |
wenzelm <none@none> |
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;
|
#
d5ac502c |
|
22-Feb-2013 |
wenzelm <none@none> |
make SML/NJ happy;
|
#
7037fae5 |
|
22-Feb-2013 |
wenzelm <none@none> |
eliminated hard tabs;
|
#
763d331c |
|
21-Feb-2013 |
wenzelm <none@none> |
highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;
|
#
9826d1f7 |
|
20-Feb-2013 |
wenzelm <none@none> |
more tight representation of command timing; tuned signatures; tuned;
|
#
e1659af1 |
|
20-Feb-2013 |
wenzelm <none@none> |
proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
|
#
ae896787 |
|
19-Feb-2013 |
wenzelm <none@none> |
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
|
#
8a4825f7 |
|
19-Feb-2013 |
wenzelm <none@none> |
suppress timing message in full PIDE protocol -- this is for batch build;
|
#
d6677e67 |
|
18-Feb-2013 |
wenzelm <none@none> |
support for prescient timing information within command transactions;
|
#
c388a45c |
|
19-Feb-2013 |
wenzelm <none@none> |
emit command_timing properties into build log; tuned;
|
#
a616fe27 |
|
16-Jan-2013 |
wenzelm <none@none> |
tuned signature;
|
#
f88ad9ae |
|
05-Jan-2013 |
wenzelm <none@none> |
more precise Local_Theory.level: 1 really means main target and >= 2 nested context; explicit target for context within global theory with after_close = exit to manage the 2 levels involved here; reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;
|
#
95d64a2f |
|
25-Nov-2012 |
wenzelm <none@none> |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
#
cad7aeb9 |
|
16-Oct-2012 |
wenzelm <none@none> |
more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
|
#
6141f390 |
|
01-Sep-2012 |
wenzelm <none@none> |
discontinued complicated/unreliable notion of recent proofs within context;
|
#
8fddcc7f |
|
31-Aug-2012 |
wenzelm <none@none> |
more precise register_proofs for local goals; tuned signature;
|
#
4613547d |
|
30-Aug-2012 |
wenzelm <none@none> |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
|
#
91fcdd2b |
|
30-Aug-2012 |
wenzelm <none@none> |
some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
|
#
69fc4752 |
|
30-Aug-2012 |
wenzelm <none@none> |
tuned signature;
|
#
56bc6c93 |
|
28-Aug-2012 |
wenzelm <none@none> |
tuned signature;
|
#
871b69bc |
|
29-Aug-2012 |
wenzelm <none@none> |
renamed Position.str_of to Position.here;
|
#
39606e42 |
|
11-Aug-2012 |
wenzelm <none@none> |
vacuous execution after first malformed command;
|
#
b2b09f5e |
|
01-Aug-2012 |
wenzelm <none@none> |
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
|
#
3be68435 |
|
17-May-2012 |
wenzelm <none@none> |
tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
|
#
28e907fb |
|
11-Apr-2012 |
wenzelm <none@none> |
clarified proof_result: finish proof formally via head tr, not end_tr;
|
#
5f2a35d0 |
|
10-Apr-2012 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
0f847227 |
|
10-Apr-2012 |
wenzelm <none@none> |
static relevance of proof via syntax keywords;
|
#
fceb8991 |
|
02-Apr-2012 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
2219eb0c |
|
21-Mar-2012 |
wenzelm <none@none> |
more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;
|
#
fd6d7f5e |
|
16-Mar-2012 |
wenzelm <none@none> |
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
|
#
99fd6f8e |
|
28-Nov-2011 |
wenzelm <none@none> |
separate module for concrete Isabelle markup; --HG-- rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala
|
#
b8a07b69 |
|
14-Nov-2011 |
wenzelm <none@none> |
pass positions for named targets, for formal links in the document model;
|
#
c0dd86bf |
|
19-Aug-2011 |
wenzelm <none@none> |
maintain recent future proofs at transaction boundaries;
|
#
8876e929 |
|
18-Aug-2011 |
wenzelm <none@none> |
more careful treatment of exception serial numbers, with propagation to message channel;
|
#
d913d68c |
|
15-Aug-2011 |
wenzelm <none@none> |
tuned error message;
|
#
64dd353c |
|
13-Aug-2011 |
wenzelm <none@none> |
clarified Toplevel.end_theory;
|
#
8428c174 |
|
13-Aug-2011 |
wenzelm <none@none> |
simplified Toplevel.init_theory: discontinued special name argument;
|
#
a9635b14 |
|
13-Aug-2011 |
wenzelm <none@none> |
simplified Toplevel.init_theory: discontinued special master argument;
|
#
424e1a73 |
|
13-Aug-2011 |
wenzelm <none@none> |
provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
|
#
cb6b88ef |
|
05-Jul-2011 |
wenzelm <none@none> |
get theory from last executation state; tuned error messages;
|
#
472284a2 |
|
05-Jul-2011 |
wenzelm <none@none> |
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example); reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);
|
#
d93eb505 |
|
05-Jul-2011 |
wenzelm <none@none> |
tuned signature; tuned;
|
#
87db399e |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
de7d7e3d |
|
26-Mar-2011 |
wenzelm <none@none> |
present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
|
#
8b04ee36 |
|
20-Mar-2011 |
wenzelm <none@none> |
structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
|
#
9634e29a |
|
04-Feb-2011 |
wenzelm <none@none> |
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
|
#
ea3105a6 |
|
31-Jan-2011 |
wenzelm <none@none> |
tuned signature; tuned vacous forks;
|
#
dbeb61d4 |
|
31-Jan-2011 |
wenzelm <none@none> |
support named tasks, for improved tracing;
|
#
4b0af333 |
|
13-Jan-2011 |
wenzelm <none@none> |
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
|
#
82abb8f6 |
|
04-Dec-2010 |
wenzelm <none@none> |
formal notepad without any result;
|
#
93623054 |
|
25-Oct-2010 |
wenzelm <none@none> |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
#
f6fdda62 |
|
17-Sep-2010 |
wenzelm <none@none> |
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
|
#
49ff537a |
|
10-Sep-2010 |
wenzelm <none@none> |
avoid extra wrapping for interrupts;
|
#
da570543 |
|
09-Sep-2010 |
wenzelm <none@none> |
removed dead code;
|
#
ad727922 |
|
09-Sep-2010 |
wenzelm <none@none> |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
#
0c97de14 |
|
31-Aug-2010 |
wenzelm <none@none> |
moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;
|
#
127443d2 |
|
30-Aug-2010 |
wenzelm <none@none> |
Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.; simplified Toplevel.error_msg;
|
#
7e04636f |
|
30-Aug-2010 |
wenzelm <none@none> |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
#
90963f01 |
|
25-Aug-2010 |
wenzelm <none@none> |
added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;
|
#
71c5a06b |
|
12-Aug-2010 |
haftmann <none@none> |
named target is optional; explicit Name_Target.reinit
|
#
be4c7e28 |
|
12-Aug-2010 |
haftmann <none@none> |
Named_Target.init: empty string represents theory target
|
#
60e1cdc3 |
|
12-Aug-2010 |
haftmann <none@none> |
Named_Target.theory_init
|
#
f90b529e |
|
11-Aug-2010 |
wenzelm <none@none> |
removed obsolete Toplevel.enter_proof_body;
|
#
bba4d42e |
|
11-Aug-2010 |
haftmann <none@none> |
avoid arcane Local_Theory.reinit entirely
|
#
2fa88f89 |
|
11-Aug-2010 |
haftmann <none@none> |
renamed Theory_Target to the more appropriate Named_Target --HG-- rename : src/Pure/Isar/theory_target.ML => src/Pure/Isar/named_target.ML
|
#
94f5d2a8 |
|
08-Aug-2010 |
wenzelm <none@none> |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
#
a68ec6c9 |
|
27-Jul-2010 |
wenzelm <none@none> |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;
|
#
191931fb |
|
25-Jul-2010 |
wenzelm <none@none> |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
#
2eeaf486 |
|
24-Jul-2010 |
wenzelm <none@none> |
tuned;
|
#
ca940030 |
|
24-Jul-2010 |
wenzelm <none@none> |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
#
17192db8 |
|
23-Jul-2010 |
wenzelm <none@none> |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
|
#
fe24dbbe |
|
22-Jul-2010 |
wenzelm <none@none> |
tuned signature;
|
#
fab6209d |
|
22-Jul-2010 |
wenzelm <none@none> |
eliminated some unreferenced identifiers;
|
#
19801ae0 |
|
22-Jul-2010 |
wenzelm <none@none> |
tuned;
|
#
f5d9ac9e |
|
21-Jul-2010 |
wenzelm <none@none> |
clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
|
#
d27889c6 |
|
20-Jul-2010 |
wenzelm <none@none> |
avoid duplicate printing of 'theory' state (cf. 173974e07dea);
|
#
acdcfe16 |
|
20-Jul-2010 |
wenzelm <none@none> |
toplevel pp for Proof.state and Toplevel.state;
|
#
309120d5 |
|
20-Jul-2010 |
wenzelm <none@none> |
Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
|
#
fceeb9a3 |
|
20-Jul-2010 |
wenzelm <none@none> |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;
|
#
a470a4aa |
|
05-Jul-2010 |
wenzelm <none@none> |
async_state: report within proper transaction context;
|
#
8d59a033 |
|
04-Jul-2010 |
wenzelm <none@none> |
general Future.report -- also for Toplevel.async_state;
|
#
a1bb34cc |
|
03-Jul-2010 |
wenzelm <none@none> |
run_command: actually observe "print" flag;
|
#
40677146 |
|
03-Jul-2010 |
wenzelm <none@none> |
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
|
#
c25c5530 |
|
31-May-2010 |
wenzelm <none@none> |
modernized some structure names, keeping a few legacy aliases;
|
#
7c58af00 |
|
31-May-2010 |
wenzelm <none@none> |
Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
|
#
6f878766 |
|
15-May-2010 |
wenzelm <none@none> |
refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
|
#
eda71e13 |
|
26-Apr-2010 |
wenzelm <none@none> |
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
|
#
99c1c459 |
|
23-Apr-2010 |
wenzelm <none@none> |
added keyword category "schematic goal", which prevents any attempt to fork the proof;
|
#
16fa875c |
|
18-Feb-2010 |
wenzelm <none@none> |
removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;
|
#
88c1a772 |
|
17-Nov-2009 |
wenzelm <none@none> |
init_theory: Runtime.controlled_execution for proper exception trace etc.;
|
#
e8e991b6 |
|
17-Nov-2009 |
wenzelm <none@none> |
implicit name space grouping for theory/local_theory transactions;
|
#
d28e2372 |
|
13-Nov-2009 |
wenzelm <none@none> |
modernized structure Local_Theory;
|
#
831d9f95 |
|
10-Nov-2009 |
wenzelm <none@none> |
Toplevel.thread provides Isar-style exception output;
|
#
8ce10e6a |
|
10-Nov-2009 |
wenzelm <none@none> |
modernized structure Theory_Target;
|
#
dfa769e1 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Generic_Data, Proof_Data; tuned;
|
#
da0f6c0f |
|
02-Nov-2009 |
wenzelm <none@none> |
modernized structure Proof_Node;
|
#
f0b808aa |
|
27-Oct-2009 |
wenzelm <none@none> |
non-critical atomic accesses;
|
#
81721859 |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated dead code; eliminated redundant parameters;
|
#
b9d789f1 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
c484a78c |
|
19-Jul-2009 |
wenzelm <none@none> |
Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);
|
#
42e5a525 |
|
19-Jul-2009 |
wenzelm <none@none> |
more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
|
#
fb305543 |
|
06-Jun-2009 |
wenzelm <none@none> |
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
|
#
50da439a |
|
04-Jun-2009 |
wenzelm <none@none> |
exn_message/raised: ML_Compiler.exception_position;
|
#
18bdca40 |
|
30-Mar-2009 |
wenzelm <none@none> |
added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
|
#
eca9a0a2 |
|
21-Mar-2009 |
wenzelm <none@none> |
restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
|
#
874fbaed |
|
18-Mar-2009 |
wenzelm <none@none> |
reduced verbosity;
|
#
b09103a4 |
|
11-Mar-2009 |
wenzelm <none@none> |
debugging: special handling of EXCURSION_FAIL;
|
#
9e7d52c9 |
|
10-Mar-2009 |
wenzelm <none@none> |
controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;
|
#
bfdc9b8e |
|
09-Mar-2009 |
wenzelm <none@none> |
simplified presentation_context_of;
|
#
a6451629 |
|
08-Mar-2009 |
wenzelm <none@none> |
simplified presentation: built into transaction, pass state directly;
|
#
83870f17 |
|
16-Jan-2009 |
wenzelm <none@none> |
run_command: check theory name for init;
|
#
e76c08e4 |
|
14-Jan-2009 |
wenzelm <none@none> |
added run_command (from isar_document.ML); tuned;
|
#
dd3ba59a |
|
11-Jan-2009 |
wenzelm <none@none> |
added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
|
#
9b85e38a |
|
10-Jan-2009 |
wenzelm <none@none> |
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
|
#
0c370e41 |
|
10-Jan-2009 |
wenzelm <none@none> |
excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;
|
#
caffd45c |
|
07-Jan-2009 |
wenzelm <none@none> |
Proof.global_future_proof;
|
#
18fdfb56 |
|
06-Jan-2009 |
wenzelm <none@none> |
added local_theory';
|
#
90ff3c57 |
|
03-Jan-2009 |
wenzelm <none@none> |
future proofs: back to Future.fork_pri ~1 for improved parallelism;
|
#
11e4f4e9 |
|
16-Dec-2008 |
wenzelm <none@none> |
future proofs: Future.fork_pri 1 minimizes queue length and pending promises -- slight improvement of throughput, at the cost of a bit of parallelism;
|
#
e83af91c |
|
16-Dec-2008 |
wenzelm <none@none> |
Future.fork_pri;
|
#
66497106 |
|
11-Dec-2008 |
wenzelm <none@none> |
removed spurious exception_trace;
|
#
86fa3e42 |
|
11-Dec-2008 |
wenzelm <none@none> |
export context_node;
|
#
bb697f45 |
|
05-Dec-2008 |
wenzelm <none@none> |
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
|
#
7caf843d |
|
04-Dec-2008 |
wenzelm <none@none> |
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
|
#
8522e5b6 |
|
21-Oct-2008 |
wenzelm <none@none> |
added Future.enabled check;
|
#
cc6ef777 |
|
09-Oct-2008 |
wenzelm <none@none> |
Multithreading.enabled;
|
#
29517154 |
|
02-Oct-2008 |
wenzelm <none@none> |
program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
|
#
f3648ae5 |
|
02-Oct-2008 |
wenzelm <none@none> |
simplified Exn.EXCEPTIONS;
|
#
30ad3fa4 |
|
01-Oct-2008 |
wenzelm <none@none> |
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; tuned;
|
#
02c01f70 |
|
01-Oct-2008 |
wenzelm <none@none> |
datatype transition: internal trans field is maintained in reverse order; tuned;
|
#
b2cc1b1e |
|
30-Sep-2008 |
wenzelm <none@none> |
renamed promise to future, tuned related interfaces;
|
#
7298aeec |
|
30-Sep-2008 |
wenzelm <none@none> |
more robust treatment of Interrupt (cf. exn.ML);
|
#
a7dc84dd |
|
30-Sep-2008 |
wenzelm <none@none> |
begin_proof: avoid race condition wrt. skip_proofs flag; replaced command_excursion by excursion, which is based on units of command/proof pairs; excursion: basic support for proof promises;
|
#
78cd7f72 |
|
30-Sep-2008 |
wenzelm <none@none> |
export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;
|
#
5dbe4f0d |
|
29-Sep-2008 |
wenzelm <none@none> |
LocalTheory.exit_global;
|
#
6b116bf7 |
|
03-Sep-2008 |
wenzelm <none@none> |
added pos_of;
|
#
27f3e697 |
|
03-Sep-2008 |
wenzelm <none@none> |
simplified Toplevel.add_hook: cover successful transactions only;
|
#
d323dd30 |
|
02-Sep-2008 |
wenzelm <none@none> |
added add_hook interface for post-transition hooks;
|
#
8e0194ec |
|
13-Aug-2008 |
wenzelm <none@none> |
simplified present_local_theory/proof;
|
#
6001bbed |
|
12-Aug-2008 |
wenzelm <none@none> |
added ignored, malformed transitions;
|
#
d61859a2 |
|
15-Jul-2008 |
wenzelm <none@none> |
support for command status;
|
#
7af516df |
|
14-Jul-2008 |
wenzelm <none@none> |
tuned;
|
#
e0fff075 |
|
15-Jul-2008 |
wenzelm <none@none> |
simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;
|
#
7f306330 |
|
14-Jul-2008 |
wenzelm <none@none> |
export EXCURSION_FAIL;
|
#
ceac4f47 |
|
14-Jul-2008 |
wenzelm <none@none> |
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning;
|
#
b9360c70 |
|
14-Jul-2008 |
wenzelm <none@none> |
replaced obsolete ProofHistory by ProofNode (backtracking only);
|
#
e68f43bf |
|
08-Jul-2008 |
wenzelm <none@none> |
export str_of;
|
#
7237a3c9 |
|
02-Jul-2008 |
wenzelm <none@none> |
init_theory: pass name explicitly; empty transition: empty name;
|
#
e26fe2a9 |
|
01-Jul-2008 |
wenzelm <none@none> |
added name_of; added get_id/put_id; tuned;
|
#
6addeb60 |
|
24-May-2008 |
wenzelm <none@none> |
present_excursion: setmp_thread_position during presentation;
|
#
7229106d |
|
10-Apr-2008 |
wenzelm <none@none> |
transaction/init: ensure stable theory (non-draft);
|
#
6a826d0c |
|
10-Apr-2008 |
wenzelm <none@none> |
eliminated unused name_of, source, source_of, print', print3, three_buffersN; tuned;
|
#
63b7b9dc |
|
10-Apr-2008 |
wenzelm <none@none> |
made purely value-oriented, moved global state to structure Isar (cf. isar.ML); export toplevel, error_msg (formerly print_exn), transition (formerly apply); moved type isar to structure OuterSyntax; moved crashes to structure Isar;
|
#
56f366ee |
|
29-Mar-2008 |
wenzelm <none@none> |
added generic_theory transaction;
|
#
2f219c71 |
|
15-Mar-2008 |
wenzelm <none@none> |
tuned;
|
#
f344976f |
|
11-Mar-2008 |
wenzelm <none@none> |
raw_loop: more graceful crash recovery;
|
#
3452e9bb |
|
11-Mar-2008 |
wenzelm <none@none> |
added exception CONTEXT, indicating context of another exception; exn_message: explicit context, *not* ML_Context.get_context; toplevel_error/apply: explicit exn_context; explicit Markup.location for exn_info (cf. at_command); fixed spelling; tuned;
|
#
57f8e0f3 |
|
16-Feb-2008 |
wenzelm <none@none> |
exn_message: added TimeLimit.TimeOut; replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
|
#
b02caf89 |
|
24-Jan-2008 |
wenzelm <none@none> |
removed unused properties; replaced ContextPosition by Position.thread_data;
|
#
51d21437 |
|
06-Jan-2008 |
wenzelm <none@none> |
removed obsolete prompt markup;
|
#
d57dd3d8 |
|
03-Jan-2008 |
wenzelm <none@none> |
replaced thread_properties by simplified version in position.ML;
|
#
1bc9eb4e |
|
03-Jan-2008 |
wenzelm <none@none> |
toplevel print_exn: proper setmp_thread_properties;
|
#
0c9699fe |
|
02-Jan-2008 |
wenzelm <none@none> |
maintain thread transition properties;
|
#
8dc91169 |
|
02-Jan-2008 |
wenzelm <none@none> |
type transition: added properties field;
|
#
3308afd8 |
|
08-Dec-2007 |
wenzelm <none@none> |
Isar loop: recover after toplevel crashes;
|
#
a3c556e4 |
|
05-Dec-2007 |
wenzelm <none@none> |
replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
|
#
e2d54ccb |
|
04-Dec-2007 |
wenzelm <none@none> |
Toplevel.loop: explicit argument for secure loop, no warning on quit;
|
#
6015d146 |
|
18-Nov-2007 |
wenzelm <none@none> |
init_empty: check before change (avoids non-linear update);
|
#
c76d2a10 |
|
05-Nov-2007 |
wenzelm <none@none> |
simplified LocalTheory.reinit; tuned;
|
#
9131a169 |
|
02-Nov-2007 |
haftmann <none@none> |
clarified theory target interface
|
#
acdbb20a |
|
28-Oct-2007 |
wenzelm <none@none> |
safe_exit: controlled_execution;
|
#
59e4b839 |
|
09-Oct-2007 |
wenzelm <none@none> |
TheoryTarget.init_cmd;
|
#
d06d005b |
|
08-Oct-2007 |
wenzelm <none@none> |
generic Syntax.pretty/string_of operations;
|
#
ddbb8c6a |
|
01-Oct-2007 |
wenzelm <none@none> |
print_state_context: local theory context, not proof context; context_position: cover Theory case as well (requires additional checkpoint);
|
#
738d25ff |
|
30-Sep-2007 |
wenzelm <none@none> |
local_theory transactions: more careful treatment of context position;
|
#
de2e0667 |
|
18-Sep-2007 |
wenzelm <none@none> |
simplified PrintMode interfaces;
|
#
0cb6645a |
|
28-Aug-2007 |
berghofe <none@none> |
Added local_theory_to_proof'
|
#
9a8712bb |
|
16-Aug-2007 |
wenzelm <none@none> |
global state transformation: non-critical, but also non-thread-safe;
|
#
72ae5946 |
|
29-Jul-2007 |
wenzelm <none@none> |
NAMED_CRITICAL;
|
#
18b78e20 |
|
29-Jul-2007 |
wenzelm <none@none> |
added TOPLEVEL_ERROR (simplified version from output.ML);
|
#
e0e1dd31 |
|
24-Jul-2007 |
wenzelm <none@none> |
*** empty log message ***
|
#
9473e8a6 |
|
24-Jul-2007 |
wenzelm <none@none> |
moved exception capture/release to structure Exn;
|
#
3c5d8a7e |
|
23-Jul-2007 |
wenzelm <none@none> |
marked some CRITICAL sections; eliminated transform_failure (to avoid critical section for main transactions); removed unused exceptions MetaSimplifier.SIMPROC_FAIL, Attrib.ATTRIB_FAIL, Method.METHOD_FAIL, Antiquote.ANTIQUOTE_FAIL;
|
#
ea82fd57 |
|
22-Jul-2007 |
wenzelm <none@none> |
init_empty: invoke operation *after* safe_exit;
|
#
e6e7ebc2 |
|
10-Jul-2007 |
wenzelm <none@none> |
Markup.enclose;
|
#
42072de0 |
|
10-Jul-2007 |
wenzelm <none@none> |
Markup.output; removed no_state markup -- produce empty state;
|
#
7f2e14c6 |
|
09-Jul-2007 |
wenzelm <none@none> |
prompt: plain string, not output;
|
#
ee33ce6e |
|
08-Jul-2007 |
wenzelm <none@none> |
simplified/more robust print_state; more robust prompt markup;
|
#
3b36d453 |
|
07-Jul-2007 |
wenzelm <none@none> |
toplevel prompt/print_state: proper markup, removed hooks; tuned;
|
#
cf707094 |
|
06-Jul-2007 |
wenzelm <none@none> |
tuned;
|
#
ec7ead07 |
|
19-Jun-2007 |
wenzelm <none@none> |
oops -- fixed profiling;
|
#
56d096f4 |
|
19-Jun-2007 |
wenzelm <none@none> |
profiling: observe no_timing;
|
#
a96a827a |
|
12-Jun-2007 |
wenzelm <none@none> |
transaction: context_position (non-destructive only);
|
#
edd80024 |
|
03-Apr-2007 |
wenzelm <none@none> |
removed unused info channel;
|
#
9924caa1 |
|
20-Jan-2007 |
wenzelm <none@none> |
Toplevel.debug: coincide with Output.debugging;
|
#
11a4159e |
|
19-Jan-2007 |
wenzelm <none@none> |
moved ML context stuff to from Context to ML_Context;
|
#
d4753879 |
|
19-Jan-2007 |
wenzelm <none@none> |
added generic_theory_of; adapted ML context operations;
|
#
c1a7637a |
|
10-Jan-2007 |
wenzelm <none@none> |
fixed exit: proper type check of state; tuned signature;
|
#
d2ebed23 |
|
05-Jan-2007 |
wenzelm <none@none> |
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
|
#
f2de4916 |
|
04-Jan-2007 |
haftmann <none@none> |
eliminated Option.app
|
#
2e340f82 |
|
03-Jan-2007 |
aspinall <none@none> |
Expose command failure recovery code for top level.
|
#
9946f056 |
|
30-Dec-2006 |
wenzelm <none@none> |
removed conditional combinator;
|
#
98861317 |
|
29-Dec-2006 |
wenzelm <none@none> |
refined notion of empty toplevel, admits undo of 'end'; added undo_exit, init_empty, init_state; removed unused toplevel, reset; tuned;
|
#
e9e15a40 |
|
14-Dec-2006 |
wenzelm <none@none> |
removed obsolete assert;
|
#
708cd9d0 |
|
23-Nov-2006 |
wenzelm <none@none> |
prefer Proof.context over Context.generic;
|
#
940ab246 |
|
11-Nov-2006 |
wenzelm <none@none> |
level: do not account for local theory blocks (relevant for document preparation);
|
#
2b461918 |
|
10-Nov-2006 |
wenzelm <none@none> |
simplified local theory wrappers;
|
#
5a3f769e |
|
09-Nov-2006 |
wenzelm <none@none> |
LocalTheory.restore;
|
#
d7883933 |
|
07-Nov-2006 |
wenzelm <none@none> |
removed obsolete print_state_hook;
|
#
1ebfc9e1 |
|
04-Nov-2006 |
wenzelm <none@none> |
removed checkpoint interface; moved back to copy/checkpoint instead of checkpoint/checkpoint (NB 1: checkpoint is idempotent, i.e. impure data is being shared, which is inappropriate; NB 2: copying a checkpoint always produces a related theory); present_proof: proper treatment of history; tuned;
|
#
d7f2f950 |
|
12-Oct-2006 |
wenzelm <none@none> |
renamed enter_forward_proof to enter_proof_body; renamed exit_local_theory to end_local_theory; added local_theory_to_proof; tuned;
|
#
18e4b0cf |
|
11-Oct-2006 |
wenzelm <none@none> |
exit_local_theory: pass interactive flag; begin_local_theory: generic init;
|
#
46f794ec |
|
10-Oct-2006 |
wenzelm <none@none> |
added type global_theory -- theory or local_theory; added begin/exit_local_theory; removed theory_context; renamed body_context_node to presentation_context; removed copy (checkpoint twice instead -- avoids unrelated theories);
|
#
21013d6d |
|
09-Oct-2006 |
wenzelm <none@none> |
loop: disallow exit in secure mode;
|
#
f8924482 |
|
06-Oct-2006 |
wenzelm <none@none> |
TheoryTarget;
|
#
fa18480a |
|
21-Sep-2006 |
wenzelm <none@none> |
member (op =);
|
#
54e6f8e2 |
|
08-Aug-2006 |
wenzelm <none@none> |
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
|
#
3a8ad7d0 |
|
14-Jul-2006 |
wenzelm <none@none> |
keep/transaction: unified execution model (with debugging etc.); tuned;
|
#
0adc567d |
|
04-Jul-2006 |
wenzelm <none@none> |
skip_proofs: do not skip proofs of schematic goals (warning);
|
#
55bcc817 |
|
11-Jun-2006 |
wenzelm <none@none> |
avoid unqualified exception;
|
#
fe76cdac |
|
02-May-2006 |
wenzelm <none@none> |
handle exception SYS_ERROR;
|
#
77797edd |
|
17-Feb-2006 |
wenzelm <none@none> |
checkpoint/copy_node: reset body context;
|
#
2e9940f2 |
|
15-Feb-2006 |
wenzelm <none@none> |
added cases_node; replaced body_context_of by body_context_node, removed no_body_context; copy: ProofContext.transfer; added present_local_theory, present_proof; removed internal command interface;
|
#
819e924d |
|
06-Feb-2006 |
wenzelm <none@none> |
added local_theory, with optional locale xname;
|
#
c4eb42aa |
|
27-Jan-2006 |
wenzelm <none@none> |
swapped theory_context;
|
#
30cbe57d |
|
19-Jan-2006 |
wenzelm <none@none> |
keep: disable Output.toplevel_errors; program: Output.ML_errors;
|
#
c2bc9a15 |
|
14-Jan-2006 |
wenzelm <none@none> |
sane ERROR vs. TOPLEVEL_ERROR handling; added program;
|
#
adaa86d0 |
|
12-Jan-2006 |
wenzelm <none@none> |
removed obsolete sign_of;
|
#
52532d9e |
|
10-Jan-2006 |
wenzelm <none@none> |
added context_of -- generic context;
|
#
7e83509b |
|
06-Jan-2006 |
wenzelm <none@none> |
transactions now always see quasi-functional intermediate checkpoint; removed obsolete theory_theory_to_proof; added
|
#
1933cd78 |
|
05-Jan-2006 |
wenzelm <none@none> |
hide type datatype node; added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy; no_body_context: no history; transaction: test save = true;
|
#
524a8c8e |
|
03-Jan-2006 |
wenzelm <none@none> |
added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);
|
#
5ed5abd7 |
|
03-Jan-2006 |
wenzelm <none@none> |
tuned;
|
#
26b3d597 |
|
18-Oct-2005 |
wenzelm <none@none> |
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
|
#
87fb3d7e |
|
20-Sep-2005 |
wenzelm <none@none> |
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
|
#
9a338822 |
|
20-Sep-2005 |
paulson <none@none> |
uniform handling of interrupts
|
#
a88a4f7d |
|
16-Sep-2005 |
wenzelm <none@none> |
theory_to_proof: check theory of initial proof state, which must not be changed;
|
#
38976b44 |
|
16-Sep-2005 |
paulson <none@none> |
catching exception Io
|
#
f325c5f4 |
|
13-Sep-2005 |
wenzelm <none@none> |
added three_buffersN, print3; tuned theory_to_proof: plain Proof.state instead of history; added EXCEPTION; removed DATA_FAIL, TRANSLATION_FAIL;
|
#
f09260f6 |
|
11-Sep-2005 |
wenzelm <none@none> |
added interact flag to control mode of excursions;
|
#
d722c18e |
|
11-Sep-2005 |
wenzelm <none@none> |
excursion: interactive if debug;
|
#
b611fef8 |
|
05-Sep-2005 |
wenzelm <none@none> |
added assert, command;
|
#
3c6237ac |
|
31-Aug-2005 |
wenzelm <none@none> |
added no_body_context;
|
#
a61f66e8 |
|
18-Aug-2005 |
wenzelm <none@none> |
proof_to_theory_context: interaction flag;
|
#
ac283f6c |
|
16-Aug-2005 |
wenzelm <none@none> |
state: body context; added theory_context, proof_to_theory_context; added is_proof, level; turned excursion_result into present_excursion;
|
#
1eef3638 |
|
13-Jul-2005 |
wenzelm <none@none> |
added print_state_hook; renamed proof'' to actual_proof; tuned;
|
#
f7a70d5d |
|
06-Jul-2005 |
wenzelm <none@none> |
debug: exception_trace; tuned;
|
#
146f1917 |
|
04-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
c7e53650 |
|
01-Jul-2005 |
wenzelm <none@none> |
added profile flag;
|
#
0be064e6 |
|
29-Jun-2005 |
wenzelm <none@none> |
added print': print depending on print_mode;
|
#
d0bd5836 |
|
20-Jun-2005 |
wenzelm <none@none> |
tuned;
|
#
64010a65 |
|
17-Jun-2005 |
wenzelm <none@none> |
Context.DATA_FAIL; accomodate identification of type Sign.sg and theory;
|
#
3644bf70 |
|
02-Jun-2005 |
wenzelm <none@none> |
tuned msgs; exn_message: added Fail; timing: info channel;
|
#
63b2df14 |
|
23-May-2005 |
wenzelm <none@none> |
node_trans: revert to original transaction code (pre 1.54);
|
#
9ac56383 |
|
17-May-2005 |
wenzelm <none@none> |
tuned;
|
#
eb1b8649 |
|
07-Apr-2005 |
wenzelm <none@none> |
improved exn_message;
|
#
381927aa |
|
26-Mar-2005 |
paulson <none@none> |
new display of theory stamps
|
#
cb2d89c8 |
|
10-Mar-2005 |
ballarin <none@none> |
Registrations of global locale interpretations: improved, better naming.
|
#
f527ae4a |
|
09-Mar-2005 |
ballarin <none@none> |
First version of global registration command.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
63efdaf5 |
|
23-Feb-2005 |
berghofe <none@none> |
Modified node_trans to avoid duplication of signature stamps when undoing.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
7c4791e1 |
|
09-Feb-2005 |
ballarin <none@none> |
Toplevel.debug for debugging in Isar.
|
#
16f87cc2 |
|
11-Jan-2005 |
berghofe <none@none> |
excursion_result now also passes previous state to presentation functions. This is useful for hiding proof scripts.
|
#
36f8bb69 |
|
11-Oct-2004 |
berghofe <none@none> |
Some changes to allow skipping of proof scripts.
|
#
c6d0a7dd |
|
21-Jun-2004 |
wenzelm <none@none> |
added >>> : transition list -> unit;
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
d556ba39 |
|
12-Jun-2004 |
wenzelm <none@none> |
added name_of, source_of, source;
|
#
598395eb |
|
29-May-2004 |
wenzelm <none@none> |
Output.timing;
|
#
2019f9e4 |
|
07-Jul-2003 |
nipkow <none@none> |
A patch by david aspinall
|
#
65210e04 |
|
08-Aug-2002 |
wenzelm <none@none> |
exception SIMPROC_FAIL: solid error reporting of simprocs;
|
#
bb94019c |
|
28-Feb-2002 |
wenzelm <none@none> |
use ignore_interrupt, raise_interrupt;
|
#
3fb1800e |
|
12-Feb-2002 |
wenzelm <none@none> |
ANTIQUOTE_FAIL;
|
#
bdf84388 |
|
08-Dec-2001 |
wenzelm <none@none> |
tuned print_state interfaces;
|
#
ca6df1f0 |
|
28-Nov-2001 |
wenzelm <none@none> |
added proof_to_theory';
|
#
050deed6 |
|
04-Nov-2001 |
wenzelm <none@none> |
simplified Proof.init_state:
|
#
1ae4842c |
|
31-Oct-2001 |
wenzelm <none@none> |
Proof.init_state thy None;
|
#
ef16ee8b |
|
22-Oct-2001 |
wenzelm <none@none> |
Display.current_goals_markers;
|
#
58e3b364 |
|
24-Oct-2000 |
wenzelm <none@none> |
tuned msg;
|
#
76783fab |
|
03-Aug-2000 |
wenzelm <none@none> |
added unknown_theory/proof/context;
|
#
96f0a075 |
|
27-Jul-2000 |
wenzelm <none@none> |
added enter_forward_proof;
|
#
5798f74d |
|
26-Jun-2000 |
wenzelm <none@none> |
excursion_result: transform_error;
|
#
e969e8e0 |
|
26-Jun-2000 |
wenzelm <none@none> |
tuned msg;
|
#
8b4b0107 |
|
25-Jun-2000 |
wenzelm <none@none> |
excursion_result;
|
#
6c6062ef |
|
31-May-2000 |
wenzelm <none@none> |
Toplevel.no_timing;
|
#
30d6b9a6 |
|
30-May-2000 |
wenzelm <none@none> |
global timing flag;
|
#
9cc94ff8 |
|
18-May-2000 |
wenzelm <none@none> |
print_state: flag for proof only;
|
#
c4ba1de8 |
|
05-May-2000 |
wenzelm <none@none> |
GPLed;
|
#
2045b738 |
|
17-Apr-2000 |
wenzelm <none@none> |
tuned msg;
|
#
e95487b9 |
|
23-Mar-2000 |
wenzelm <none@none> |
tuned output;
|
#
2f6f1359 |
|
15-Mar-2000 |
wenzelm <none@none> |
eliminated toplevel stack;
|
#
1adb358d |
|
05-Oct-1999 |
wenzelm <none@none> |
added is_toplevel;
|
#
65c2bf55 |
|
26-Sep-1999 |
wenzelm <none@none> |
added keep', theory';
|
#
a1e16dee |
|
25-Sep-1999 |
wenzelm <none@none> |
avoid interrupts of read loop;
|
#
3f512f8c |
|
07-Sep-1999 |
wenzelm <none@none> |
added context_of;
|
#
01c7ab69 |
|
20-Aug-1999 |
wenzelm <none@none> |
print_context;
|
#
ced59265 |
|
09-Aug-1999 |
wenzelm <none@none> |
tuned print_state; quiet flag;
|
#
06d64596 |
|
27-Jul-1999 |
wenzelm <none@none> |
init / init_theory: pass int flag;
|
#
84842cf8 |
|
22-Jul-1999 |
wenzelm <none@none> |
Toplevel.excursion_error;
|
#
b9997939 |
|
16-Jul-1999 |
wenzelm <none@none> |
removed BREAK, ROLLBACK;
|
#
e2bb3374 |
|
10-Jul-1999 |
wenzelm <none@none> |
tuned Interrupt msgs;
|
#
75608698 |
|
10-Jul-1999 |
wenzelm <none@none> |
fixed interrupts (eliminated races);
|
#
a8c30eab |
|
21-May-1999 |
wenzelm <none@none> |
tuned; added prompt_state_fn hook; added kill operation; provide toplevel node history, nests with proof history; toplevel prompt includes nest level; more robust recovery from stale signatures;
|
#
a37168e8 |
|
17-May-1999 |
wenzelm <none@none> |
cleaned comments; node_cases renamed to node_case; more robust rollback of transactions via backup;
|
#
49ef1288 |
|
05-Feb-1999 |
wenzelm <none@none> |
improved msg;
|
#
7db14615 |
|
03-Feb-1999 |
wenzelm <none@none> |
comment;
|
#
f4da5c50 |
|
01-Dec-1998 |
wenzelm <none@none> |
excursion: ERROR_MESSAGE; exn_message: ERROR;
|
#
15f5598c |
|
29-Nov-1998 |
wenzelm <none@none> |
added exception RESTART;
|
#
fa35cde0 |
|
20-Nov-1998 |
wenzelm <none@none> |
print_state hook, obeys Goals.current_goals_markers by default;
|
#
de076570 |
|
19-Nov-1998 |
wenzelm <none@none> |
break: exhibit state stack;
|
#
5b304d8b |
|
18-Nov-1998 |
wenzelm <none@none> |
exn_message FAIL;
|
#
e68f556a |
|
18-Nov-1998 |
wenzelm <none@none> |
export exn_message;
|
#
d8eaffc2 |
|
17-Nov-1998 |
wenzelm <none@none> |
BREAK: include state; report Attrib.ATTRIB_FAIL, Method.METHOD_FAIL;
|
#
78cddaf7 |
|
09-Nov-1998 |
wenzelm <none@none> |
The Isabelle/Isar toplevel.
|