wenzelm@30176
|
1 |
(* Title: Pure/System/isar.ML
|
wenzelm@26605
|
2 |
Author: Makarius
|
wenzelm@26605
|
3 |
|
wenzelm@37306
|
4 |
Global state of the raw Isar read-eval-print loop.
|
wenzelm@26605
|
5 |
*)
|
wenzelm@26605
|
6 |
|
wenzelm@26605
|
7 |
signature ISAR =
|
wenzelm@26605
|
8 |
sig
|
wenzelm@29348
|
9 |
val init: unit -> unit
|
wenzelm@29348
|
10 |
val exn: unit -> (exn * string) option
|
wenzelm@26605
|
11 |
val state: unit -> Toplevel.state
|
wenzelm@33289
|
12 |
val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
|
wenzelm@27533
|
13 |
val print: unit -> unit
|
wenzelm@26605
|
14 |
val >> : Toplevel.transition -> bool
|
wenzelm@26605
|
15 |
val >>> : Toplevel.transition list -> unit
|
wenzelm@27529
|
16 |
val linear_undo: int -> unit
|
wenzelm@27524
|
17 |
val undo: int -> unit
|
wenzelm@27530
|
18 |
val kill: unit -> unit
|
wenzelm@27530
|
19 |
val kill_proof: unit -> unit
|
wenzelm@44563
|
20 |
val crashes: exn list Synchronized.var
|
wenzelm@38551
|
21 |
val toplevel_loop: TextIO.instream ->
|
wenzelm@38551
|
22 |
{init: bool, welcome: bool, sync: bool, secure: bool} -> unit
|
wenzelm@26606
|
23 |
val loop: unit -> unit
|
wenzelm@26605
|
24 |
val main: unit -> unit
|
wenzelm@26605
|
25 |
end;
|
wenzelm@26605
|
26 |
|
wenzelm@26605
|
27 |
structure Isar: ISAR =
|
wenzelm@26605
|
28 |
struct
|
wenzelm@26605
|
29 |
|
wenzelm@27432
|
30 |
|
wenzelm@29348
|
31 |
(** TTY model -- SINGLE-THREADED! **)
|
wenzelm@29348
|
32 |
|
wenzelm@29348
|
33 |
(* the global state *)
|
wenzelm@29348
|
34 |
|
wenzelm@29348
|
35 |
type history = (Toplevel.state * Toplevel.transition) list;
|
wenzelm@29348
|
36 |
(*previous state, state transition -- regular commands only*)
|
wenzelm@29348
|
37 |
|
wenzelm@29348
|
38 |
local
|
wenzelm@32738
|
39 |
val global_history = Unsynchronized.ref ([]: history);
|
wenzelm@32738
|
40 |
val global_state = Unsynchronized.ref Toplevel.toplevel;
|
wenzelm@32738
|
41 |
val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
|
wenzelm@29348
|
42 |
in
|
wenzelm@29348
|
43 |
|
wenzelm@29348
|
44 |
fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
|
wenzelm@29348
|
45 |
let
|
wenzelm@29348
|
46 |
fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
|
wenzelm@29348
|
47 |
| edit n (st, hist) = edit (n - 1) (f st hist);
|
wenzelm@29348
|
48 |
in edit count (! global_state, ! global_history) end);
|
wenzelm@29348
|
49 |
|
wenzelm@33234
|
50 |
fun state () = ! global_state;
|
wenzelm@29348
|
51 |
|
wenzelm@33234
|
52 |
fun exn () = ! global_exn;
|
wenzelm@33234
|
53 |
fun set_exn exn = global_exn := exn;
|
wenzelm@29348
|
54 |
|
wenzelm@29348
|
55 |
end;
|
wenzelm@29348
|
56 |
|
wenzelm@29348
|
57 |
|
wenzelm@29348
|
58 |
fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
|
wenzelm@29348
|
59 |
|
wenzelm@33289
|
60 |
fun goal () = Proof.goal (Toplevel.proof_of (state ()))
|
wenzelm@29348
|
61 |
handle Toplevel.UNDEF => error "No goal present";
|
wenzelm@29348
|
62 |
|
wenzelm@29348
|
63 |
fun print () = Toplevel.print_state false (state ());
|
wenzelm@29348
|
64 |
|
wenzelm@29348
|
65 |
|
wenzelm@29348
|
66 |
(* history navigation *)
|
wenzelm@29348
|
67 |
|
wenzelm@29348
|
68 |
local
|
wenzelm@29348
|
69 |
|
wenzelm@29348
|
70 |
fun find_and_undo _ [] = error "Undo history exhausted"
|
wenzelm@29348
|
71 |
| find_and_undo which ((prev, tr) :: hist) =
|
wenzelm@38384
|
72 |
if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
|
wenzelm@29348
|
73 |
|
wenzelm@29348
|
74 |
in
|
wenzelm@29348
|
75 |
|
wenzelm@29348
|
76 |
fun linear_undo n = edit_history n (K (find_and_undo (K true)));
|
wenzelm@29348
|
77 |
|
wenzelm@29348
|
78 |
fun undo n = edit_history n (fn st => fn hist =>
|
wenzelm@36950
|
79 |
find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
|
wenzelm@29348
|
80 |
|
wenzelm@29348
|
81 |
fun kill () = edit_history 1 (fn st => fn hist =>
|
wenzelm@29348
|
82 |
find_and_undo
|
wenzelm@36950
|
83 |
(if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
|
wenzelm@29348
|
84 |
|
wenzelm@29348
|
85 |
fun kill_proof () = edit_history 1 (fn st => fn hist =>
|
wenzelm@36950
|
86 |
if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
|
wenzelm@29348
|
87 |
else raise Toplevel.UNDEF);
|
wenzelm@29348
|
88 |
|
wenzelm@29348
|
89 |
end;
|
wenzelm@29348
|
90 |
|
wenzelm@29348
|
91 |
|
wenzelm@29348
|
92 |
(* interactive state transformations *)
|
wenzelm@29348
|
93 |
|
wenzelm@29348
|
94 |
fun op >> tr =
|
wenzelm@29348
|
95 |
(case Toplevel.transition true tr (state ()) of
|
wenzelm@29348
|
96 |
NONE => false
|
wenzelm@39202
|
97 |
| SOME (_, SOME exn_info) =>
|
wenzelm@39202
|
98 |
(set_exn (SOME exn_info);
|
wenzelm@39202
|
99 |
Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
|
wenzelm@39202
|
100 |
true)
|
wenzelm@29348
|
101 |
| SOME (st', NONE) =>
|
wenzelm@29348
|
102 |
let
|
wenzelm@29348
|
103 |
val name = Toplevel.name_of tr;
|
wenzelm@36950
|
104 |
val _ = if Keyword.is_theory_begin name then init () else ();
|
wenzelm@29348
|
105 |
val _ =
|
wenzelm@36950
|
106 |
if Keyword.is_regular name
|
wenzelm@29348
|
107 |
then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
|
wenzelm@29348
|
108 |
in true end);
|
wenzelm@29348
|
109 |
|
wenzelm@29348
|
110 |
fun op >>> [] = ()
|
wenzelm@29348
|
111 |
| op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
|
wenzelm@29348
|
112 |
|
wenzelm@29348
|
113 |
|
wenzelm@39511
|
114 |
(* toplevel loop -- uninterruptible *)
|
wenzelm@29348
|
115 |
|
wenzelm@44563
|
116 |
val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
|
wenzelm@29348
|
117 |
|
wenzelm@29348
|
118 |
local
|
wenzelm@29348
|
119 |
|
wenzelm@29348
|
120 |
fun raw_loop secure src =
|
wenzelm@29348
|
121 |
let
|
wenzelm@29348
|
122 |
fun check_secure () =
|
wenzelm@29348
|
123 |
(if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
|
wenzelm@29348
|
124 |
in
|
wenzelm@29348
|
125 |
(case Source.get_single (Source.set_prompt Source.default_prompt src) of
|
wenzelm@29348
|
126 |
NONE => if secure then quit () else ()
|
wenzelm@29348
|
127 |
| SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
|
wenzelm@29374
|
128 |
handle exn =>
|
wenzelm@31478
|
129 |
(Output.error_msg (ML_Compiler.exn_message exn)
|
wenzelm@29374
|
130 |
handle crash =>
|
wenzelm@44563
|
131 |
(Synchronized.change crashes (cons crash);
|
wenzelm@29374
|
132 |
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
|
wenzelm@38570
|
133 |
raw_loop secure src)
|
wenzelm@29348
|
134 |
end;
|
wenzelm@29348
|
135 |
|
wenzelm@29348
|
136 |
in
|
wenzelm@29348
|
137 |
|
wenzelm@38551
|
138 |
fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
|
wenzelm@29348
|
139 |
(Context.set_thread_data NONE;
|
wenzelm@32486
|
140 |
if do_init then init () else ();
|
wenzelm@29348
|
141 |
if welcome then writeln (Session.welcome ()) else ();
|
wenzelm@38551
|
142 |
uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
|
wenzelm@29348
|
143 |
|
wenzelm@29348
|
144 |
end;
|
wenzelm@29348
|
145 |
|
wenzelm@29348
|
146 |
fun loop () =
|
wenzelm@38551
|
147 |
toplevel_loop TextIO.stdIn
|
wenzelm@38551
|
148 |
{init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
|
wenzelm@29348
|
149 |
|
wenzelm@29348
|
150 |
fun main () =
|
wenzelm@38551
|
151 |
toplevel_loop TextIO.stdIn
|
wenzelm@38551
|
152 |
{init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
|
wenzelm@29348
|
153 |
|
wenzelm@29348
|
154 |
|
wenzelm@29348
|
155 |
|
wenzelm@30174
|
156 |
(** command syntax **)
|
wenzelm@28300
|
157 |
|
wenzelm@28300
|
158 |
local
|
wenzelm@28300
|
159 |
|
wenzelm@28300
|
160 |
val op >> = Scan.>>;
|
wenzelm@28300
|
161 |
|
wenzelm@28300
|
162 |
in
|
wenzelm@28300
|
163 |
|
wenzelm@30174
|
164 |
(* global history *)
|
wenzelm@30174
|
165 |
|
wenzelm@30174
|
166 |
val _ =
|
wenzelm@36953
|
167 |
Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
|
wenzelm@30174
|
168 |
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
|
wenzelm@30174
|
169 |
|
wenzelm@30174
|
170 |
val _ =
|
wenzelm@36953
|
171 |
Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
|
wenzelm@36950
|
172 |
(Scan.optional Parse.nat 1 >>
|
wenzelm@30174
|
173 |
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
|
wenzelm@30174
|
174 |
|
wenzelm@30174
|
175 |
val _ =
|
wenzelm@36953
|
176 |
Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
|
wenzelm@36950
|
177 |
(Scan.optional Parse.nat 1 >>
|
wenzelm@30174
|
178 |
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
|
wenzelm@30174
|
179 |
|
wenzelm@30174
|
180 |
val _ =
|
wenzelm@36953
|
181 |
Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
|
wenzelm@36950
|
182 |
Keyword.control
|
wenzelm@36950
|
183 |
(Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
|
wenzelm@30174
|
184 |
Toplevel.keep (fn state =>
|
wenzelm@30174
|
185 |
if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
|
wenzelm@30174
|
186 |
|
wenzelm@30174
|
187 |
val _ =
|
wenzelm@36953
|
188 |
Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
|
wenzelm@36950
|
189 |
Keyword.control
|
wenzelm@36950
|
190 |
(Parse.name >>
|
wenzelm@30174
|
191 |
(fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
|
wenzelm@30174
|
192 |
| txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
|
wenzelm@30174
|
193 |
|
wenzelm@30174
|
194 |
val _ =
|
wenzelm@36953
|
195 |
Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
|
wenzelm@30174
|
196 |
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
|
wenzelm@30174
|
197 |
|
wenzelm@26605
|
198 |
end;
|
wenzelm@26605
|
199 |
|
wenzelm@28300
|
200 |
end;
|