# HG changeset patch
# User wenzelm
# Date 1345578512 -7200
# Node ID 157dd47032e0060272ee2e6a4e53283d738ac9fb
# Parent  b629f037a0cb9b491649f5603e07b4d5928d5cfc
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy;
clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

diff -r b629f037a0cb -r 157dd47032e0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 21 21:25:45 2012 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 21 21:48:32 2012 +0200
@@ -324,12 +324,17 @@
 val _ =
   Outer_Syntax.command
     (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
-    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
-      let val (_, [(txt, pos)]) = files (Context.theory_of gthy) in
-        gthy
-        |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
-        |> Local_Theory.propagate_ml_env
-      end)));
+    (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
+      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
+        let
+          val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
+          val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
+        in
+          gthy
+          |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
+          |> Local_Theory.propagate_ml_env
+          |> Context.mapping provide (Local_Theory.background_theory provide)
+        end)));
 
 Unsynchronized.setmp Multithreading.max_threads 1
   use_thy "Pure";
diff -r b629f037a0cb -r 157dd47032e0 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 21 21:25:45 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 21 21:48:32 2012 +0200
@@ -220,7 +220,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy initiators update_time deps text name parents =
+fun load_thy initiators update_time deps text name uses keywords parents =
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -228,7 +228,6 @@
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
-    val {uses, keywords, ...} = Thy_Header.read pos text;
     val header = Thy_Header.make name imports keywords uses;
 
     val (theory, present) =
@@ -239,21 +238,21 @@
 
 fun check_deps base_keywords dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_imports name, [])
+    SOME NONE => (true, NONE, get_imports name, [], [])
   | NONE =>
-      let val {master, text, imports, keywords, ...} = Thy_Load.check_thy base_keywords dir name
-      in (false, SOME (make_deps master imports, text), imports, keywords) end
+      let val {master, text, imports, keywords, uses} = Thy_Load.check_thy base_keywords dir name
+      in (false, SOME (make_deps master imports, text), imports, uses, keywords) end
   | SOME (SOME {master, ...}) =>
       let
-        val {master = master', text = text', imports = imports', keywords, ...} =
-          Thy_Load.check_thy base_keywords dir name;
+        val {master = master', text = text', imports = imports', uses = uses', keywords = keywords'}
+          = Thy_Load.check_thy base_keywords dir name;
         val deps' = SOME (make_deps master' imports', text');
         val current =
           #2 master = #2 master' andalso
             (case lookup_theory name of
               NONE => false
             | SOME theory => Thy_Load.all_current theory);
-      in (current, deps', imports', keywords) end);
+      in (current, deps', imports', uses', keywords') end);
 
 in
 
@@ -271,7 +270,7 @@
           val dir' = Path.append dir (Path.dir path);
           val _ = member (op =) initiators name andalso error (cycle_msg initiators);
 
-          val (current, deps, imports, keywords) = check_deps base_keywords dir' name
+          val (current, deps, imports, uses, keywords) = check_deps base_keywords dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
@@ -288,8 +287,10 @@
               (case deps of
                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
-                  let val update_time = serial ()
-                  in Task (parents, load_thy initiators update_time dep text name) end);
+                  let
+                    val update_time = serial ();
+                    val load = load_thy initiators update_time dep text name uses keywords;
+                  in Task (parents, load) end);
 
           val base_keywords'' = keywords @ base_keywords';
           val tasks'' = new_entry name parents task tasks';
diff -r b629f037a0cb -r 157dd47032e0 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Aug 21 21:25:45 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Aug 21 21:48:32 2012 +0200
@@ -11,9 +11,9 @@
   val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
   val check_file: Path.T -> Path.T -> Path.T
   val thy_path: Path.T -> Path.T
-  val check_thy: (string * Keyword.T option) list -> Path.T -> string ->
+  val check_thy: Thy_Header.keywords -> Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, imports: string list,
-    uses: (Path.T * bool) list, keywords: (string * Keyword.T option) list}
+    uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   val use_file: Path.T -> theory -> string * theory
   val loaded_files: theory -> Path.T list
@@ -157,28 +157,23 @@
 
 val thy_path = Path.ext "thy";
 
-fun check_thy base_keywords dir name =
+fun check_thy base_keywords dir thy_name =
   let
-    val path = thy_path (Path.basic name);
+    val path = thy_path (Path.basic thy_name);
     val master_file = check_file dir path;
     val text = File.read master_file;
-    val (name', imports, uses, more_keywords) =
-      if name = Context.PureN then (Context.PureN, [], [], [])
-      else
-        let
-          val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
-          val more_keywords = map (apsnd (Option.map Keyword.spec)) keywords;
-          val syntax =
-            Keyword.get_keywords ()
-            |> fold Keyword.define_keywords base_keywords
-            |> fold Keyword.define_keywords more_keywords;
-          val more_uses = map (rpair false) (find_files syntax text);
-        in (name, imports, uses @ more_uses, more_keywords) end;
-    val _ = name <> name' andalso
-      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
+
+    val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
+    val _ = thy_name <> name andalso
+      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name);
+
+    val syntax =
+      fold (Keyword.define_keywords o apsnd (Option.map Keyword.spec))
+        (keywords @ base_keywords) (Keyword.get_keywords ());
+    val more_uses = map (rpair false) (find_files syntax text);
   in
    {master = (master_file, SHA1.digest text), text = text,
-    imports = imports, uses = uses, keywords = more_keywords}
+    imports = imports, uses = uses @ more_uses, keywords = keywords}
   end;