# HG changeset patch # User wenzelm # Date 918055867 -3600 # Node ID 128646d4a975bf66736947a19133ca70125035e0 # Parent 99f107fd478f6530103fc3ccdc059132dc3d86b5 of_file: Path.T, Position.T; diff -r 99f107fd478f -r 128646d4a975 src/Pure/General/source.ML --- a/src/Pure/General/source.ML Wed Feb 03 16:28:38 1999 +0100 +++ b/src/Pure/General/source.ML Wed Feb 03 16:31:07 1999 +0100 @@ -17,7 +17,7 @@ val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source val of_list: 'a list -> ('a, 'a list) source val of_string: string -> (string, string list) source - val of_file: string -> (string, string list) source + val of_file: Path.T -> (string, string list) source * Position.T val decorate_prompt_fn: (string -> string) ref val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source val tty: (string, unit) source @@ -108,7 +108,10 @@ fun of_list xs = make_source [] xs default_prompt drain_list; val of_string = of_list o explode; -val of_file = of_string o File.read; + +fun of_file raw_path = + let val path = Path.expand raw_path + in (of_string (File.read path), Position.line_name 1 (quote (Path.pack path))) end; (* stream source *)