src/Pure/Isar/token.ML
changeset 70032 29a4f633609e
parent 68730 0bc491938780
child 70072 def3ec9cdb7e
     1.1 --- a/src/Pure/Isar/token.ML	Thu Feb 28 21:59:58 2019 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Fri Mar 01 16:49:41 2019 +0100
     1.3 @@ -64,6 +64,7 @@
     1.4    val unparse: T -> string
     1.5    val print: T -> string
     1.6    val text_of: T -> string * string
     1.7 +  val file_source: file -> Input.source
     1.8    val get_files: T -> file Exn.result list
     1.9    val put_files: file Exn.result list -> T -> T
    1.10    val get_value: T -> value option
    1.11 @@ -365,6 +366,12 @@
    1.12  
    1.13  (* inlined file content *)
    1.14  
    1.15 +fun file_source (file: file) =
    1.16 +  let
    1.17 +    val text = cat_lines (#lines file);
    1.18 +    val end_pos = fold Position.advance (Symbol.explode text) (#pos file);
    1.19 +  in Input.source true text (Position.range (#pos file, end_pos)) end;
    1.20 +
    1.21  fun get_files (Token (_, _, Value (SOME (Files files)))) = files
    1.22    | get_files _ = [];
    1.23