blob: b14c01ca886554fb014fbc546248d10489e77017 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(* ========================================================================= *)
(* 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 "<prompt>" ^
(!pg_prompt_info()) ^
"</prompt>"
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
"<error>" ^ x ^ "</error>"
else x)
| _ -> Format.print_string (Printexc.to_string e);;
#install_printer print_exn;;
*)
|
