Tue, 30 Sep 2008 22:02:51 +0200 begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm [Tue, 30 Sep 2008 22:02:51 +0200] rev 28433
begin_proof: avoid race condition wrt. skip_proofs flag; replaced command_excursion by excursion, which is based on units of command/proof pairs; excursion: basic support for proof promises;
Tue, 30 Sep 2008 22:02:50 +0200 load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm [Tue, 30 Sep 2008 22:02:50 +0200] rev 28432
load_thy: Toplevel.excursion based on units of command/proof pairs;
Tue, 30 Sep 2008 22:02:47 +0200 more command categories;
wenzelm [Tue, 30 Sep 2008 22:02:47 +0200] rev 28431
more command categories; tuned;
Tue, 30 Sep 2008 22:02:45 +0200 renamed Future.fork_irrelevant to Future.fork_background;
wenzelm [Tue, 30 Sep 2008 22:02:45 +0200] rev 28430
renamed Future.fork_irrelevant to Future.fork_background; tuned;
Tue, 30 Sep 2008 22:02:44 +0200 export explicit joint_futures, removed Theory.at_end hook;
wenzelm [Tue, 30 Sep 2008 22:02:44 +0200] rev 28429
export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;
Tue, 30 Sep 2008 14:30:44 +0200 tuned
haftmann [Tue, 30 Sep 2008 14:30:44 +0200] rev 28428
tuned
Tue, 30 Sep 2008 14:19:28 +0200 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm [Tue, 30 Sep 2008 14:19:28 +0200] rev 28427
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
Tue, 30 Sep 2008 14:19:27 +0200 Toplevel.commit_exit: position;
wenzelm [Tue, 30 Sep 2008 14:19:27 +0200] rev 28426
Toplevel.commit_exit: position;
Tue, 30 Sep 2008 14:19:26 +0200 export setmp_thread_position;
wenzelm [Tue, 30 Sep 2008 14:19:26 +0200] rev 28425
export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;
Tue, 30 Sep 2008 14:19:25 +0200 simplified process_file, eliminated Toplevel.excursion;
wenzelm [Tue, 30 Sep 2008 14:19:25 +0200] rev 28424
simplified process_file, eliminated Toplevel.excursion; load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip