clarified type Token.file;

--- a/src/Pure/Isar/token.ML	Thu Aug 23 13:31:00 2012 +0200
+++ b/src/Pure/Isar/token.ML	Thu Aug 23 13:55:27 2012 +0200
@@ -10,10 +10,10 @@
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
     Error of string | Sync | EOF
-  type files = Path.T * (string * Position.T) list
+  type file = {src_path: Path.T, text: string, pos: Position.T}
   datatype value =
     Text of string | Typ of typ | Term of term | Fact of thm list |
-    Attribute of morphism -> attribute | Files of files
+    Attribute of morphism -> attribute | Files of file list
   type T
   val str_of_kind: kind -> string
   val position_of: T -> Position.T
@@ -44,8 +44,8 @@
   val content_of: T -> string
   val unparse: T -> string
   val text_of: T -> string * string
-  val get_files: T -> files option
-  val put_files: files -> T -> T
+  val get_files: T -> file list option
+  val put_files: file list -> T -> T
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val mk_text: string -> T
@@ -78,7 +78,7 @@
   args.ML).  Note that an assignable ref designates an intermediate
   state of internalization -- it is NOT meant to persist.*)
 
-type files = Path.T * (string * Position.T) list;  (*master dir, multiple file content*)
+type file = {src_path: Path.T, text: string, pos: Position.T};
 
 datatype value =
   Text of string |
@@ -86,7 +86,7 @@
   Term of term |
   Fact of thm list |
   Attribute of morphism -> attribute |
-  Files of files;
+  Files of file list;
 
 datatype slot =
   Slot |

--- a/src/Pure/Thy/thy_load.ML	Thu Aug 23 13:31:00 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 23 13:55:27 2012 +0200
@@ -22,7 +22,7 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
     theory list -> theory * unit future
-  val parse_files: string -> (theory -> Token.files) parser
+  val parse_files: string -> (theory -> Token.file list) parser
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
 end;
@@ -69,14 +69,17 @@
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
+fun make_file dir file =
+  let val full_path = check_file dir file
+  in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
+
 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;
+  in map (make_file dir) paths end;
 
 fun parse_files cmd =
   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>

--- 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)));