--- a/src/Pure/pure_syn.ML Thu Aug 23 13:31:00 2012 +0200
+++ b/src/Pure/pure_syn.ML Thu Aug 23 13:55:27 2012 +0200
@@ -18,15 +18,13 @@
val _ =
Outer_Syntax.command
(("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
- (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
- >> (fn (name, files) => Toplevel.generic_theory (fn gthy =>
+ (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
let
- val src_path = Path.explode name;
- val (_, [(txt, pos)]) = files (Context.theory_of gthy);
- val provide = Thy_Load.provide (src_path, SHA1.digest txt);
+ val [{src_path, text, pos}] = files (Context.theory_of gthy);
+ val provide = Thy_Load.provide (src_path, SHA1.digest text);
in
gthy
- |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
+ |> ML_Context.exec (fn () => ML_Context.eval_text true pos text)
|> Local_Theory.propagate_ml_env
|> Context.mapping provide (Local_Theory.background_theory provide)
end)));