equal
deleted
inserted
replaced
64 (case try Url.explode file_node of |
64 (case try Url.explode file_node of |
65 NONE => () |
65 NONE => () |
66 | SOME (Url.File _) => () |
66 | SOME (Url.File _) => () |
67 | _ => |
67 | _ => |
68 error ("Prover cannot load remote file " ^ |
68 error ("Prover cannot load remote file " ^ |
69 Markup.markup (Markup.path file_node) (quote file_node))); |
69 Markup.markup (Markup.url file_node) (quote file_node))); |
70 val full_path = File.check_file (File.full_path master_dir src_path); |
70 val full_path = File.check_file (File.full_path master_dir src_path); |
71 val text = File.read full_path; |
71 val text = File.read full_path; |
72 val lines = split_lines text; |
72 val lines = split_lines text; |
73 val digest = SHA1.digest text; |
73 val digest = SHA1.digest text; |
74 val file_pos = Position.copy_id pos (Path.position full_path); |
74 val file_pos = Position.copy_id pos (Path.position full_path); |