src/Pure/ML/ml_file.ML
changeset 70032 29a4f633609e
parent 68820 2e4df245754e
     1.1 --- a/src/Pure/ML/ml_file.ML	Thu Feb 28 21:59:58 2019 +0100
     1.2 +++ b/src/Pure/ML/ml_file.ML	Fri Mar 01 16:49:41 2019 +0100
     1.3 @@ -17,9 +17,9 @@
     1.4  
     1.5  fun command environment debug files = Toplevel.generic_theory (fn gthy =>
     1.6    let
     1.7 -    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     1.8 -    val provide = Resources.provide (src_path, digest);
     1.9 -    val source = Input.source true (cat_lines lines) (pos, pos);
    1.10 +    val [file: Token.file] = files (Context.theory_of gthy);
    1.11 +    val provide = Resources.provide_file file;
    1.12 +    val source = Token.file_source file;
    1.13  
    1.14      val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
    1.15