tuned signature;

--- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:52:01 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 18:08:57 2013 +0100
@@ -9,6 +9,7 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
+  val read_files: Path.T -> string -> Path.T * Position.T -> Token.file list
   val parse_files: string -> (theory -> Token.file list) parser
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
@@ -55,11 +56,11 @@
 fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
 
 
-(* inlined files *)
+(* auxiliary files *)
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
-fun read_files cmd dir (path, pos) =
+fun read_files dir cmd (path, pos) =
   let
     fun make_file file =
       let
@@ -76,48 +77,10 @@
   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, Token.position_of 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;
-
-fun find_file toks =
-  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
-    if Token.is_name tok then
-      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
-        handle ERROR msg => error (msg ^ Token.pos_of tok)
-    else NONE);
-
-in
-
-fun resolve_files master_dir span =
-  (case span of
-    Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
-      if Keyword.is_theory_load cmd then
-        (case find_file toks of
-          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
-        | SOME (i, path) =>
-            let
-              val toks' = toks |> map_index (fn (j, tok) =>
-                if i = j then Token.put_files (read_files cmd master_dir path) tok
-                else tok);
-            in Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks') end)
-      else span
-  | span => span);
-
-end;
+    | NONE => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)));
 
 
-(* check files *)
+(* theory files *)
 
 val thy_path = Path.ext "thy";
 
@@ -213,7 +176,7 @@
     val lexs = Keyword.get_lexicons ();
 
     val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
+    val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
     val elements = Thy_Syntax.parse_elements spans;
 
     val _ = Present.theory_source name

--- a/src/Pure/Thy/thy_syntax.ML	Sat Nov 16 17:52:01 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sat Nov 16 18:08:57 2013 +0100
@@ -15,6 +15,7 @@
   val span_content: span -> Token.T list
   val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
+  val resolve_files: (string -> Path.T * Position.T -> Token.file list) -> span -> span
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
   val map_element: ('a -> 'b) -> 'a element -> 'b element
@@ -142,6 +143,47 @@
 end;
 
 
+(* inlined files *)
+
+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;
+
+fun find_file toks =
+  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
+    if Token.is_name tok then
+      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
+        handle ERROR msg => error (msg ^ Token.pos_of tok)
+    else NONE);
+
+in
+
+fun resolve_files read_files span =
+  (case span of
+    Span (Command (cmd, pos), toks) =>
+      if Keyword.is_theory_load cmd then
+        (case find_file toks of
+          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
+        | SOME (i, path) =>
+            let
+              val toks' = toks |> map_index (fn (j, tok) =>
+                if i = j then Token.put_files (read_files cmd path) tok
+                else tok);
+            in Span (Command (cmd, pos), toks') end)
+      else span
+  | _ => span);
+
+end;
+
+
 
 (** specification elements: commands with optional proof **)