merged

removed superfluous output_typewriter from cs 65064e8f269

more idiomatic handling of latex typewriter type setting

more canonical type setting of type writer code examples

resynchronize isabelle.sty

reverted cs 5aced2f43837 -- no need for hardwired latex command here

reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter

reverted cs 07549694e2f1

shifted abstraction over imperative print mode

removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned

moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule

exporting the generic version instead of the context version in quickcheck

splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests

adding a mutual recursive example for named alternative rules for the predicate compiler

handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types

improving naming of assumptions in code_pred

adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim

handling equivalences smarter in the predicate compiler

removing duplicate rewrite rule from simpset in predicate compiler

rewriting function mk_Eval_of in predicate compiler

merged

improved and tuned external codegen tool

make SML/NJ happy

CONTRIBUTORS and NEWS

corrections and tuning

merged

merged

merged

tuned

persistent session-panel.selection;

slightly more robust EditBus plumbing wrt. Document_View/Document_Model;

permissive exit;

added Session_Dockable.session_phase label;

separate Plugin.init_model; slightly more robust initialization of Document_View/Document_Model, depending of Session.phase;

simplified Session.Phase; slightly more robust session startup; misc tuning;

tuned messages -- cf. Admin/MacOS/App1;

tuned dialog;

explicit Session.Phase indication with associated event bus; asynchronous Session.start(); synchronous Session.stop(); added Plugin.session_manager on top of basic Session; eliminated separate isabelle.activate action; misc tuning;

tuned signature;

Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;

tuned;

manage persistent syslog via Session, not Isabelle_Process; tuned;

tuned prover message categorization;

tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;

tuned message;

Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;

Snapshot.convert/revert: explicit error report to isolate sporadic crash;

make compiler doubly sure;

isabelle-process: less verbose no-commit mode;

tuned message;

tuned panel names and actions;

renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;

reactivated polyml-5.4.0 -- SVN 1214 fixes a problem with arbitrary precision arithmetic that was triggered by method "approximation" in HOL/Decision_Procs/Approximation_Ex.thy;

merged

more lists lemmas

merged

merged

tuned text

sections on @{code} and code_reflect

formal syntax diagram for code_reflect