author | wenzelm |
Thu, 10 Apr 2008 13:24:22 +0200 | |
changeset 26605 | 24e60e823d22 |
child 26606 | 379596d12f25 |
permissions | -rw-r--r-- |
wenzelm@26605 | 1 |
(* Title: Pure/Isar/isar.ML |
wenzelm@26605 | 2 |
ID: $Id$ |
wenzelm@26605 | 3 |
Author: Makarius |
wenzelm@26605 | 4 |
|
wenzelm@26605 | 5 |
The global Isabelle/Isar state and main read-eval-print loop. |
wenzelm@26605 | 6 |
*) |
wenzelm@26605 | 7 |
|
wenzelm@26605 | 8 |
signature ISAR = |
wenzelm@26605 | 9 |
sig |
wenzelm@26605 | 10 |
val state: unit -> Toplevel.state |
wenzelm@26605 | 11 |
val exn: unit -> (exn * string) option |
wenzelm@26605 | 12 |
val context: unit -> Proof.context |
wenzelm@26605 | 13 |
val goal: unit -> thm |
wenzelm@26605 | 14 |
val >> : Toplevel.transition -> bool |
wenzelm@26605 | 15 |
val >>> : Toplevel.transition list -> unit |
wenzelm@26605 | 16 |
val init: unit -> unit |
wenzelm@26605 | 17 |
val crashes: exn list ref |
wenzelm@26605 | 18 |
val main: unit -> unit |
wenzelm@26605 | 19 |
val loop: unit -> unit |
wenzelm@26605 | 20 |
val sync_main: unit -> unit |
wenzelm@26605 | 21 |
val sync_loop: unit -> unit |
wenzelm@26605 | 22 |
val secure_main: unit -> unit |
wenzelm@26605 | 23 |
end; |
wenzelm@26605 | 24 |
|
wenzelm@26605 | 25 |
structure Isar: ISAR = |
wenzelm@26605 | 26 |
struct |
wenzelm@26605 | 27 |
|
wenzelm@26605 | 28 |
(* the global state *) |
wenzelm@26605 | 29 |
|
wenzelm@26605 | 30 |
val global_state = ref (Toplevel.toplevel, NONE: (exn * string) option); |
wenzelm@26605 | 31 |
|
wenzelm@26605 | 32 |
fun state () = #1 (! global_state); |
wenzelm@26605 | 33 |
fun exn () = #2 (! global_state); |
wenzelm@26605 | 34 |
|
wenzelm@26605 | 35 |
fun context () = |
wenzelm@26605 | 36 |
Toplevel.context_of (state ()) |
wenzelm@26605 | 37 |
handle Toplevel.UNDEF => error "Unknown context"; |
wenzelm@26605 | 38 |
|
wenzelm@26605 | 39 |
fun goal () = |
wenzelm@26605 | 40 |
#2 (#2 (Proof.get_goal (Toplevel.proof_of (state ())))) |
wenzelm@26605 | 41 |
handle Toplevel.UNDEF => error "No goal present"; |
wenzelm@26605 | 42 |
|
wenzelm@26605 | 43 |
|
wenzelm@26605 | 44 |
(* interactive state transformations --- NOT THREAD-SAFE! *) |
wenzelm@26605 | 45 |
|
wenzelm@26605 | 46 |
nonfix >> >>>; |
wenzelm@26605 | 47 |
|
wenzelm@26605 | 48 |
fun >> tr = |
wenzelm@26605 | 49 |
(case Toplevel.transition true tr (state ()) of |
wenzelm@26605 | 50 |
NONE => false |
wenzelm@26605 | 51 |
| SOME (state', exn_info) => |
wenzelm@26605 | 52 |
(global_state := (state', exn_info); |
wenzelm@26605 | 53 |
(case exn_info of |
wenzelm@26605 | 54 |
NONE => () |
wenzelm@26605 | 55 |
| SOME err => Toplevel.error_msg tr err); |
wenzelm@26605 | 56 |
true)); |
wenzelm@26605 | 57 |
|
wenzelm@26605 | 58 |
fun >>> [] = () |
wenzelm@26605 | 59 |
| >>> (tr :: trs) = if >> tr then >>> trs else (); |
wenzelm@26605 | 60 |
|
wenzelm@26605 | 61 |
fun init () = (>> (Toplevel.init_empty (K true) (K ()) Toplevel.empty); ()); |
wenzelm@26605 | 62 |
|
wenzelm@26605 | 63 |
|
wenzelm@26605 | 64 |
(* main loop *) |
wenzelm@26605 | 65 |
|
wenzelm@26605 | 66 |
val crashes = ref ([]: exn list); |
wenzelm@26605 | 67 |
|
wenzelm@26605 | 68 |
local |
wenzelm@26605 | 69 |
|
wenzelm@26605 | 70 |
(*Spurious interrupts ahead! Race condition?*) |
wenzelm@26605 | 71 |
fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE; |
wenzelm@26605 | 72 |
|
wenzelm@26605 | 73 |
fun raw_loop secure src = |
wenzelm@26605 | 74 |
let |
wenzelm@26605 | 75 |
fun check_secure () = |
wenzelm@26605 | 76 |
(if secure then warning "Secure loop -- cannot exit to ML" else (); secure); |
wenzelm@26605 | 77 |
in |
wenzelm@26605 | 78 |
(case get_interrupt (Source.set_prompt Source.default_prompt src) of |
wenzelm@26605 | 79 |
NONE => (writeln "\nInterrupt."; raw_loop secure src) |
wenzelm@26605 | 80 |
| SOME NONE => if secure then quit () else () |
wenzelm@26605 | 81 |
| SOME (SOME (tr, src')) => if >> tr orelse check_secure () then raw_loop secure src' else ()) |
wenzelm@26605 | 82 |
handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash => |
wenzelm@26605 | 83 |
(CRITICAL (fn () => change crashes (cons crash)); |
wenzelm@26605 | 84 |
warning "Recovering after Isar toplevel crash -- see also Isar.crashes"); |
wenzelm@26605 | 85 |
raw_loop secure src) |
wenzelm@26605 | 86 |
end; |
wenzelm@26605 | 87 |
|
wenzelm@26605 | 88 |
in |
wenzelm@26605 | 89 |
|
wenzelm@26605 | 90 |
fun gen_loop secure do_terminate = |
wenzelm@26605 | 91 |
(Context.set_thread_data NONE; |
wenzelm@26605 | 92 |
uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar do_terminate)) ()); |
wenzelm@26605 | 93 |
|
wenzelm@26605 | 94 |
fun gen_main secure do_terminate = |
wenzelm@26605 | 95 |
(init (); |
wenzelm@26605 | 96 |
writeln (Session.welcome ()); |
wenzelm@26605 | 97 |
gen_loop secure do_terminate); |
wenzelm@26605 | 98 |
|
wenzelm@26605 | 99 |
end; |
wenzelm@26605 | 100 |
|
wenzelm@26605 | 101 |
fun main () = gen_main (Secure.is_secure ()) false; |
wenzelm@26605 | 102 |
fun loop () = gen_loop (Secure.is_secure ()) false; |
wenzelm@26605 | 103 |
fun sync_main () = gen_main (Secure.is_secure ()) true; |
wenzelm@26605 | 104 |
fun sync_loop () = gen_loop (Secure.is_secure ()) true; |
wenzelm@26605 | 105 |
fun secure_main () = (init (); gen_loop true true); |
wenzelm@26605 | 106 |
|
wenzelm@26605 | 107 |
end; |
wenzelm@26605 | 108 |