author | wenzelm |
Tue, 07 Apr 2015 11:25:54 +0200 | |
changeset 59944 | 83071f4c8ae6 |
parent 59943 | e83ecf0a0ee1 |
child 59945 | cfbaee8cdf1d |
--- a/src/Pure/PIDE/command.ML Tue Apr 07 10:13:33 2015 +0200 +++ b/src/Pure/PIDE/command.ML Tue Apr 07 11:25:54 2015 +0200 @@ -51,6 +51,7 @@ fun read_file_node file_node master_dir pos src_path = let + val _ = Position.report pos Markup.language_path; val _ = (case try Url.explode file_node of NONE => ()