| #
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
|