Changes

Summary

load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature;
clarified modules;
clarified modules;
ML debugger support in Pure (again, see 3565c9f407ec);
use bootstrap compiler earlier;

Changeset 62493:dd154240a53c by wenzelm: load secure.ML earlier;<br>eliminated obsolete ml_parse.ML;<br>tuned signature;
The file was added	`src/Pure/RAW/secure.ML`
The file was modified	`src/HOL/Tools/Quickcheck/narrowing_generators.ML` (diff)
The file was modified	`src/Pure/ML/ml_compiler.ML` (diff)
The file was modified	`src/Pure/ML/ml_env.ML` (diff)
The file was modified	`src/Pure/RAW/ROOT_polyml.ML` (diff)
The file was modified	`src/Pure/RAW/compiler_polyml.ML` (diff)
The file was modified	`src/Pure/ROOT` (diff)
The file was modified	`src/Pure/ROOT.ML` (diff)
The file was modified	`src/Tools/Code/code_runtime.ML` (diff)
The file was modified	`src/Tools/Spec_Check/spec_check.ML` (diff)
The file was removed	`src/Pure/General/secure.ML`
The file was removed	`src/Pure/ML/ml_parse.ML`
Changeset 62492:0e53fade87fe by wenzelm: clarified modules;
The file was modified	`src/Pure/PIDE/document.scala` (diff)
The file was modified	`src/Pure/RAW/exn.ML` (diff)
The file was modified	`src/Pure/RAW/exn.scala` (diff)
The file was modified	`src/Pure/ROOT.scala` (diff)
The file was modified	`src/Pure/System/process_result.scala` (diff)
The file was modified	`src/Pure/library.scala` (diff)
Changeset 62491:7187cb7a77c5 by wenzelm: clarified modules;
The file was modified	`src/Pure/General/scan.ML` (diff)
The file was modified	`src/Pure/RAW/exn.ML` (diff)
The file was modified	`src/Pure/library.ML` (diff)
Changeset 62490:39d01eaf5292 by wenzelm: ML debugger support in Pure (again, see 3565c9f407ec);
The file was modified	`src/Pure/ML/ml_compiler.ML` (diff)
The file was modified	`src/Pure/Pure.thy` (diff)
The file was modified	`src/Pure/RAW/ROOT_polyml.ML` (diff)
The file was modified	`src/Pure/RAW/compiler_polyml.ML` (diff)
The file was modified	`src/Pure/ROOT` (diff)
The file was modified	`src/Pure/ROOT.ML` (diff)
The file was modified	`src/Pure/Tools/build.scala` (diff)
The file was removed	`src/Pure/RAW/use_context.ML`
Changeset 62489:36f11bc393a2 by wenzelm: use bootstrap compiler earlier;
The file was modified	`src/Pure/RAW/compiler_polyml.ML` (diff)
The file was modified	`src/Pure/RAW/use_context.ML` (diff)