diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 4 | ||||
| -rw-r--r-- | ide/ideutils.ml | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 7cbab56d44..cfc0e09a0c 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -217,7 +217,7 @@ let evars () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -227,7 +227,7 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in match all_goals with | [] -> None | g :: _ -> diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 83e5da9509..0977a18906 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -372,8 +372,7 @@ let read_file name buf = let io_read_all chan = Buffer.clear read_buffer; let read_once () = - (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *) - let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in + let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in Buffer.add_subbytes read_buffer read_string 0 len in begin |