blob: a6342872b423c39678166176eff7eaf7cbb3d935 (
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
|
(* ========================================================================= *)
(* 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 message *)
(* ------------------------------------------------------------------------- *)
(* FIXME: rebinding failwith has an odd effect on top level, triggering
new errors which were perhaps previously caught?*)
(*
let plain_failwith = failwith
let failwith s = if (!pg_mode)
then plain_failwith ("<error>" ^ s ^ "</error>")
else plain_failwith s;;
*)
|