| Mon, 12 Aug 2013 22:38:39 +0200 |
traytel |
temporary sorry's for temporarily nonterminating (due to 2b430bbb5a1a) proofs
|
changeset |
files
|
| Mon, 12 Aug 2013 21:30:37 +0200 |
blanchet |
qualify intermediate typedefs
|
changeset |
files
|
| Mon, 12 Aug 2013 21:30:36 +0200 |
blanchet |
avoid double qualification for case constants
|
changeset |
files
|
| Mon, 12 Aug 2013 21:30:35 +0200 |
blanchet |
qualify more generated names with optional type name component
|
changeset |
files
|
| Mon, 12 Aug 2013 20:04:03 +0200 |
traytel |
eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
|
changeset |
files
|
| Mon, 12 Aug 2013 15:36:55 +0200 |
traytel |
generalized library function
|
changeset |
files
|
| Mon, 12 Aug 2013 18:03:47 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Mon, 12 Aug 2013 18:02:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 12 Aug 2013 17:57:51 +0200 |
wenzelm |
clarified Query_Operation.register: avoid hard-wired parallel policy;
|
changeset |
files
|
| Mon, 12 Aug 2013 17:17:49 +0200 |
wenzelm |
moved generic module to its proper place;
|
changeset |
files
|
| Mon, 12 Aug 2013 17:11:27 +0200 |
wenzelm |
manage hyperlinks via PIDE editor interface;
|
changeset |
files
|
| Mon, 12 Aug 2013 15:09:13 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Mon, 12 Aug 2013 14:53:16 +0200 |
wenzelm |
prefer PIDE editor operations;
|
changeset |
files
|
| Mon, 12 Aug 2013 14:27:58 +0200 |
wenzelm |
central management of Document.Overlays, independent of Document_Model;
|
changeset |
files
|
| Mon, 12 Aug 2013 13:32:26 +0200 |
wenzelm |
tuned -- use Multi_Map;
|
changeset |
files
|
| Mon, 12 Aug 2013 13:30:54 +0200 |
wenzelm |
support for maps with multiple entries per key;
|
changeset |
files
|
| Mon, 12 Aug 2013 12:06:48 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 12 Aug 2013 11:56:12 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 12 Aug 2013 11:49:58 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 12 Aug 2013 11:39:29 +0200 |
wenzelm |
tuned signature -- more abstract PIDE editor operations;
|
changeset |
files
|
| Mon, 12 Aug 2013 15:48:57 +0200 |
blanchet |
tuned messages
|
changeset |
files
|
| Mon, 12 Aug 2013 15:25:17 +0200 |
blanchet |
clarified option name (since case/fold/rec are also destructors)
|
changeset |
files
|
| Mon, 12 Aug 2013 15:25:17 +0200 |
blanchet |
define case constant from other 'free constructor' axioms
|
changeset |
files
|
| Mon, 12 Aug 2013 15:25:16 +0200 |
blanchet |
introduced case tactics
|
changeset |
files
|
| Mon, 12 Aug 2013 15:25:16 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 12 Aug 2013 09:51:00 +0200 |
blanchet |
handle both TVars and TFrees -- necessary for 'wrap_free_constructors'
|
changeset |
files
|
| Mon, 12 Aug 2013 09:38:42 +0200 |
blanchet |
qualify map and rel names
|
changeset |
files
|
| Mon, 12 Aug 2013 09:08:42 +0200 |
blanchet |
reverted ill-advised naming scheme of 5a77edcdbe54
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
made (hopefully temporary) hack more robust
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
added warning
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
gracefully handle one more error condition
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
gracefully fail to define polymorphic (co)datatypes in local context
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
made code more robust
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
avoid DUP exception in local context (cf. 062aa11e98e1)
|
changeset |
files
|
| Sun, 11 Aug 2013 23:35:57 +0200 |
blanchet |
honor user tfree names
|
changeset |
files
|
| Sat, 10 Aug 2013 12:00:34 +0200 |
kleing |
prefer local facts over global ones
|
changeset |
files
|
| Sat, 10 Aug 2013 11:59:03 +0200 |
kleing |
use local context for name space
|
changeset |
files
|
| Sat, 10 Aug 2013 10:59:56 +0200 |
wenzelm |
explicit "strict" flag for print functions (flipped internal meaning);
|
changeset |
files
|
| Sat, 10 Aug 2013 10:15:30 +0200 |
kleing |
avoid unnecessary case distinction
|
changeset |
files
|
| Sat, 10 Aug 2013 09:06:42 +0200 |
kleing |
adjust tooltip for duplicates option
|
changeset |
files
|
| Fri, 09 Aug 2013 20:44:46 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 09 Aug 2013 20:31:51 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Fri, 09 Aug 2013 20:30:11 +0200 |
wenzelm |
Find is docked on startup;
|
changeset |
files
|
| Fri, 09 Aug 2013 20:26:54 +0200 |
wenzelm |
sorted lines;
|
changeset |
files
|
| Fri, 09 Aug 2013 20:23:53 +0200 |
wenzelm |
tuned GUI;
|
changeset |
files
|
| Fri, 09 Aug 2013 20:16:33 +0200 |
wenzelm |
retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);
|
changeset |
files
|
| Fri, 09 Aug 2013 20:01:50 +0200 |
wenzelm |
removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;
|
changeset |
files
|
| Fri, 09 Aug 2013 17:25:47 +0200 |
wenzelm |
enable search in pre-loaded theory;
|
changeset |
files
|
| Fri, 09 Aug 2013 16:17:48 +0200 |
wenzelm |
more GUI options;
|
changeset |
files
|
| Fri, 09 Aug 2013 15:49:50 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 09 Aug 2013 15:14:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 09 Aug 2013 15:00:29 +0200 |
wenzelm |
tuned GUI;
|
changeset |
files
|
| Fri, 09 Aug 2013 15:40:38 +0200 |
blanchet |
tuned name generation code (to make it easier to adapt later)
|
changeset |
files
|
| Fri, 09 Aug 2013 15:03:39 +0200 |
blanchet |
honor user type names if possible
|
changeset |
files
|
| Fri, 09 Aug 2013 13:57:21 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 09 Aug 2013 13:51:34 +0200 |
wenzelm |
more abstract consume_status operation;
|
changeset |
files
|
| Fri, 09 Aug 2013 13:37:51 +0200 |
wenzelm |
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
|
changeset |
files
|
| Fri, 09 Aug 2013 12:29:15 +0200 |
wenzelm |
more active "provers" field, which increases chances that its history is stored;
|
changeset |
files
|
| Fri, 09 Aug 2013 12:25:24 +0200 |
wenzelm |
removed command location is considered finished, and its overlay removed eventually;
|
changeset |
files
|
| Fri, 09 Aug 2013 11:18:36 +0200 |
wenzelm |
cancel_query via direct access to the exec_id of the running query process;
|
changeset |
files
|
| Fri, 09 Aug 2013 10:41:17 +0200 |
wenzelm |
retain original messages properties, e.g. for retrieval via Command.Results;
|
changeset |
files
|
| Fri, 09 Aug 2013 09:55:25 +0200 |
wenzelm |
clarified toplevel_error: absorb and print interrupts;
|
changeset |
files
|
| Fri, 09 Aug 2013 00:04:47 +0200 |
wenzelm |
more explicit error;
|
changeset |
files
|
| Fri, 09 Aug 2013 00:02:18 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 08 Aug 2013 23:52:35 +0200 |
wenzelm |
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
|
changeset |
files
|
| Thu, 08 Aug 2013 23:34:52 +0200 |
wenzelm |
more robust read_query;
|
changeset |
files
|
| Fri, 09 Aug 2013 12:27:29 +0200 |
kleing |
removed commented out declaration
|
changeset |
files
|
| Fri, 09 Aug 2013 11:26:29 +0200 |
traytel |
tuned
|
changeset |
files
|
| Thu, 08 Aug 2013 20:43:54 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 08 Aug 2013 17:49:07 +0200 |
wenzelm |
eliminate \<twosuperior> as well;
|
changeset |
files
|
| Thu, 08 Aug 2013 17:36:14 +0200 |
wenzelm |
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
|
changeset |
files
|
| Thu, 08 Aug 2013 17:24:31 +0200 |
wenzelm |
prefer plain subscript for identifiers;
|
changeset |
files
|
| Thu, 08 Aug 2013 17:04:02 +0200 |
wenzelm |
proper low-level comparison -- heed warning by Scala compiler;
|
changeset |
files
|
| Thu, 08 Aug 2013 18:20:15 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Thu, 08 Aug 2013 18:15:12 +0200 |
Andreas Lochbihler |
prefer Code.abort with explicit error message
|
changeset |
files
|
| Thu, 08 Aug 2013 18:13:12 +0200 |
kleing |
avoid re-inventing transitive closure
|
changeset |
files
|
| Thu, 08 Aug 2013 16:38:50 +0200 |
traytel |
merged
|
changeset |
files
|
| Thu, 08 Aug 2013 16:38:28 +0200 |
traytel |
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
|
changeset |
files
|
| Thu, 08 Aug 2013 15:30:25 +0200 |
traytel |
tuned
|
changeset |
files
|
| Thu, 08 Aug 2013 14:48:19 +0200 |
traytel |
tuned tactic;
|
changeset |
files
|
| Thu, 08 Aug 2013 16:10:05 +0200 |
Andreas Lochbihler |
abort execution of generated code with explicit exception message
|
changeset |
files
|
| Thu, 08 Aug 2013 14:55:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 08 Aug 2013 14:24:21 +0200 |
wenzelm |
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
|
changeset |
files
|
| Thu, 08 Aug 2013 14:13:04 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Thu, 08 Aug 2013 14:47:24 +0200 |
kleing |
snippet for instr type
|
changeset |
files
|
| Thu, 08 Aug 2013 12:01:02 +0200 |
traytel |
filter function on streams
|
changeset |
files
|
| Thu, 08 Aug 2013 12:00:45 +0200 |
traytel |
tuned
|
changeset |
files
|
| Wed, 07 Aug 2013 23:20:11 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 07 Aug 2013 21:16:20 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 07 Aug 2013 20:32:54 +0200 |
wenzelm |
maintain commands together with index -- avoid redundant reconstruction of full_index;
|
changeset |
files
|
| Wed, 07 Aug 2013 19:59:58 +0200 |
wenzelm |
more elementary list structures for markup tree traversal;
|
changeset |
files
|
| Wed, 07 Aug 2013 17:23:40 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Aug 2013 17:23:40 +0200 |
blanchet |
enrich exported ML function's signature
|
changeset |
files
|
| Wed, 07 Aug 2013 15:43:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Aug 2013 15:35:33 +0200 |
wenzelm |
more NEWS and CONTRIBUTORS;
|
changeset |
files
|
| Fri, 02 Aug 2013 15:42:47 +0900 |
Christian Sternagel |
some documentation for adhoc overloading;
|
changeset |
files
|
| Fri, 02 Aug 2013 15:42:01 +0900 |
Christian Sternagel |
added examples of adhoc overloading
|
changeset |
files
|
| Fri, 02 Aug 2013 15:41:19 +0900 |
Christian Sternagel |
use uniform spelling of "adhoc"
|
changeset |
files
|
| Fri, 02 Aug 2013 12:11:02 +0900 |
Christian Sternagel |
tuned formatting of error message
|
changeset |
files
|
| Wed, 07 Aug 2013 14:47:50 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 07 Aug 2013 14:13:59 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 07 Aug 2013 13:46:32 +0200 |
wenzelm |
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
|
changeset |
files
|
| Wed, 07 Aug 2013 11:50:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 07 Aug 2013 11:44:17 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 07 Aug 2013 11:17:06 +0200 |
wenzelm |
enabled key event to apply query;
|
changeset |
files
|
| Wed, 07 Aug 2013 10:58:26 +0200 |
wenzelm |
prefer single-line HistoryTextField;
|
changeset |
files
|
| Wed, 07 Aug 2013 15:40:59 +0200 |
kuncar |
contract equalities in transfer and transfer domain rules when they are registered
|
changeset |
files
|
| Wed, 07 Aug 2013 15:40:29 +0200 |
kuncar |
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
|
changeset |
files
|
| Tue, 06 Aug 2013 23:24:10 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 06 Aug 2013 23:20:25 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Tue, 06 Aug 2013 22:27:52 +0200 |
wenzelm |
more generic button;
|
changeset |
files
|
| Tue, 06 Aug 2013 22:02:20 +0200 |
wenzelm |
support for query operations that consist of parallel segments;
|
changeset |
files
|
| Tue, 06 Aug 2013 21:41:24 +0200 |
wenzelm |
more tooltips;
|
changeset |
files
|
| Tue, 06 Aug 2013 21:34:58 +0200 |
wenzelm |
tuned -- more explicit type Status.Value;
|
changeset |
files
|
| Tue, 06 Aug 2013 21:08:04 +0200 |
wenzelm |
more explicit status for query operation;
|
changeset |
files
|
| Tue, 06 Aug 2013 17:30:09 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 05 Aug 2013 23:57:29 +0200 |
wenzelm |
query process animation;
|
changeset |
files
|
| Mon, 05 Aug 2013 22:54:50 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 06 Aug 2013 15:50:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 06 Aug 2013 15:50:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 06 Aug 2013 15:50:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 06 Aug 2013 15:50:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 06 Aug 2013 15:50:23 +0200 |
blanchet |
export ML function (for primcorec)
|
changeset |
files
|
| Mon, 05 Aug 2013 21:23:06 +0200 |
wenzelm |
more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;
|
changeset |
files
|
| Mon, 05 Aug 2013 17:52:07 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 05 Aug 2013 17:14:02 +0200 |
wenzelm |
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
|
changeset |
files
|
| Mon, 05 Aug 2013 16:12:03 +0200 |
wenzelm |
remove overlay after result has arrived -- one-shot query operation;
|
changeset |
files
|
| Mon, 05 Aug 2013 15:48:13 +0200 |
wenzelm |
more message markup, provided by prover;
|
changeset |
files
|
| Mon, 05 Aug 2013 15:29:10 +0200 |
wenzelm |
tuned signature -- more uniform treatment of overlays as command mapping;
|
changeset |
files
|
| Mon, 05 Aug 2013 15:03:52 +0200 |
wenzelm |
commands with overlay remain visible, to avoid loosing printed output;
|
changeset |
files
|
| Mon, 05 Aug 2013 11:08:54 +0200 |
wenzelm |
initial update of nodes_required, for proper GUI state;
|
changeset |
files
|
| Mon, 05 Aug 2013 11:01:17 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 05 Aug 2013 10:55:46 +0200 |
wenzelm |
avoid repeated PIDE.flush_buffers when manipulating overlays;
|
changeset |
files
|
| Fri, 02 Aug 2013 23:03:59 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 02 Aug 2013 22:54:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 02 Aug 2013 22:46:54 +0200 |
wenzelm |
some actual find_theorems functionality;
|
changeset |
files
|
| Fri, 02 Aug 2013 22:17:53 +0200 |
wenzelm |
more general Output.result: allow to update arbitrary properties;
|
changeset |
files
|
| Fri, 02 Aug 2013 22:13:31 +0200 |
wenzelm |
prefer canonical order, to avoid potential fluctuation due to front-end edits;
|
changeset |
files
|
| Fri, 02 Aug 2013 20:47:02 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 02 Aug 2013 16:02:06 +0200 |
wenzelm |
minimal print function "find_theorems", which merely echos its arguments;
|
changeset |
files
|
| Fri, 02 Aug 2013 16:00:14 +0200 |
wenzelm |
support print functions with explicit arguments, as provided by overlays;
|
changeset |
files
|
| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
changeset |
files
|
| Fri, 02 Aug 2013 12:19:29 +0200 |
wenzelm |
some tracking of command location;
|
changeset |
files
|
| Fri, 02 Aug 2013 12:17:55 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 02 Aug 2013 11:51:21 +0200 |
wenzelm |
dockable window for "find" dialog (GUI only);
|
changeset |
files
|
| Fri, 02 Aug 2013 11:50:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 02 Aug 2013 22:36:31 +0200 |
traytel |
more robust tactics (don't use unfolding when RHS might contain schematics not contained on the LHS)
|
changeset |
files
|
| Fri, 02 Aug 2013 21:52:45 +0200 |
blanchet |
more (co)datatype docs
|
changeset |
files
|
| Fri, 02 Aug 2013 19:21:34 +0200 |
nipkow |
tuned exercises
|
changeset |
files
|
| Fri, 02 Aug 2013 19:10:10 +0200 |
blanchet |
more (co)datatype documentation
|
changeset |
files
|
| Fri, 02 Aug 2013 17:56:44 +0200 |
blanchet |
more (co)datatype documentation
|
changeset |
files
|
| Fri, 02 Aug 2013 12:08:55 +0200 |
traytel |
store relator induction in fp_result
|
changeset |
files
|
| Thu, 01 Aug 2013 23:25:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 01 Aug 2013 23:10:46 +0200 |
wenzelm |
optional static analysis for Poly/ML 5.5.x;
|
changeset |
files
|
| Thu, 01 Aug 2013 22:47:52 +0200 |
wenzelm |
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
|
changeset |
files
|
| Thu, 01 Aug 2013 22:20:07 +0200 |
wenzelm |
recode utf8 for ML, as done in feeder.pl;
|
changeset |
files
|
| Thu, 01 Aug 2013 22:19:32 +0200 |
wenzelm |
more explicit read-only non-TTY mode;
|
changeset |
files
|
| Thu, 01 Aug 2013 22:05:49 +0200 |
wenzelm |
clarified options;
|
changeset |
files
|
| Thu, 01 Aug 2013 21:56:43 +0200 |
wenzelm |
specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
|
changeset |
files
|
| Thu, 01 Aug 2013 21:09:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Aug 2013 20:45:49 +0200 |
wenzelm |
test recent polyml-svn, which is becoming polyml-5.5.1;
|
changeset |
files
|
| Thu, 01 Aug 2013 22:37:04 +0200 |
blanchet |
minor doc fixes
|
changeset |
files
|
| Thu, 01 Aug 2013 22:28:49 +0200 |
blanchet |
more (co)datatype docs
|
changeset |
files
|
| Thu, 01 Aug 2013 18:13:31 +0200 |
blanchet |
more (co)datatype documentation
|
changeset |
files
|
| Thu, 01 Aug 2013 16:53:03 +0200 |
kleing |
merged
|
changeset |
files
|
| Thu, 01 Aug 2013 16:52:28 +0200 |
kleing |
removed duplicate lemma
|
changeset |
files
|
| Thu, 01 Aug 2013 15:50:16 +0200 |
blanchet |
more (co)datatype documentation
|
changeset |
files
|
| Thu, 01 Aug 2013 14:22:21 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 01 Aug 2013 14:22:10 +0200 |
blanchet |
more (co)datatype docs
|
changeset |
files
|
| Thu, 01 Aug 2013 00:18:45 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Wed, 31 Jul 2013 23:41:32 +0200 |
wenzelm |
recovered "\<phi>\<^isub>i" from 0b02aaf7c7c5;
|
changeset |
files
|
| Wed, 31 Jul 2013 22:15:17 +0200 |
wenzelm |
proper border (again) -- avoid NPE on Windows;
|
changeset |
files
|
| Wed, 31 Jul 2013 21:53:33 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Wed, 31 Jul 2013 21:49:29 +0200 |
wenzelm |
added home-made tooltips;
|
changeset |
files
|
| Wed, 31 Jul 2013 21:13:05 +0200 |
wenzelm |
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
|
changeset |
files
|
| Wed, 31 Jul 2013 19:59:14 +0200 |
wenzelm |
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
|
changeset |
files
|
| Wed, 31 Jul 2013 18:08:12 +0200 |
nipkow |
added Getting Started text
|
changeset |
files
|
| Wed, 31 Jul 2013 16:50:41 +0200 |
traytel |
more robust tactic
|
changeset |
files
|
| Wed, 31 Jul 2013 15:24:07 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 31 Jul 2013 13:00:42 +0200 |
wenzelm |
clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
|
changeset |
files
|
| Wed, 31 Jul 2013 12:46:53 +0200 |
wenzelm |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
changeset |
files
|
| Wed, 31 Jul 2013 12:31:10 +0200 |
wenzelm |
paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;
|
changeset |
files
|
| Wed, 31 Jul 2013 12:14:13 +0200 |
wenzelm |
allow explicit indication of required node: full eval, no prints;
|
changeset |
files
|
| Wed, 31 Jul 2013 10:54:37 +0200 |
wenzelm |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
changeset |
files
|
| Wed, 31 Jul 2013 13:40:57 +0200 |
blanchet |
more work on (co)datatype docs
|
changeset |
files
|
| Wed, 31 Jul 2013 11:28:59 +0200 |
blanchet |
more (co)datatype documentation
|
changeset |
files
|
| Tue, 30 Jul 2013 23:17:26 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 30 Jul 2013 23:16:17 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 30 Jul 2013 22:43:11 +0200 |
wenzelm |
more uniform border;
|
changeset |
files
|
| Tue, 30 Jul 2013 22:31:34 +0200 |
wenzelm |
proper PIDE markup for codegen arguments;
|
changeset |
files
|
| Tue, 30 Jul 2013 21:22:37 +0200 |
wenzelm |
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
|
changeset |
files
|
| Tue, 30 Jul 2013 19:53:06 +0200 |
wenzelm |
tuned -- more uniform ML vs. Scala;
|
changeset |
files
|
| Tue, 30 Jul 2013 18:19:16 +0200 |
wenzelm |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
changeset |
files
|
| Tue, 30 Jul 2013 16:22:07 +0200 |
wenzelm |
more timing;
|
changeset |
files
|
| Tue, 30 Jul 2013 16:01:19 +0200 |
wenzelm |
more timing;
|
changeset |
files
|
| Tue, 30 Jul 2013 19:59:17 +0200 |
blanchet |
removed spurious headings
|
changeset |
files
|
| Tue, 30 Jul 2013 19:49:42 +0200 |
blanchet |
more (co)datatype documentation
|
changeset |
files
|
| Tue, 30 Jul 2013 16:22:39 +0200 |
blanchet |
avoid DUP error in local context
|
changeset |
files
|
| Tue, 30 Jul 2013 16:22:39 +0200 |
blanchet |
sketched documentation for new (co)datatype package
|
changeset |
files
|
| Tue, 30 Jul 2013 16:22:39 +0200 |
blanchet |
tuned docs (the function package isn't so new anymore)
|
changeset |
files
|
| Tue, 30 Jul 2013 15:45:01 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 30 Jul 2013 15:20:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
changeset |
files
|
| Tue, 30 Jul 2013 12:07:14 +0200 |
wenzelm |
pro-forma Execution.reset, despite lack of final join/commit;
|
changeset |
files
|
| Tue, 30 Jul 2013 11:54:57 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 30 Jul 2013 11:44:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 30 Jul 2013 11:38:43 +0200 |
wenzelm |
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
|
changeset |
files
|
| Mon, 29 Jul 2013 22:17:32 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 29 Jul 2013 22:17:19 +0200 |
nipkow |
tuned intro
|
changeset |
files
|
| Sun, 28 Jul 2013 05:32:02 +0200 |
haftmann |
silenced subsumption warnings for default code equations entirely
|
changeset |
files
|
| Mon, 29 Jul 2013 20:51:05 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 29 Jul 2013 20:46:21 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Mon, 29 Jul 2013 20:38:40 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 29 Jul 2013 20:34:53 +0200 |
wenzelm |
updated key bindings to execution range;
|
changeset |
files
|
| Mon, 29 Jul 2013 19:55:38 +0200 |
wenzelm |
traverse node on change of "required" state;
|
changeset |
files
|
| Mon, 29 Jul 2013 18:59:58 +0200 |
wenzelm |
keep memo_exec execution running, which is important to cancel goal forks eventually;
|
changeset |
files
|
| Mon, 29 Jul 2013 16:52:04 +0200 |
wenzelm |
maintain explicit execution frontier: avoid conflict with former task via static dependency;
|
changeset |
files
|
| Mon, 29 Jul 2013 16:01:05 +0200 |
wenzelm |
afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
|
changeset |
files
|
| Mon, 29 Jul 2013 15:59:47 +0200 |
wenzelm |
clarified conditions for node traversal;
|
changeset |
files
|
| Mon, 29 Jul 2013 15:20:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Jul 2013 15:09:20 +0200 |
wenzelm |
pro-forma Goal.reset_futures, despite lack of final join/commit;
|
changeset |
files
|
| Mon, 29 Jul 2013 15:01:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Jul 2013 14:49:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Jul 2013 14:43:21 +0200 |
wenzelm |
back to model.update_perspective with delay (cf. a20631db9c8a);
|
changeset |
files
|
| Mon, 29 Jul 2013 14:37:59 +0200 |
wenzelm |
show displaced messages (e.g. from protocol thread) as raw output;
|
changeset |
files
|
| Mon, 29 Jul 2013 14:18:57 +0200 |
wenzelm |
actually purge removed goal futures -- avoid memory leak;
|
changeset |
files
|
| Mon, 29 Jul 2013 13:43:43 +0200 |
wenzelm |
tuned -- less redundant data structure;
|
changeset |
files
|
| Mon, 29 Jul 2013 13:43:12 +0200 |
wenzelm |
always init GUI state;
|
changeset |
files
|
| Mon, 29 Jul 2013 13:28:27 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 29 Jul 2013 13:24:15 +0200 |
wenzelm |
discontinued notion of "stable" result -- running execution is never canceled;
|
changeset |
files
|
| Mon, 29 Jul 2013 13:00:36 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Mon, 29 Jul 2013 12:50:16 +0200 |
wenzelm |
support declarative editor_execution_range, instead of old-style check/cancel buttons;
|
changeset |
files
|
| Mon, 29 Jul 2013 18:06:39 +0200 |
blanchet |
avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
|
changeset |
files
|
| Mon, 29 Jul 2013 17:27:56 +0200 |
blanchet |
updated Sledgehammer prover versions
|
changeset |
files
|
| Mon, 29 Jul 2013 16:13:35 +0200 |
blanchet |
parse nonnumeric identifiers in E proofs correctly
|
changeset |
files
|
| Mon, 29 Jul 2013 15:42:04 +0200 |
blanchet |
simplified Vampire hack -- no need to run it for other ATPs
|
changeset |
files
|
| Mon, 29 Jul 2013 15:30:31 +0200 |
blanchet |
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
|
changeset |
files
|
| Sun, 28 Jul 2013 20:51:15 +0200 |
wenzelm |
prefer examples that work out of the box;
|
changeset |
files
|
| Sun, 28 Jul 2013 20:50:44 +0200 |
wenzelm |
breakable @{file};
|
changeset |
files
|
| Sun, 28 Jul 2013 20:10:59 +0200 |
wenzelm |
prefer existing swipl;
|
changeset |
files
|