author | wenzelm |
Thu, 10 Jul 2008 18:02:34 +0200 | |
changeset 27529 | 6a5ccbb1bca0 |
parent 27528 | 4bbf70c35a6e |
child 27530 | df14c9cbd21d |
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 |
27529 | 16 |
val linear_undo: int -> unit |
27524 | 17 |
val undo: int -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
18 |
val crashes: exn list ref |
26643 | 19 |
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
|
20 |
val loop: unit -> unit |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
21 |
val main: unit -> unit |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
22 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
23 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
24 |
structure Isar: ISAR = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
25 |
struct |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
26 |
|
27432 | 27 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
28 |
(** individual toplevel commands **) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
29 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
30 |
(* unique identification *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
31 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
32 |
type id = string; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
33 |
val no_id : id = ""; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
34 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
35 |
fun identify tr = |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
36 |
(case Toplevel.get_id tr of |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
37 |
SOME id => (id, tr) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
38 |
| NONE => |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
39 |
let val id = "isabelle:" ^ serial_string () |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
40 |
in (id, Toplevel.put_id id tr) end); |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
41 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
42 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
43 |
(* command category *) |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
44 |
|
27524 | 45 |
datatype category = Empty | Theory | Proof | Diag | Control; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
46 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
47 |
fun category_of tr = |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
48 |
let val name = Toplevel.name_of tr in |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
49 |
if name = "" then Empty |
27524 | 50 |
else if OuterKeyword.is_theory name then Theory |
51 |
else if OuterKeyword.is_proof name then Proof |
|
52 |
else if OuterKeyword.is_diag name then Diag |
|
53 |
else Control |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
54 |
end; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
55 |
|
27524 | 56 |
val is_theory = fn Theory => true | _ => false; |
57 |
val is_proper = fn Theory => true | Proof => true | _ => false; |
|
58 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
59 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
60 |
(* datatype command *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
61 |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
62 |
datatype status = |
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
63 |
Initial | |
27518 | 64 |
Result of Toplevel.state * (exn * string) option; |
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
65 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
66 |
datatype command = Command of |
27501 | 67 |
{category: category, |
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
68 |
transition: Toplevel.transition, |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
69 |
status: status}; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
70 |
|
27501 | 71 |
fun make_command (category, transition, status) = |
72 |
Command {category = category, transition = transition, status = status}; |
|
27438
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
73 |
|
9b2427cc234e
command: always keep transition, not just as initial status;
wenzelm
parents:
27432
diff
changeset
|
74 |
val empty_command = |
27518 | 75 |
make_command (Empty, Toplevel.empty, Result (Toplevel.toplevel, NONE)); |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
76 |
|
27501 | 77 |
fun map_command f (Command {category, transition, status}) = |
78 |
make_command (f (category, transition, status)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
79 |
|
27501 | 80 |
fun map_status f = map_command (fn (category, transition, status) => |
81 |
(category, transition, f status)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
82 |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
83 |
|
27501 | 84 |
(* global collection of identified commands *) |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
85 |
|
27518 | 86 |
fun err_dup id = sys_error ("Duplicate command " ^ quote id); |
87 |
fun err_undef id = sys_error ("Unknown command " ^ quote id); |
|
88 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
89 |
local |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
90 |
|
27501 | 91 |
val empty_commands = Graph.empty: command Graph.T; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
92 |
val global_commands = ref empty_commands; |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
93 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
94 |
in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
95 |
|
27501 | 96 |
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f) |
27518 | 97 |
handle Graph.DUP id => err_dup id | Graph.UNDEF id => err_undef id; |
27501 | 98 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
99 |
fun init_commands () = change_commands (K empty_commands); |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
100 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
101 |
fun the_command id = |
27524 | 102 |
let val Command cmd = |
103 |
if id = no_id then empty_command |
|
104 |
else (Graph.get_node (! global_commands) id handle Graph.UNDEF _ => err_undef id) |
|
105 |
in cmd end; |
|
27518 | 106 |
|
107 |
fun prev_command id = |
|
108 |
if id = no_id then NONE |
|
109 |
else |
|
110 |
(case Graph.imm_preds (! global_commands) id handle Graph.UNDEF _ => err_undef id of |
|
111 |
[] => NONE |
|
112 |
| [prev] => SOME prev |
|
113 |
| _ => sys_error ("Non-linear command dependency " ^ quote id)); |
|
27501 | 114 |
|
115 |
end; |
|
116 |
||
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
117 |
|
27518 | 118 |
fun the_result id = |
27524 | 119 |
(case the_command id of |
120 |
{status = Result res, ...} => res |
|
121 |
| {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition)); |
|
122 |
||
123 |
val the_state = #1 o the_result; |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
124 |
|
27501 | 125 |
fun new_command prev (id, cmd) = |
126 |
change_commands (Graph.new_node (id, cmd) #> prev <> no_id ? Graph.add_edge (prev, id)); |
|
127 |
||
128 |
fun dispose_command id = change_commands (Graph.del_nodes [id]); |
|
129 |
||
130 |
fun change_command_status id f = change_commands (Graph.map_node id (map_status f)); |
|
131 |
||
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
132 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
133 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
134 |
(** TTY interaction **) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
135 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
136 |
(* global point *) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
137 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
138 |
local val global_point = ref no_id in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
139 |
|
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
140 |
fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f); |
27524 | 141 |
fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point); |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
142 |
|
27501 | 143 |
end; |
144 |
||
27524 | 145 |
fun set_point id = change_point (K id); |
146 |
||
147 |
fun point_result () = NAMED_CRITICAL "Isar" (fn () => |
|
148 |
let val id = point () in (id, the_result id) end); |
|
27501 | 149 |
|
27518 | 150 |
fun state () = #1 (#2 (point_result ())); |
151 |
fun exn () = #2 (#2 (point_result ())); |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
152 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
153 |
fun context () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
154 |
Toplevel.context_of (state ()) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
155 |
handle Toplevel.UNDEF => error "Unknown context"; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
156 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
157 |
fun goal () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
158 |
#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
|
159 |
handle Toplevel.UNDEF => error "No goal present"; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
160 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
161 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
162 |
(* interactive state transformations --- NOT THREAD-SAFE! *) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
163 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
164 |
nonfix >> >>>; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
165 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
166 |
fun >> raw_tr = |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
167 |
let |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
168 |
val (id, tr) = identify raw_tr; |
27518 | 169 |
val (prev, (prev_state, _)) = point_result (); |
27524 | 170 |
val category = category_of tr; |
171 |
val _ = new_command prev (id, make_command (category, tr, Initial)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
172 |
in |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
173 |
(case Toplevel.transition true tr prev_state of |
27501 | 174 |
NONE => (dispose_command id; false) |
27527 | 175 |
| SOME (result as (_, err)) => |
176 |
(change_command_status id (K (Result result)); |
|
177 |
Option.map (Toplevel.error_msg tr) err; |
|
178 |
if is_some err orelse category = Control then dispose_command id |
|
27524 | 179 |
else set_point id; |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
180 |
true)) |
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
181 |
end; |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
182 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
183 |
fun >>> [] = () |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
184 |
| >>> (tr :: trs) = if >> tr then >>> trs else (); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
185 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
186 |
|
27524 | 187 |
(* old-style navigation *) |
188 |
||
189 |
local |
|
190 |
||
191 |
fun err_undo () = error "Undo history exhausted"; |
|
192 |
||
193 |
fun get_prev id = the_default no_id (prev_command id); |
|
194 |
||
195 |
fun find_command pred id = |
|
196 |
(case #category (the_command id) of |
|
197 |
Empty => err_undo () |
|
198 |
| category => if pred category then id else find_command pred (get_prev id)); |
|
199 |
||
27529 | 200 |
fun undo_command id = |
201 |
let val {category, transition, ...} = the_command id in |
|
27524 | 202 |
(case Toplevel.init_of transition of |
27529 | 203 |
SOME name => get_prev id before ThyInfo.kill_thy name |
204 |
| NONE => get_prev id) |
|
27524 | 205 |
end; |
206 |
||
27529 | 207 |
fun undo_linear id = undo_command (find_command is_proper id); |
208 |
fun undo_nested id = undo_command |
|
209 |
(find_command (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id); |
|
210 |
||
27524 | 211 |
in |
212 |
||
27529 | 213 |
fun linear_undo n = change_point (funpow n undo_linear); |
214 |
fun undo n = change_point (funpow n undo_nested); |
|
27524 | 215 |
|
216 |
end; |
|
217 |
||
218 |
||
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
219 |
(* toplevel loop *) |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
220 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
221 |
val crashes = ref ([]: exn list); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
222 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
223 |
local |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
224 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
225 |
fun raw_loop secure src = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
226 |
let |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
227 |
fun check_secure () = |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
228 |
(if secure then warning "Secure loop -- cannot exit to ML" else (); secure); |
27524 | 229 |
val prev = point (); |
230 |
val prev_name = Toplevel.name_of (#transition (the_command prev)); |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
231 |
val prompt_markup = |
27524 | 232 |
prev <> no_id ? Markup.markup |
233 |
(Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt); |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
234 |
in |
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
235 |
(case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
236 |
NONE => if secure then quit () else () |
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
237 |
| 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
|
238 |
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
|
239 |
(CRITICAL (fn () => change crashes (cons crash)); |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
240 |
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
|
241 |
raw_loop secure src) |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
242 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
243 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
244 |
in |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
245 |
|
27428
f92d47cdc0de
explicit identification of toplevel commands, with status etc.;
wenzelm
parents:
26643
diff
changeset
|
246 |
fun toplevel_loop {init, welcome, sync, secure} = |
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
247 |
(Context.set_thread_data NONE; |
27528 | 248 |
if init then (set_point no_id; init_commands ()) else (); |
26643 | 249 |
if welcome then writeln (Session.welcome ()) else (); |
26606
379596d12f25
replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents:
26605
diff
changeset
|
250 |
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
|
251 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
252 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
253 |
|
26643 | 254 |
fun loop () = |
255 |
toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; |
|
27528 | 256 |
|
26643 | 257 |
fun main () = |
258 |
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
|
259 |
|
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
260 |
end; |
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
261 |