blob: 5d4601983d16e1715dc081345a297872d284519a (
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
(*
Isabelle configuration for Proof General.
Author: David Aspinall <da@dcs.ed.ac.uk>
Contact: Isabelle maintainer <isabelle@dcs.ed.ac.uk>
$Id$
*)
signature PROOFGENERAL =
sig
val kill_goal : unit -> unit
val help : unit -> unit
val show_context : unit -> unit
val retract_file : string -> unit
end
structure ProofGeneral =
struct
(* Some top-level commands for Proof General.
These easily could be customized to do different things.
*)
fun kill_goal () = Goal "PROP no_goal_supplied";
fun help () = print version;
fun show_context () = the_context();
(* Function used internally by Proof General to track
dependencies between theory and ML files. *)
fun retract_file thy =
let fun file_msg x = if (x <> "") then
writeln ("Proof General, you can unlock the file "
^ (quote x))
else ()
fun show_msgs thy =
let val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy
in (file_msg thy_file; file_msg ml_file) end
fun already_loaded thy =
let val t = get_thyinfo thy
in if is_none t then false
else let val {thy_time, ml_time, ...} = the t
in is_some thy_time andalso is_some ml_time end
end
fun children_loaded thy =
let val children = children_of thy
val present = filter (is_some o get_thyinfo) children;
in filter already_loaded present end
in
if already_loaded thy then
(show_msgs thy; map retract_file (children_loaded thy); ())
else ()
end;
end;
(* add markup to proof state output *)
val proof_state_special_prefix="\248";
val proof_state_special_suffix="\249";
val goal_start_special="\253";
current_goals_markers:=(proof_state_special_prefix,
proof_state_special_suffix,
goal_start_special);
(* Turn on verbose update output, Proof General likes to parse it. *)
update_verbose:=true;
(* Let Proof General see the theories loaded in the logic image. *)
update();
|
