58 fun read_file_node file_node master_dir pos delimited src_path = |
58 fun read_file_node file_node master_dir pos delimited src_path = |
59 let |
59 let |
60 val _ = |
60 val _ = |
61 if Context_Position.pide_reports () |
61 if Context_Position.pide_reports () |
62 then Position.report pos (Markup.language_path delimited) else (); |
62 then Position.report pos (Markup.language_path delimited) else (); |
63 val _ = |
63 |
|
64 fun read_file () = |
|
65 let |
|
66 val path = File.check_file (File.full_path master_dir src_path); |
|
67 val text = File.read path; |
|
68 val file_pos = Path.position path; |
|
69 in (text, file_pos) end; |
|
70 |
|
71 fun read_url () = |
|
72 let |
|
73 val text = Isabelle_System.download file_node; |
|
74 val file_pos = Position.file file_node; |
|
75 in (text, file_pos) end; |
|
76 |
|
77 val (text, file_pos) = |
64 (case try Url.explode file_node of |
78 (case try Url.explode file_node of |
65 NONE => () |
79 NONE => read_file () |
66 | SOME (Url.File _) => () |
80 | SOME (Url.File _) => read_file () |
67 | _ => |
81 | _ => read_url ()); |
68 error ("Prover cannot load remote file " ^ |
82 |
69 Markup.markup (Markup.url file_node) (quote file_node))); |
|
70 val full_path = File.check_file (File.full_path master_dir src_path); |
|
71 val text = File.read full_path; |
|
72 val lines = split_lines text; |
83 val lines = split_lines text; |
73 val digest = SHA1.digest text; |
84 val digest = SHA1.digest text; |
74 val file_pos = Position.copy_id pos (Path.position full_path); |
85 in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end |
75 in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end |
|
76 handle ERROR msg => error (msg ^ Position.here pos); |
86 handle ERROR msg => error (msg ^ Position.here pos); |
77 |
87 |
78 val read_file = read_file_node ""; |
88 val read_file = read_file_node ""; |
79 |
89 |
80 local |
90 local |