2016-04-09 wenzelm [Sat, 09 Apr 2016 16:16:05 +0200] rev 62930
shared output primitives of physical/virtual Pure;
src/Pure/General/output.ML src/Pure/General/output.scala src/Pure/General/output_primitives.ML src/Pure/General/output_primitives_virtual.ML src/Pure/ML/ml_name_space.ML src/Pure/ML_Bootstrap.thy src/Pure/ROOT.ML src/Pure/ROOT0.ML src/Pure/System/isabelle_process.ML src/Pure/Tools/build.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:52:10 +0200] rev 62929
shared thread position for physical/virtual Pure;
src/Pure/Concurrent/thread_position.ML src/Pure/General/position.ML src/Pure/ML/ml_name_space.ML src/Pure/ROOT0.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:40:00 +0200] rev 62928
prefer Synchronized.var;
src/Pure/PIDE/session.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:28:32 +0200] rev 62927
tuned signature;
src/Pure/Concurrent/multithreading.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:21:29 +0200] rev 62926
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
src/Pure/Concurrent/multithreading.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:17:50 +0200] rev 62925
tuned signature;
src/HOL/TPTP/MaSh_Eval.thy src/HOL/TPTP/MaSh_Export_Base.thy src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML src/Pure/Concurrent/future.ML src/Pure/Concurrent/multithreading.ML src/Pure/Tools/build.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:11:31 +0200] rev 62924
tuned signature -- closer to Exn.Interrupt.expose in Scala;
src/Pure/Concurrent/future.ML src/Pure/Concurrent/multithreading.ML src/Pure/Concurrent/thread_attributes.ML src/Pure/Concurrent/timeout.ML src/Pure/PIDE/command.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 14:00:23 +0200] rev 62923
clarified bootstrap;
src/Pure/Concurrent/event_timer.ML src/Pure/Concurrent/future.ML src/Pure/Concurrent/lazy.ML src/Pure/Concurrent/multithreading.ML src/Pure/Concurrent/par_list.ML src/Pure/Concurrent/single_assignment.ML src/Pure/Concurrent/standard_thread.ML src/Pure/Concurrent/synchronized.ML src/Pure/Concurrent/task_queue.ML src/Pure/Concurrent/thread_attributes.ML src/Pure/Concurrent/thread_data.ML src/Pure/Concurrent/thread_data_virtual.ML src/Pure/Concurrent/timeout.ML src/Pure/Concurrent/unsynchronized.ML src/Pure/General/exn.ML src/Pure/ML/exn_debugger.ML src/Pure/ML/exn_properties.ML src/Pure/ML/ml_name_space.ML src/Pure/ML/ml_pervasive0.ML src/Pure/ML/ml_pervasive1.ML src/Pure/PIDE/execution.ML src/Pure/PIDE/query_operation.ML src/Pure/ROOT.ML src/Pure/ROOT0.ML src/Pure/System/bash.ML src/Pure/System/command_line.ML src/Pure/System/isabelle_process.ML src/Pure/Thy/thy_info.ML src/Pure/Tools/debugger.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 13:28:32 +0200] rev 62922
clarified context;
avoid Unsynchronized.ref;
src/Doc/Implementation/Logic.thy src/HOL/Extraction.thy src/HOL/Proofs/ex/Proof_Terms.thy src/HOL/Proofs/ex/XML_Data.thy src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/inductive_realizer.ML src/Pure/Isar/isar_cmd.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_rewrite_rules.ML src/Pure/Proof/proof_syntax.ML src/Pure/Proof/reconstruct.ML

2016-04-09 wenzelm [Sat, 09 Apr 2016 12:36:25 +0200] rev 62921
old;
src/HOL/Main.thy