(* ========================================================================= *)
(* HOL Light tweaks for Proof General. *)
(* *)
(* Mark Adams, David Aspinall. *)
(* LFCS, School of Informatics, University of Edinburgh *)
(* *)
(* (c) Copyright University of Edinburgh and authors, 2012. *)
(* *)
(* This file adjust the OCaml prompt to help Proof General synchronization. *)
(* It is loaded before HOL Light. *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Proof General mode, providing extra annotations in output *)
(* ------------------------------------------------------------------------- *)
let pg_mode = ref (true : bool);;
let pg_mode_on () = (pg_mode := true);;
let pg_mode_off () = (pg_mode := false);;
let pg_prompt_info = ref (fun () -> "");;
(* ------------------------------------------------------------------------- *)
(* Adjust the OCaml prompt to carry information for Proof General *)
(* ------------------------------------------------------------------------- *)
let original_prompt_fn = !Toploop.read_interactive_input in
(Toploop.read_interactive_input :=
fun prompt buffer len ->
let prompt' =
if (!pg_mode)
then "" ^
(!pg_prompt_info()) ^
""
else prompt in
original_prompt_fn prompt' buffer len);;
(* ------------------------------------------------------------------------- *)
(* Adjust error printing to markup error messages *)
(* ------------------------------------------------------------------------- *)
(* Doesn't really work, as many errors are from OCaml top level and
not printed in this way.
let print_exn e =
match e with
Failure x -> Format.print_string
(if (!pg_mode) then
"" ^ x ^ ""
else x)
| _ -> Format.print_string (Printexc.to_string e);;
#install_printer print_exn;;
*)