simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;

--- a/src/Pure/Isar/keyword.ML	Thu Aug 23 12:00:11 2012 +0200
+++ b/src/Pure/Isar/keyword.ML	Thu Aug 23 12:33:42 2012 +0200
@@ -57,7 +57,6 @@
   val command_tags: string -> string list
   val dest: unit -> string list * string list
   val status: unit -> unit
-  val thy_load_commands: keywords -> (string * string list) list
   val define_keywords: string * T option -> keywords -> keywords
   val define: string * T option -> unit
   val is_diag: string -> bool
@@ -221,11 +220,6 @@
   in () end;
 
 
-fun thy_load_commands (Keywords {commands, ...}) =
-  Symtab.fold (fn (name, Keyword {kind, files, ...}) =>
-      kind = kind_of thy_load ? cons (name, files)) commands [];
-
-
 (* define *)
 
 fun define_keywords (name, opt_kind) = map_keywords (fn ((minor, major), commands) =>

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 23 12:00:11 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 23 12:33:42 2012 +0200
@@ -594,14 +594,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val filerefs = map #1 (#uses (Thy_Load.check_thy [] (Path.dir f) thy))
+                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val thyrefs = #imports (Thy_Load.check_thy [] Path.current thy)
+            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,

--- a/src/Pure/Thy/thy_info.ML	Thu Aug 23 12:00:11 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Aug 23 12:33:42 2012 +0200
@@ -236,16 +236,16 @@
     fun commit () = update_thy deps theory;
   in (theory, present, commit) end;
 
-fun check_deps base_keywords dir name =
+fun check_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, get_imports name, [], [])
   | NONE =>
-      let val {master, text, imports, keywords, uses} = Thy_Load.check_thy base_keywords dir name
+      let val {master, text, imports, keywords, uses} = Thy_Load.check_thy 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', uses = uses', keywords = keywords'}
-          = Thy_Load.check_thy base_keywords dir name;
+          = Thy_Load.check_thy dir name;
         val deps' = SOME (make_deps master' imports', text');
         val current =
           #2 master = #2 master' andalso
@@ -256,29 +256,29 @@
 
 in
 
-fun require_thys initiators dir strs result =
-      fold_map (require_thy initiators dir) strs result |>> forall I
-and require_thy initiators dir str (base_keywords, tasks) =
+fun require_thys initiators dir strs tasks =
+      fold_map (require_thy initiators dir) strs tasks |>> forall I
+and require_thy initiators dir str tasks =
   let
     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
   in
     (case try (Graph.get_node tasks) name of
-      SOME task => (task_finished task, (base_keywords, tasks))
+      SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val dir' = Path.append dir (Path.dir path);
           val _ = member (op =) initiators name andalso error (cycle_msg initiators);
 
-          val (current, deps, imports, uses, keywords) = check_deps base_keywords dir' name
+          val (current, deps, imports, uses, keywords) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
 
           val parents = map base_name imports;
-          val (parents_current, (base_keywords', tasks')) =
+          val (parents_current, tasks') =
             require_thys (name :: initiators)
-              (Path.append dir (master_dir (Option.map #1 deps))) imports (base_keywords, tasks);
+              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
@@ -292,9 +292,8 @@
                     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';
-        in (all_current, (base_keywords'', tasks'')) end)
+        in (all_current, tasks'') end)
   end;
 
 end;
@@ -303,7 +302,7 @@
 (* use_thy *)
 
 fun use_thys_wrt dir arg =
-  schedule_tasks (snd (snd (require_thys [] dir arg ([], Graph.empty))));
+  schedule_tasks (snd (require_thys [] dir arg Graph.empty));
 
 val use_thys = use_thys_wrt Path.current;
 val use_thy = use_thys o single;
@@ -326,7 +325,7 @@
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val {master, ...} = Thy_Load.check_thy [] (Thy_Load.master_directory theory) name;
+    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val imports = Thy_Load.imports_of theory;
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>

--- a/src/Pure/Thy/thy_load.ML	Thu Aug 23 12:00:11 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 23 12:33:42 2012 +0200
@@ -10,7 +10,7 @@
   val imports_of: theory -> string list
   val provide: Path.T * SHA1.digest -> theory -> theory
   val thy_path: Path.T -> Path.T
-  val check_thy: Thy_Header.keywords -> Path.T -> string ->
+  val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, imports: string list,
     uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
@@ -69,6 +69,21 @@
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
+fun read_files cmd dir path =
+  let
+    val paths =
+      (case Keyword.command_files cmd of
+        [] => [path]
+      | exts => map (fn ext => Path.ext ext path) exts);
+    val files = paths |> map (check_file dir #> (fn p => (File.read p, Path.position p)));
+  in (dir, files) end;
+
+fun parse_files cmd =
+  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
+    (case Token.get_files tok of
+      SOME files => files
+    | NONE => read_files cmd (master_directory thy) (Path.explode name)));
+
 local
 
 fun clean ((i1, t1) :: (i2, t2) :: toks) =
@@ -88,42 +103,8 @@
         handle ERROR msg => error (msg ^ Token.pos_of tok)
     else NONE);
 
-fun command_files path exts =
-  if null exts then [path]
-  else map (fn ext => Path.ext ext path) exts;
-
 in
 
-fun find_files syntax text =
-  let val thy_load_commands = Keyword.thy_load_commands syntax in
-    if exists (fn (cmd, _) => String.isSubstring cmd text) thy_load_commands then
-      Thy_Syntax.parse_tokens (Keyword.lexicons_of syntax) Position.none text
-      |> Thy_Syntax.parse_spans
-      |> maps
-        (fn Thy_Syntax.Span (Thy_Syntax.Command (cmd, _), toks) =>
-              (case AList.lookup (op =) thy_load_commands cmd of
-                SOME exts =>
-                  (case find_file toks of
-                    SOME (_, path) => command_files path exts
-                  | NONE => [])
-              | NONE => [])
-          | _ => [])
-    else []
-  end;
-
-fun read_files cmd dir path =
-  let
-    val files =
-      command_files path (Keyword.command_files cmd)
-      |> map (check_file dir #> (fn p => (File.read p, Path.position p)));
-  in (dir, files) end;
-
-fun parse_files cmd =
-  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
-    (case Token.get_files tok of
-      SOME files => files
-    | NONE => read_files cmd (master_directory thy) (Path.explode name)));
-
 fun resolve_files master_dir span =
   (case span of
     Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
@@ -146,7 +127,7 @@
 
 val thy_path = Path.ext "thy";
 
-fun check_thy base_keywords dir thy_name =
+fun check_thy dir thy_name =
   let
     val path = thy_path (Path.basic thy_name);
     val master_file = check_file dir path;
@@ -155,14 +136,9 @@
     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 @ more_uses, keywords = keywords}
+    imports = imports, uses = uses, keywords = keywords}
   end;