equal
deleted
inserted
replaced
56 type blob = |
56 type blob = |
57 (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) |
57 (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) |
58 |
58 |
59 fun read_file_node file_node master_dir pos src_path = |
59 fun read_file_node file_node master_dir pos src_path = |
60 let |
60 let |
61 val _ = Position.report pos Markup.language_path; |
61 val _ = |
|
62 if Context_Position.pide_reports () |
|
63 then Position.report pos Markup.language_path else (); |
62 val _ = |
64 val _ = |
63 (case try Url.explode file_node of |
65 (case try Url.explode file_node of |
64 NONE => () |
66 NONE => () |
65 | SOME (Url.File _) => () |
67 | SOME (Url.File _) => () |
66 | _ => |
68 | _ => |