src/Pure/PIDE/command.ML
changeset 72945 756b9cb8a176
parent 72841 fd8d82c4433b
child 72950 ac6457a70db5
equal deleted inserted replaced
72944:50c48773b954 72945:756b9cb8a176
    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);