# HG changeset patch
# User wenzelm
# Date 1551455381 -3600
# Node ID 29a4f633609e4fa429b3bc46941f4d7751046ee6
# Parent  5f993636ac079a85514d08c3c59515fd734f61f7
clarified signature;
more thorough end_pos;

diff -r 5f993636ac07 -r 29a4f633609e src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Feb 28 21:59:58 2019 +0100
+++ b/src/Pure/Isar/token.ML	Fri Mar 01 16:49:41 2019 +0100
@@ -64,6 +64,7 @@
   val unparse: T -> string
   val print: T -> string
   val text_of: T -> string * string
+  val file_source: file -> Input.source
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
   val get_value: T -> value option
@@ -365,6 +366,12 @@
 
 (* inlined file content *)
 
+fun file_source (file: file) =
+  let
+    val text = cat_lines (#lines file);
+    val end_pos = fold Position.advance (Symbol.explode text) (#pos file);
+  in Input.source true text (Position.range (#pos file, end_pos)) end;
+
 fun get_files (Token (_, _, Value (SOME (Files files)))) = files
   | get_files _ = [];
 
diff -r 5f993636ac07 -r 29a4f633609e src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Thu Feb 28 21:59:58 2019 +0100
+++ b/src/Pure/ML/ml_file.ML	Fri Mar 01 16:49:41 2019 +0100
@@ -17,9 +17,9 @@
 
 fun command environment debug files = Toplevel.generic_theory (fn gthy =>
   let
-    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
-    val provide = Resources.provide (src_path, digest);
-    val source = Input.source true (cat_lines lines) (pos, pos);
+    val [file: Token.file] = files (Context.theory_of gthy);
+    val provide = Resources.provide_file file;
+    val source = Token.file_source file;
 
     val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
diff -r 5f993636ac07 -r 29a4f633609e src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Thu Feb 28 21:59:58 2019 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Mar 01 16:49:41 2019 +0100
@@ -31,6 +31,7 @@
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   val parse_files: string -> (theory -> Token.file list) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
+  val provide_file: Token.file -> theory -> theory
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val loaded_files_current: theory -> bool
   val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
@@ -215,6 +216,8 @@
       error ("Duplicate use of source file: " ^ Path.print src_path)
     else (master_dir, imports, (src_path, id) :: provided));
 
+fun provide_file (file: Token.file) = provide (#src_path file, #digest file);
+
 fun provide_parse_files cmd =
   parse_files cmd >> (fn files => fn thy =>
     let