#
76687af0 |
|
09-May-2018 |
wenzelm <none@none> |
clarified future scheduling parameters, with support for parallel_limit;
|
#
f1670845 |
|
24-Apr-2018 |
wenzelm <none@none> |
clarified modules;
|
#
d8de6504 |
|
19-Feb-2018 |
wenzelm <none@none> |
clarified signature;
|
#
a33527e4 |
|
14-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
c26205a1 |
|
14-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
794cf015 |
|
13-Dec-2016 |
wenzelm <none@none> |
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
|
#
50338057 |
|
17-Oct-2016 |
wenzelm <none@none> |
eliminated unused argument;
|
#
8b8ff0c3 |
|
09-Apr-2016 |
wenzelm <none@none> |
tuned signature;
|
#
0d7124c4 |
|
09-Apr-2016 |
wenzelm <none@none> |
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
|
#
87ab331d |
|
09-Apr-2016 |
wenzelm <none@none> |
tuned signature;
|
#
db5a2118 |
|
09-Apr-2016 |
wenzelm <none@none> |
tuned signature -- closer to Exn.Interrupt.expose in Scala;
|
#
e5eeadb3 |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap;
|
#
e195e62f |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
#
85017fd2 |
|
06-Apr-2016 |
wenzelm <none@none> |
unused;
|
#
ff2c5cc2 |
|
06-Apr-2016 |
wenzelm <none@none> |
tuned signature;
|
#
185dcd47 |
|
02-Apr-2016 |
wenzelm <none@none> |
prefer infix operations;
|
#
06d08ecd |
|
26-Mar-2016 |
wenzelm <none@none> |
obsolete -- done in Isabelle_Process.init_options;
|
#
866c57fc |
|
03-Mar-2016 |
wenzelm <none@none> |
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; --HG-- rename : src/Pure/RAW/multithreading.ML => src/Pure/Concurrent/multithreading.ML rename : src/Pure/RAW/unsynchronized.ML => src/Pure/Concurrent/unsynchronized.ML rename : src/Pure/RAW/exn.ML => src/Pure/General/exn.ML rename : src/Pure/RAW/exn.scala => src/Pure/General/exn.scala rename : src/Pure/RAW/secure.ML => src/Pure/General/secure.ML rename : src/Pure/RAW/fixed_int_dummy.ML => src/Pure/ML/fixed_int_dummy.ML rename : src/Pure/RAW/ml_compiler0.ML => src/Pure/ML/ml_compiler0.ML rename : src/Pure/RAW/ml_debugger.ML => src/Pure/ML/ml_debugger.ML rename : src/Pure/RAW/ml_heap.ML => src/Pure/ML/ml_heap.ML rename : src/Pure/RAW/ml_name_space.ML => src/Pure/ML/ml_name_space.ML rename : src/Pure/RAW/ml_pretty.ML => src/Pure/ML/ml_pretty.ML rename : src/Pure/RAW/ml_profiling.ML => src/Pure/ML/ml_profiling.ML rename : src/Pure/RAW/ml_system.ML => src/Pure/ML/ml_system.ML
|