2010-07-21 wenzelm 2010-07-21 replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
2010-07-21 wenzelm 2010-07-21 thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
2010-07-21 wenzelm 2010-07-21 explicit dependency on theory HOL;
2010-07-21 wenzelm 2010-07-21 ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);
2010-07-21 wenzelm 2010-07-21 added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
2010-07-21 wenzelm 2010-07-21 thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;
2010-07-21 wenzelm 2010-07-21 clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 wenzelm 2010-07-20 qualified Thy_Info.get_theory;
2010-07-20 wenzelm 2010-07-20 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
2010-07-20 wenzelm 2010-07-20 further Mac OS X deviations;
2010-07-20 wenzelm 2010-07-20 warning in proper transaction context;
2010-07-20 wenzelm 2010-07-20 SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here;
2010-07-20 wenzelm 2010-07-20 avoid duplicate printing of 'theory' state (cf. 173974e07dea);
2010-07-20 wenzelm 2010-07-20 toplevel pp for Proof.state and Toplevel.state;
2010-07-20 wenzelm 2010-07-20 execute document version at high priority;
2010-07-20 wenzelm 2010-07-20 Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
2010-07-20 wenzelm 2010-07-20 edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;
2010-07-20 wenzelm 2010-07-20 back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c); cancel passive tasks more actively via Exn.Interrupt, by treating them like ragular jobs here; attempts to re-assign canceled futures/promises raise Exn.Interrupt; tuned;
2010-07-20 wenzelm 2010-07-20 export Graph.get_entry for convenience;
2010-07-20 wenzelm 2010-07-20 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;
2010-07-20 wenzelm 2010-07-20 tuned;
2010-07-20 wenzelm 2010-07-20 observe follow_caret (again);
2010-07-19 wenzelm 2010-07-19 Session: predefined real time parameters; Document_View: delayed caret handling, for improved reactivity; selected_command: proper_command_at ignores ignored commands;
2010-07-19 haftmann 2010-07-19 bind and then latex symbols
2010-07-18 wenzelm 2010-07-18 minor update of dependencies;
2010-07-16 haftmann 2010-07-16 corrected range chec
2010-07-16 haftmann 2010-07-16 first roughly working version of Imperative HOL for Scala
2010-07-16 haftmann 2010-07-16 tuned
2010-07-16 haftmann 2010-07-16 merged
2010-07-16 haftmann 2010-07-16 a first sketch for Imperative HOL witht Scala
2010-07-16 haftmann 2010-07-16 don't fail gracefully
2010-07-16 haftmann 2010-07-16 restored long-broken syntax sanity checks
2010-07-16 haftmann 2010-07-16 tuned interpunctation
2010-07-16 haftmann 2010-07-16 fragments of Scala
2010-07-15 haftmann 2010-07-15 merged
2010-07-15 haftmann 2010-07-15 adjusted; fixed typo
2010-07-15 haftmann 2010-07-15 dropped spurious export_code
2010-07-14 kleing 2010-07-14 use different log server (macbroy23 down)
2010-07-14 haftmann 2010-07-14 more consistent spacing in generated monadic code
2010-07-14 haftmann 2010-07-14 braced needed in layout-insensitive syntax
2010-07-14 haftmann 2010-07-14 repaired some implementations of imperative operations
2010-07-14 haftmann 2010-07-14 repaired reference implementation for OCaml
2010-07-14 haftmann 2010-07-14 part of pervasive test
2010-07-14 haftmann 2010-07-14 avoid ambiguities; tuned
2010-07-14 haftmann 2010-07-14 repaired of_list implementation for SML, OCaml
2010-07-14 haftmann 2010-07-14 avoid export_code ... file -
2010-07-14 haftmann 2010-07-14 explicit optional checking
2010-07-14 haftmann 2010-07-14 added Isar syntax for code checking
2010-07-14 haftmann 2010-07-14 corrected import
2010-07-14 haftmann 2010-07-14 use generic description slot for formal code checking
2010-07-14 haftmann 2010-07-14 formal slot for code checker
2010-07-14 haftmann 2010-07-14 export_code without file prints to standard output
2010-07-14 haftmann 2010-07-14 check without explicit path
2010-07-14 haftmann 2010-07-14 load cache_io before code generator; moved adhoc-overloading to generic tools
2010-07-14 haftmann 2010-07-14 tuned infix syntax
2010-07-14 haftmann 2010-07-14 dropped M suffix; added predicate monad bind
2010-07-14 haftmann 2010-07-14 self-built symbol for part of bind operator
2010-07-14 haftmann 2010-07-14 redirect stderr to stdout
2010-07-13 paulson 2010-07-13 merged
2010-07-13 paulson 2010-07-13 merged