clarified signature;
authorwenzelm
Fri Mar 01 16:49:41 2019 +0100 (7 weeks ago ago)
changeset 7003229a4f633609e
parent 70031 5f993636ac07
child 70033 54243334edcf
clarified signature;
more thorough end_pos;
src/Pure/Isar/token.ML
src/Pure/ML/ml_file.ML
src/Pure/PIDE/resources.ML
     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  
     2.1 --- a/src/Pure/ML/ml_file.ML	Thu Feb 28 21:59:58 2019 +0100
     2.2 +++ b/src/Pure/ML/ml_file.ML	Fri Mar 01 16:49:41 2019 +0100
     2.3 @@ -17,9 +17,9 @@
     2.4  
     2.5  fun command environment debug files = Toplevel.generic_theory (fn gthy =>
     2.6    let
     2.7 -    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     2.8 -    val provide = Resources.provide (src_path, digest);
     2.9 -    val source = Input.source true (cat_lines lines) (pos, pos);
    2.10 +    val [file: Token.file] = files (Context.theory_of gthy);
    2.11 +    val provide = Resources.provide_file file;
    2.12 +    val source = Token.file_source file;
    2.13  
    2.14      val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
    2.15  
     3.1 --- a/src/Pure/PIDE/resources.ML	Thu Feb 28 21:59:58 2019 +0100
     3.2 +++ b/src/Pure/PIDE/resources.ML	Fri Mar 01 16:49:41 2019 +0100
     3.3 @@ -31,6 +31,7 @@
     3.4      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
     3.5    val parse_files: string -> (theory -> Token.file list) parser
     3.6    val provide: Path.T * SHA1.digest -> theory -> theory
     3.7 +  val provide_file: Token.file -> theory -> theory
     3.8    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     3.9    val loaded_files_current: theory -> bool
    3.10    val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
    3.11 @@ -215,6 +216,8 @@
    3.12        error ("Duplicate use of source file: " ^ Path.print src_path)
    3.13      else (master_dir, imports, (src_path, id) :: provided));
    3.14  
    3.15 +fun provide_file (file: Token.file) = provide (#src_path file, #digest file);
    3.16 +
    3.17  fun provide_parse_files cmd =
    3.18    parse_files cmd >> (fn files => fn thy =>
    3.19      let