# HG changeset patch # User wenzelm # Date 1459779262 -7200 # Node ID 1bd1d84929316e635a5db5302c5ef87cc9494f43 # Parent 3c576c7f97313998290d62e9adbbd6783e4b7f75 clarified bootstrap; diff -r 3c576c7f9731 -r 1bd1d8492931 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Mon Apr 04 15:53:56 2016 +0200 +++ b/src/Doc/Implementation/Integration.thy Mon Apr 04 16:14:22 2016 +0200 @@ -152,7 +152,6 @@ text %mlref \ \begin{mldecls} @{index_ML use_thy: "string -> unit"} \\ - @{index_ML use_thys: "string list -> unit"} \\[0.5ex] @{index_ML Thy_Info.get_theory: "string -> theory"} \\ @{index_ML Thy_Info.remove_thy: "string -> unit"} \\ @{index_ML Thy_Info.register_thy: "theory -> unit"} \\ @@ -161,14 +160,6 @@ \<^descr> @{ML use_thy}~\A\ ensures that theory \A\ is fully up-to-date wrt.\ the external file store; outdated ancestors are reloaded on demand. - \<^descr> @{ML use_thys} is similar to @{ML use_thy}, but handles several theories - simultaneously. Thus it acts like processing the import header of a theory, - without performing the merge of the result. By loading a whole sub-graph of - theories, the intrinsic parallelism can be exploited by the system to - speedup loading. - - This variant is used by default in @{tool build} @{cite "isabelle-system"}. - \<^descr> @{ML Thy_Info.get_theory}~\A\ retrieves the theory value presently associated with name \A\. Note that the result might be outdated wrt.\ the file-system content. diff -r 3c576c7f9731 -r 1bd1d8492931 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Mon Apr 04 15:53:56 2016 +0200 +++ b/src/Doc/System/Environment.thy Mon Apr 04 16:14:22 2016 +0200 @@ -395,8 +395,8 @@ The user is connected to the raw ML toplevel loop: this is neither Isabelle/Isar nor Isabelle/ML within the usual formal context. The most - relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML - use_thys}. + relevant ML commands at this stage are @{ML use} (for ML files) and + @{ML use_thy} (for theory files). \ diff -r 3c576c7f9731 -r 1bd1d8492931 src/Pure/ML/ml_final.ML --- a/src/Pure/ML/ml_final.ML Mon Apr 04 15:53:56 2016 +0200 +++ b/src/Pure/ML/ml_final.ML Mon Apr 04 16:14:22 2016 +0200 @@ -12,10 +12,6 @@ structure Pure = struct val thy = Thy_Info.pure_theory () end; -fun use_thys args = - Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args)); -val use_thy = use_thys o single; - Proofterm.proofs := 0; Context.set_thread_data NONE; diff -r 3c576c7f9731 -r 1bd1d8492931 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Apr 04 15:53:56 2016 +0200 +++ b/src/Pure/ROOT.ML Mon Apr 04 16:14:22 2016 +0200 @@ -321,7 +321,7 @@ use "Tools/named_thms.ML"; use "ML/ml_pp.ML"; use "ML/ml_file.ML"; -Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none)); +use_thy "Pure"; (* final ML setup *) diff -r 3c576c7f9731 -r 1bd1d8492931 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Apr 04 15:53:56 2016 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Apr 04 16:14:22 2016 +0200 @@ -388,3 +388,5 @@ fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; + +fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy (name, Position.none));