src/Pure/System/isabelle_process.ML
Mon, 29 Jul 2013 15:09:20 +0200 wenzelm pro-forma Goal.reset_futures, despite lack of final join/commit;
Fri, 19 Jul 2013 23:29:43 +0200 wenzelm proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);
Fri, 19 Jul 2013 17:58:57 +0200 wenzelm just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
Mon, 15 Jul 2013 10:25:35 +0200 wenzelm more careful termination of removed execs, leaving running execs undisturbed;
Wed, 10 Jul 2013 23:25:28 +0200 wenzelm more abstract message channel;
Wed, 10 Jul 2013 22:56:48 +0200 wenzelm explicit shutdown of message output thread;
Wed, 10 Jul 2013 22:04:57 +0200 wenzelm tuned signature;
Wed, 10 Jul 2013 21:21:37 +0200 wenzelm fall back on synchronous message output for single-threaded SML/NJ;
Wed, 10 Jul 2013 20:44:39 +0200 wenzelm retain main thread for protocol loop -- no access to raw ML toplevel;
Mon, 08 Jul 2013 12:47:39 +0200 wenzelm tuned;
Mon, 08 Jul 2013 12:07:06 +0200 wenzelm more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
Wed, 22 May 2013 14:10:45 +0200 wenzelm explicit management of Session.Protocol_Handlers, with protocol state and functions;
Tue, 21 May 2013 18:03:36 +0200 wenzelm proper options;
Tue, 21 May 2013 17:55:28 +0200 wenzelm proper options;
Fri, 17 May 2013 20:30:04 +0200 wenzelm retain quick_and_dirty as-is -- no censorship;
Sun, 12 May 2013 15:05:15 +0200 wenzelm full default options for Isabelle_Process and Build;
Wed, 27 Mar 2013 16:46:52 +0100 wenzelm separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
Wed, 27 Mar 2013 16:38:25 +0100 wenzelm more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Wed, 13 Mar 2013 21:25:08 +0100 wenzelm clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
Mon, 04 Mar 2013 15:03:46 +0100 wenzelm refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
Tue, 22 Jan 2013 11:28:54 +0100 wenzelm more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
Wed, 16 Jan 2013 16:26:36 +0100 wenzelm more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
Fri, 04 Jan 2013 12:33:25 +0100 wenzelm prefer old graph browser in Isabelle/jEdit, which still produces better layout;
Thu, 03 Jan 2013 14:03:44 +0100 wenzelm always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
Thu, 13 Dec 2012 19:53:55 +0100 wenzelm smarter handling of tracing messages: prover process pauses and enters user dialog;
Thu, 13 Dec 2012 18:00:24 +0100 wenzelm enable Isabelle/ML to produce uninterpreted result messages as well;
Mon, 10 Dec 2012 16:06:57 +0100 wenzelm more generous tracing limit -- rescaled in MB;
Thu, 29 Nov 2012 10:45:25 +0100 wenzelm more uniform ML statistics;
Wed, 28 Nov 2012 17:18:53 +0100 wenzelm some support for ML runtime statistics;
Wed, 28 Nov 2012 16:09:05 +0100 wenzelm prefer tight Markup.print_int/parse_int for property values;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Sun, 18 Nov 2012 16:04:13 +0100 wenzelm more generous tracing_limit, with explicit system option;
Sun, 18 Nov 2012 15:28:58 +0100 wenzelm update options via protocol;
Mon, 01 Oct 2012 20:17:30 +0200 wenzelm more direct message header: eliminated historic encoding via single letter;
Sat, 29 Sep 2012 19:28:03 +0200 wenzelm enable show_markup by default (approx. double output size);
Fri, 28 Sep 2012 16:51:58 +0200 wenzelm smarter handling of tracing messages;
Tue, 25 Sep 2012 22:36:06 +0200 wenzelm basic integration of graphview into document model;
Tue, 04 Sep 2012 00:16:03 +0200 wenzelm enable parallel terminal proofs in interaction;
Tue, 07 Aug 2012 19:16:58 +0200 wenzelm simplified process startup phases: INIT suffices for is_ready;
Tue, 07 Aug 2012 17:08:22 +0200 wenzelm prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
Tue, 07 Aug 2012 16:34:15 +0200 wenzelm prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
Fri, 01 Jun 2012 13:02:09 +0200 wenzelm tuned message;
Mon, 09 Apr 2012 23:06:14 +0200 wenzelm disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;
Sat, 07 Apr 2012 19:59:09 +0200 wenzelm enable parallel proofs (cf. e8552cba702d), only affects packages so far;
Sat, 03 Mar 2012 18:18:39 +0100 wenzelm clarified terminology of raw protocol messages;
Mon, 20 Feb 2012 15:36:48 +0100 wenzelm clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
Thu, 05 Jan 2012 14:15:37 +0100 wenzelm prefer raw_message for protocol implementation;
Thu, 05 Jan 2012 13:24:29 +0100 wenzelm tuned signature -- emphasize special nature of protocol commands;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Mon, 17 Oct 2011 11:24:22 +0200 wenzelm always use sockets on Windows/Cygwin;
Fri, 23 Sep 2011 14:13:15 +0200 wenzelm default print mode for Isabelle/Scala, not just Isabelle/jEdit;
Thu, 22 Sep 2011 20:33:08 +0200 wenzelm abstract System_Channel in ML (cf. Scala version);
Wed, 21 Sep 2011 22:18:17 +0200 wenzelm alternative Socket_Channel;
Mon, 19 Sep 2011 16:40:17 +0200 wenzelm at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
Tue, 06 Sep 2011 10:16:12 +0200 wenzelm flush after Output.raw_message (and init message) for reduced latency of important protocol events;
Tue, 23 Aug 2011 16:53:05 +0200 wenzelm tuned signature -- contrast physical output primitives versus Output.raw_message;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Tue, 12 Jul 2011 13:45:05 +0200 wenzelm clarified YXML.embed_controls -- this is idempotent and cannot be nested;
Tue, 12 Jul 2011 13:39:29 +0200 wenzelm allow empty body for raw_message -- important for Invoke_Scala;
Mon, 11 Jul 2011 11:13:33 +0200 wenzelm some support for raw messages, which bypass standard Symbol/YXML decoding;
less more (0) -100 -60 tip