equal
deleted
inserted
replaced
17 val goal: unit -> thm list * thm |
17 val goal: unit -> thm list * thm |
18 val main: unit -> unit |
18 val main: unit -> unit |
19 val loop: unit -> unit |
19 val loop: unit -> unit |
20 val sync_main: unit -> unit |
20 val sync_main: unit -> unit |
21 val sync_loop: unit -> unit |
21 val sync_loop: unit -> unit |
|
22 val secure_main: unit -> unit |
22 val toplevel: (unit -> 'a) -> 'a |
23 val toplevel: (unit -> 'a) -> 'a |
23 end; |
24 end; |
24 end; |
25 end; |
25 |
26 |
26 signature OUTER_SYNTAX = |
27 signature OUTER_SYNTAX = |
317 |
318 |
318 (** the read-eval-print loop **) |
319 (** the read-eval-print loop **) |
319 |
320 |
320 (* main loop *) |
321 (* main loop *) |
321 |
322 |
322 fun gen_loop term = |
323 fun gen_loop secure terminated = |
323 (CRITICAL (fn () => ML_Context.set_context NONE); |
324 (CRITICAL (fn () => ML_Context.set_context NONE); |
324 Toplevel.loop (isar term)); |
325 Toplevel.loop secure (isar terminated)); |
325 |
326 |
326 fun gen_main term = |
327 fun gen_main secure terminated = |
327 (Toplevel.init_state (); |
328 (Toplevel.init_state (); |
328 writeln (Session.welcome ()); |
329 writeln (Session.welcome ()); |
329 gen_loop term); |
330 gen_loop secure terminated); |
330 |
331 |
331 structure Isar = |
332 structure Isar = |
332 struct |
333 struct |
333 val state = Toplevel.get_state; |
334 val state = Toplevel.get_state; |
334 val exn = Toplevel.exn; |
335 val exn = Toplevel.exn; |
339 |
340 |
340 fun goal () = |
341 fun goal () = |
341 #2 (Proof.get_goal (Toplevel.proof_of (state ()))) |
342 #2 (Proof.get_goal (Toplevel.proof_of (state ()))) |
342 handle Toplevel.UNDEF => error "No goal present"; |
343 handle Toplevel.UNDEF => error "No goal present"; |
343 |
344 |
344 fun main () = gen_main false; |
345 fun main () = gen_main (Secure.is_secure ()) false; |
345 fun loop () = gen_loop false; |
346 fun loop () = gen_loop (Secure.is_secure ()) false; |
346 fun sync_main () = gen_main true; |
347 fun sync_main () = gen_main (Secure.is_secure ()) true; |
347 fun sync_loop () = gen_loop true; |
348 fun sync_loop () = gen_loop (Secure.is_secure ()) true; |
|
349 fun secure_main () = gen_main true false; |
348 val toplevel = Toplevel.program; |
350 val toplevel = Toplevel.program; |
349 end; |
351 end; |
350 |
352 |
351 end; |
353 end; |
352 |
354 |