Mon, 31 Mar 2014 12:16:37 +0200 hoelzl add connected_local_const
Mon, 31 Mar 2014 12:16:35 +0200 hoelzl add rules about infinity of intervals
Sun, 30 Mar 2014 21:24:59 +0200 wenzelm tuned proofs;
Sun, 30 Mar 2014 21:03:40 +0200 wenzelm immediate completion even with delay, which is the default according to 638b29331549;
Sun, 30 Mar 2014 20:23:26 +0200 wenzelm special treatment for various kinds of selections: imitate normal flow of editing;
Sat, 29 Mar 2014 21:26:11 +0100 wenzelm merged
Sat, 29 Mar 2014 20:41:50 +0100 wenzelm do not absorb vacuous copy operation, e.g. relevant when tooltip has focus but no selection, while the main text area has a selection but no focus;
Sat, 29 Mar 2014 20:22:38 +0100 wenzelm check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
Sat, 29 Mar 2014 12:42:24 +0100 wenzelm dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
Fri, 28 Mar 2014 18:21:07 -0700 huffman tuned proofs
Fri, 28 Mar 2014 18:21:20 -0700 huffman minimized imports
Sat, 29 Mar 2014 12:05:24 +0100 wenzelm merged
Sat, 29 Mar 2014 11:29:42 +0100 wenzelm tuned rendering -- change mouse pointer for active areas;
Sat, 29 Mar 2014 10:49:32 +0100 wenzelm propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
Sat, 29 Mar 2014 10:17:09 +0100 wenzelm tuned signature;
Sat, 29 Mar 2014 09:34:51 +0100 wenzelm tuned signature;
Sat, 29 Mar 2014 09:24:39 +0100 wenzelm tuned -- see Text.Range.overlaps(Range);
Sat, 29 Mar 2014 11:41:39 +0100 nipkow tuned
Fri, 28 Mar 2014 21:17:47 +0100 wenzelm tuned;
Thu, 27 Mar 2014 21:38:45 +0100 wenzelm merged
Thu, 27 Mar 2014 21:18:14 +0100 wenzelm tuned -- avoid code duplication;
Thu, 27 Mar 2014 21:16:08 +0100 wenzelm tuned;
Thu, 27 Mar 2014 20:28:19 +0100 wenzelm more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
Thu, 27 Mar 2014 19:47:30 +0100 wenzelm back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
Thu, 27 Mar 2014 18:42:53 +0100 wenzelm tuned;
Thu, 27 Mar 2014 17:56:13 +0100 wenzelm redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Thu, 27 Mar 2014 13:00:40 +0100 wenzelm more frugal merge of markup trees: non-overlapping tree counts as empty;
Thu, 27 Mar 2014 12:11:32 +0100 wenzelm more frugal merge of markup trees: filter wrt. subsequent query;
Thu, 27 Mar 2014 11:19:31 +0100 wenzelm tuned signature;
Thu, 27 Mar 2014 10:43:43 +0100 wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
Wed, 26 Mar 2014 21:01:09 +0100 wenzelm tuned signature -- expose less intermediate information;
Wed, 26 Mar 2014 20:32:15 +0100 wenzelm support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
Wed, 26 Mar 2014 20:08:07 +0100 wenzelm less markup by default -- this is stored persistently in Isabelle/Scala;
Wed, 26 Mar 2014 19:42:16 +0100 wenzelm clarified valid_id: always standardize towards static command.id;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
Wed, 26 Mar 2014 14:15:34 +0100 wenzelm unused;
Wed, 26 Mar 2014 12:32:51 +0100 wenzelm more uniform Execution.fork vs. Execution.print;
Wed, 26 Mar 2014 12:15:42 +0100 wenzelm added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
Wed, 26 Mar 2014 11:05:25 -0700 huffman tuned proofs
Wed, 26 Mar 2014 14:00:37 +0000 paulson Some useful lemmas
Wed, 26 Mar 2014 09:19:04 +0100 wenzelm tuned comments;
Wed, 26 Mar 2014 09:13:38 +0100 wenzelm tuned load order;
Wed, 26 Mar 2014 09:07:31 +0100 wenzelm superseded by (provide_)parse_files;
Wed, 26 Mar 2014 08:59:53 +0100 wenzelm tuned;
Tue, 25 Mar 2014 20:12:53 +0100 wenzelm merged
Tue, 25 Mar 2014 19:27:55 +0100 wenzelm more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);
Tue, 25 Mar 2014 19:13:33 +0100 wenzelm eliminated dead code;
Tue, 25 Mar 2014 19:03:02 +0100 wenzelm proper configuration option "ML_print_depth";
Tue, 25 Mar 2014 17:59:34 +0100 wenzelm removed junk;
Tue, 25 Mar 2014 16:54:38 +0100 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);
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Tue, 25 Mar 2014 15:15:33 +0100 wenzelm separate "sml" mode, suppress old "ml" mode altogether;
Tue, 25 Mar 2014 14:52:35 +0100 wenzelm some SML examples;
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Tue, 25 Mar 2014 10:37:10 +0100 wenzelm updated to scala-2.10.4;
Tue, 25 Mar 2014 14:20:58 +0100 hoelzl cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
Tue, 25 Mar 2014 13:14:33 +0100 traytel prove theorems with fixed variables (export afterwards)
Mon, 24 Mar 2014 14:51:10 -0700 huffman generalized theorems about derivatives of limits of sequences of funtions
Mon, 24 Mar 2014 19:06:20 +0100 wenzelm removed unused 'ax_specification', to give 'specification' a chance to become localized;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip