src/Pure/Thy/thy_load.ML

--- a/src/Pure/Thy/thy_load.ML	Mon Aug 20 21:52:31 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Aug 21 11:00:54 2012 +0200
@@ -73,6 +73,59 @@
     else (master_dir, imports, required, (src_path, path_id) :: provided));
 
 
+(* inlined files *)
+
+fun command_files cmd path =
+  (case Keyword.command_files cmd of
+    [] => [path]
+  | exts => map (fn ext => Path.ext ext path) exts);
+
+fun read_files cmd dir tok =
+  let
+    val path = Path.explode (Token.content_of tok);
+    val files =
+      command_files cmd path
+      |> map (Path.append dir #> (fn p => (File.read p, Path.position p)));
+  in (dir, files) end;
+
+fun parse_files cmd =
+  Scan.ahead Parse.not_eof -- Parse.group (fn () => "file name/path specification") Parse.name
+    >> (fn (tok, name) => fn thy =>
+      (case Token.get_files tok of
+        SOME files => files
+      | NONE =>
+          (warning ("Dynamic loading of files: " ^ quote name ^ Token.pos_of tok);
+            read_files cmd (master_directory thy) tok)));
+
+local
+
+fun clean ((i1, t1) :: (i2, t2) :: toks) =
+      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
+      else (i1, t1) :: clean ((i2, t2) :: toks)
+  | clean toks = toks;
+
+fun clean_tokens toks =
+  ((0 upto length toks - 1) ~~ toks)
+  |> filter (fn (_, tok) => Token.is_proper tok) |> clean;
+
+in
+
+fun resolve_files dir (span as Thy_Syntax.Span (Thy_Syntax.Command cmd, toks)) =
+      if Keyword.is_theory_load cmd then
+        (case find_first (Token.is_name o #2) (rev (clean_tokens toks)) of
+          NONE => span
+        | SOME (i, _) =>
+            let
+              val toks' = toks |> map_index (fn (j, tok) =>
+                if i = j then Token.put_files (read_files cmd dir tok) tok
+                else tok);
+            in Thy_Syntax.Span (Thy_Syntax.Command cmd, toks') end)
+      else span
+  | resolve_files _ span = span;
+
+end;
+
+
 (* check files *)
 
 fun check_file dir file = File.check_file (File.full_path dir file);
@@ -160,51 +213,6 @@
 fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
 
 
-(* inlined files *)
-
-fun read_files cmd dir tok =
-  let
-    val path = Path.explode (Token.content_of tok);
-    val exts = Keyword.command_files cmd;
-    val variants =
-      if null exts then [path]
-      else map (fn ext => Path.ext ext path) exts;
-  in (dir, variants |> map (Path.append dir #> (fn p => (File.read p, Path.position p)))) end;
-
-
-fun clean ((i1, t1) :: (i2, t2) :: toks) =
-      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
-      else (i1, t1) :: clean ((i2, t2) :: toks)
-  | clean toks = toks;
-
-fun clean_tokens toks =
-  ((0 upto length toks - 1) ~~ toks)
-  |> filter (fn (_, tok) => Token.is_proper tok) |> clean;
-
-fun resolve_files dir (span as Thy_Syntax.Span (Thy_Syntax.Command cmd, toks)) =
-      if Keyword.is_theory_load cmd then
-        (case find_first (Token.is_name o #2) (rev (clean_tokens toks)) of
-          NONE => span
-        | SOME (i, _) =>
-            let
-              val toks' = toks |> map_index (fn (j, tok) =>
-                if i = j then Token.put_files (read_files cmd dir tok) tok
-                else tok);
-            in Thy_Syntax.Span (Thy_Syntax.Command cmd, toks') end)
-      else span
-  | resolve_files _ span = span;
-
-fun parse_files cmd =
-  Scan.ahead Parse.not_eof -- Parse.group (fn () => "file name/path specification") Parse.name
-    >> (fn (tok, name) => fn thy =>
-      (case Token.get_files tok of
-        SOME files => files
-      | NONE =>
-          (warning ("Dynamic loading of files: " ^ quote name ^
-              Position.str_of (Token.position_of tok));
-            read_files cmd (master_directory thy) tok)));
-
-
 (* load_thy *)
 
 fun begin_theory dir {name, imports, keywords, uses} parents =