Sun, 08 Aug 2010 20:03:31 +0200 wenzelm proper context for Syntax.parse_token;
Sun, 08 Aug 2010 19:54:54 +0200 wenzelm prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Sun, 08 Aug 2010 14:22:54 +0200 wenzelm fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
Sun, 08 Aug 2010 14:00:59 +0200 wenzelm YXML.parse: refrain from interning, let XML.Cache do it (partially);
Sun, 08 Aug 2010 13:59:57 +0200 wenzelm cache_string: store trimmed string value;
Sat, 07 Aug 2010 23:02:19 +0200 wenzelm simple_dialog: allow scala.swing.Component as well;
Sat, 07 Aug 2010 22:43:57 +0200 wenzelm simplified some Markup;
Sat, 07 Aug 2010 22:09:52 +0200 wenzelm simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
Sat, 07 Aug 2010 21:22:39 +0200 wenzelm more robust treatment of Markup.token;
Sat, 07 Aug 2010 21:03:06 +0200 wenzelm simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
Sat, 07 Aug 2010 19:52:14 +0200 wenzelm concentrate structural document notions in document.scala;
Sat, 07 Aug 2010 17:24:46 +0200 wenzelm maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
Sat, 07 Aug 2010 16:49:03 +0200 wenzelm tuned;
Sat, 07 Aug 2010 16:44:52 +0200 wenzelm more explicit model of pending text edits;
Sat, 07 Aug 2010 16:15:52 +0200 wenzelm more explicit treatment of Swing thread context;
Sat, 07 Aug 2010 14:45:26 +0200 wenzelm replaced individual Document_Model history by all-inclusive one in Session;
Sat, 07 Aug 2010 13:19:48 +0200 wenzelm misc tuning and clarification;
Fri, 06 Aug 2010 21:52:49 +0200 wenzelm avoid null in Scala;
Fri, 06 Aug 2010 14:37:04 +0200 wenzelm updated keywords;
Fri, 06 Aug 2010 14:35:04 +0200 wenzelm removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
Fri, 06 Aug 2010 12:38:02 +0200 wenzelm merged
Fri, 06 Aug 2010 11:37:33 +0200 blanchet merged
Fri, 06 Aug 2010 11:35:10 +0200 blanchet quotient types registered as codatatypes are no longer quotient types
Fri, 06 Aug 2010 11:33:58 +0200 blanchet added a friendly warning
Fri, 06 Aug 2010 11:05:57 +0200 blanchet extend the scope of limitation about nonconservative extensions
Fri, 06 Aug 2010 10:50:52 +0200 blanchet improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
Thu, 05 Aug 2010 22:29:43 +0200 ballarin Remove duplicate locale activation code; performance improvement.
Thu, 05 Aug 2010 21:56:22 +0200 blanchet added record field
Thu, 05 Aug 2010 20:17:50 +0200 blanchet added "whack"
Thu, 05 Aug 2010 18:33:07 +0200 blanchet handle "Rep_unit" & Co. gracefully
Thu, 05 Aug 2010 18:00:50 +0200 blanchet added support for "Abs_" and "Rep_" functions on quotient types
Thu, 05 Aug 2010 15:44:54 +0200 blanchet fiddle with specialization etc.
Thu, 05 Aug 2010 14:45:27 +0200 blanchet handle inductive predicates correctly after change in "def" semantics
Thu, 05 Aug 2010 14:32:24 +0200 blanchet don't specialize built-ins or constructors
Thu, 05 Aug 2010 14:20:34 +0200 blanchet more docs
Thu, 05 Aug 2010 14:10:18 +0200 blanchet prevent the expansion of too large definitions -- use equations for these instead
Thu, 05 Aug 2010 12:58:57 +0200 blanchet make nitpick accept "==" for "nitpick_(p)simp"s
Thu, 05 Aug 2010 12:40:12 +0200 blanchet fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
Thu, 05 Aug 2010 11:54:53 +0200 blanchet deal correctly with Pure.conjunction in mono check
Thu, 05 Aug 2010 09:49:46 +0200 blanchet rename internal functions
Thu, 05 Aug 2010 01:12:12 +0200 blanchet remove buggy and needless condition
Thu, 05 Aug 2010 00:21:11 +0200 blanchet renamed internal function
Wed, 04 Aug 2010 23:27:27 +0200 blanchet Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
Wed, 04 Aug 2010 22:47:52 +0200 blanchet avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
Wed, 04 Aug 2010 21:56:17 +0200 blanchet improve datatype symmetry breaking;
Wed, 04 Aug 2010 10:52:29 +0200 blanchet merged
Wed, 04 Aug 2010 10:51:04 +0200 blanchet make SML/NJ happy
Wed, 04 Aug 2010 10:39:35 +0200 blanchet get rid of all "optimizations" regarding "unit" and other cardinality-1 types
Tue, 03 Aug 2010 21:37:12 +0200 blanchet tuning
Tue, 03 Aug 2010 21:20:31 +0200 blanchet better "Pretty" handling
Tue, 03 Aug 2010 18:27:21 +0200 blanchet change formula for enumerating scopes
Tue, 03 Aug 2010 18:14:44 +0200 blanchet example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
Tue, 03 Aug 2010 17:43:15 +0200 blanchet speed up Nitpick examples a little bit
Tue, 03 Aug 2010 17:29:54 +0200 blanchet minor changes
Tue, 03 Aug 2010 17:29:27 +0200 blanchet updated example timings
Tue, 03 Aug 2010 15:15:17 +0200 blanchet more helpful message
Tue, 03 Aug 2010 14:54:30 +0200 blanchet also mention gfp
Tue, 03 Aug 2010 14:49:42 +0200 blanchet bump up the max cardinalities, to use up more of the time given to us by the user
Tue, 03 Aug 2010 14:49:02 +0200 blanchet make tracing monotonicity easier
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip