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