src/Pure/ROOT.ML
changeset 48876 157dd47032e0
parent 48867 e9beabf045ab
child 48879 cb5cdbb645cd
     1.1 --- a/src/Pure/ROOT.ML	Tue Aug 21 21:25:45 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Aug 21 21:48:32 2012 +0200
     1.3 @@ -324,12 +324,17 @@
     1.4  val _ =
     1.5    Outer_Syntax.command
     1.6      (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
     1.7 -    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
     1.8 -      let val (_, [(txt, pos)]) = files (Context.theory_of gthy) in
     1.9 -        gthy
    1.10 -        |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    1.11 -        |> Local_Theory.propagate_ml_env
    1.12 -      end)));
    1.13 +    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
    1.14 +      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
    1.15 +        let
    1.16 +          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
    1.17 +          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
    1.18 +        in
    1.19 +          gthy
    1.20 +          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    1.21 +          |> Local_Theory.propagate_ml_env
    1.22 +          |> Context.mapping provide (Local_Theory.background_theory provide)
    1.23 +        end)));
    1.24  
    1.25  Unsynchronized.setmp Multithreading.max_threads 1
    1.26    use_thy "Pure";