author  wenzelm 
Tue, 11 Mar 2008 22:31:09 +0100  
changeset 26256  3e7939e978c6 
parent 26081  fbdb1161b4b0 
child 26257  707969e76f5c 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
The Isabelle/Isar toplevel. 

6 
*) 

7 

8 
signature TOPLEVEL = 

9 
sig 

19063  10 
exception UNDEF 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

11 
type generic_theory 
18589  12 
type node 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

13 
val theory_node: node > generic_theory option 
18589  14 
val proof_node: node > ProofHistory.T option 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

15 
val cases_node: (generic_theory > 'a) > (Proof.state > 'a) > node > 'a 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

16 
val presentation_context: node option > xstring option > Proof.context 
5828  17 
type state 
7732  18 
val is_toplevel: state > bool 
18589  19 
val is_theory: state > bool 
20 
val is_proof: state > bool 

17076  21 
val level: state > int 
6689  22 
val node_history_of: state > node History.T 
5828  23 
val node_of: state > node 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

24 
val node_case: (generic_theory > 'a) > (Proof.state > 'a) > state > 'a 
21506  25 
val context_of: state > Proof.context 
22089  26 
val generic_theory_of: state > generic_theory 
5828  27 
val theory_of: state > theory 
28 
val proof_of: state > Proof.state 

18589  29 
val proof_position_of: state > int 
21007  30 
val enter_proof_body: state > Proof.state 
16815  31 
val print_state_context: state > unit 
32 
val print_state: bool > state > unit 

16682  33 
val quiet: bool ref 
34 
val debug: bool ref 

17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

35 
val interact: bool ref 
16682  36 
val timing: bool ref 
37 
val profiling: int ref 

16815  38 
val skip_proofs: bool ref 
25584  39 
val crashes: exn list ref 
5828  40 
exception TERMINATE 
5990  41 
exception RESTART 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

42 
exception CONTEXT of Proof.context * exn 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

43 
exception TOPLEVEL_ERROR 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

44 
val exn_message: exn > string 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

45 
val program: (unit > 'a) > 'a 
16682  46 
type transition 
6689  47 
val undo_limit: bool > int option 
5828  48 
val empty: transition 
14923  49 
val name_of: transition > string 
50 
val source_of: transition > OuterLex.token list option 

5828  51 
val name: string > transition > transition 
52 
val position: Position.T > transition > transition 

14923  53 
val source: OuterLex.token list > transition > transition 
5828  54 
val interactive: bool > transition > transition 
55 
val print: transition > transition 

16607  56 
val print': string > transition > transition 
17363  57 
val three_buffersN: string 
58 
val print3: transition > transition 

9010  59 
val no_timing: transition > transition 
22056  60 
val init_theory: (bool > theory) > (theory > unit) > (theory > unit) > 
61 
transition > transition 

25441
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

62 
val init_empty: (state > bool) > (unit > unit) > transition > transition 
6689  63 
val exit: transition > transition 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

64 
val undo_exit: transition > transition 
6689  65 
val kill: transition > transition 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

66 
val history: (node History.T > node History.T) > transition > transition 
5828  67 
val keep: (state > unit) > transition > transition 
7612  68 
val keep': (bool > state > unit) > transition > transition 
5828  69 
val imperative: (unit > unit) > transition > transition 
70 
val theory: (theory > theory) > transition > transition 

7612  71 
val theory': (bool > theory > theory) > transition > transition 
20985  72 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  73 
val end_local_theory: transition > transition 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

74 
val local_theory: xstring option > (local_theory > local_theory) > transition > transition 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

75 
val present_local_theory: xstring option > (bool > node > unit) > transition > transition 
24453  76 
val local_theory_to_proof': xstring option > (bool > local_theory > Proof.state) > 
77 
transition > transition 

21007  78 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
79 
transition > transition 

17363  80 
val theory_to_proof: (theory > Proof.state) > transition > transition 
21007  81 
val end_proof: (bool > Proof.state > Proof.context) > transition > transition 
82 
val forget_proof: transition > transition 

21177  83 
val present_proof: (bool > node > unit) > transition > transition 
84 
val proofs': (bool > Proof.state > Proof.state Seq.seq) > transition > transition 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

85 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21177  86 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
87 
val proof: (Proof.state > Proof.state) > transition > transition 

16815  88 
val actual_proof: (ProofHistory.T > ProofHistory.T) > transition > transition 
89 
val skip_proof: (int History.T > int History.T) > transition > transition 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

90 
val skip_proof_to_theory: (int > bool) > transition > transition 
9512  91 
val unknown_theory: transition > transition 
92 
val unknown_proof: transition > transition 

93 
val unknown_context: transition > transition 

17076  94 
val present_excursion: (transition * (state > state > 'a > 'a)) list > 'a > 'a 
5828  95 
val excursion: transition list > unit 
96 
val set_state: state > unit 

97 
val get_state: unit > state 

98 
val exn: unit > (exn * string) option 

99 
val >> : transition > bool 

14985  100 
val >>> : transition list > unit 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

101 
val init_state: unit > unit 
14091  102 
type 'a isar 
25527
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

103 
val loop: bool > 'a isar > unit 
5828  104 
end; 
105 

6965  106 
structure Toplevel: TOPLEVEL = 
5828  107 
struct 
108 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

109 

5828  110 
(** toplevel state **) 
111 

19063  112 
exception UNDEF; 
113 

114 

21294  115 
(* local theory wrappers *) 
5828  116 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

117 
type generic_theory = Context.generic; (*theory or local_theory*) 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

118 

25292  119 
val loc_init = TheoryTarget.context; 
21294  120 
val loc_exit = ProofContext.theory_of o LocalTheory.exit; 
121 

25292  122 
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "" loc) thy 
21294  123 
 loc_begin NONE (Context.Proof lthy) = lthy 
25269  124 
 loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); 
21294  125 

126 
fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit 

127 
 loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore 

25292  128 
 loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => 
129 
Context.Proof (LocalTheory.reinit (LocalTheory.raw_theory (K (loc_exit lthy')) lthy)); 

21294  130 

131 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

132 
(* datatype node *) 
21294  133 

5828  134 
datatype node = 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

135 
Theory of generic_theory * Proof.context option  (*theory with presentation context*) 
21007  136 
Proof of ProofHistory.T * ((Proof.context > generic_theory) * generic_theory)  
137 
(*history of proof states, finish, original theory*) 

138 
SkipProof of int History.T * (generic_theory * generic_theory); 

18563  139 
(*history of proof depths, resulting theory, original theory*) 
5828  140 

22056  141 
val the_global_theory = fn Theory (Context.Theory thy, _) => thy  _ => raise UNDEF; 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

142 
val theory_node = fn Theory (gthy, _) => SOME gthy  _ => NONE; 
18589  143 
val proof_node = fn Proof (prf, _) => SOME prf  _ => NONE; 
144 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

145 
fun cases_node f _ (Theory (gthy, _)) = f gthy 
19063  146 
 cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf) 
21007  147 
 cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; 
19063  148 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

149 
fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

150 
 presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

151 
 presentation_context (SOME node) (SOME loc) = 
25269  152 
loc_init loc (cases_node Context.theory_of Proof.theory_of node) 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

153 
 presentation_context NONE _ = raise UNDEF; 
19063  154 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

155 

9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

156 
(* datatype state *) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

157 

22056  158 
type state_info = node History.T * ((theory > unit) * (theory > unit)); 
5828  159 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

160 
datatype state = 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

161 
Toplevel of state_info option  (*outer toplevel, leftover end state*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

162 
State of state_info; 
5828  163 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

164 
val toplevel = Toplevel NONE; 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

165 

9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

166 
fun is_toplevel (Toplevel _) = true 
7732  167 
 is_toplevel _ = false; 
168 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

169 
fun level (Toplevel _) = 0 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

170 
 level (State (node, _)) = 
17076  171 
(case History.current node of 
21310
bfcc24fc7c46
level: do not account for local theory blocks (relevant for document preparation);
wenzelm
parents:
21294
diff
changeset

172 
Theory _ => 0 
bfcc24fc7c46
level: do not account for local theory blocks (relevant for document preparation);
wenzelm
parents:
21294
diff
changeset

173 
 Proof (prf, _) => Proof.level (ProofHistory.current prf) 
bfcc24fc7c46
level: do not account for local theory blocks (relevant for document preparation);
wenzelm
parents:
21294
diff
changeset

174 
 SkipProof (h, _) => History.current h + 1); (*different notion of proof depth!*) 
17076  175 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

176 
fun str_of_state (Toplevel _) = "at top level" 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

177 
 str_of_state (State (node, _)) = 
16815  178 
(case History.current node of 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

179 
Theory (Context.Theory _, _) => "in theory mode" 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

180 
 Theory (Context.Proof _, _) => "in local theory mode" 
16815  181 
 Proof _ => "in proof mode" 
182 
 SkipProof _ => "in skipped proof mode"); 

5946
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

183 

a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

184 

5828  185 
(* top node *) 
186 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

187 
fun node_history_of (Toplevel _) = raise UNDEF 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

188 
 node_history_of (State (node, _)) = node; 
6689  189 

190 
val node_of = History.current o node_history_of; 

5828  191 

18589  192 
fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); 
193 
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); 

194 

19063  195 
fun node_case f g state = cases_node f g (node_of state); 
5828  196 

21506  197 
val context_of = node_case Context.proof_of Proof.context_of; 
22089  198 
val generic_theory_of = node_case I (Context.Proof o Proof.context_of); 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

199 
val theory_of = node_case Context.theory_of Proof.theory_of; 
18589  200 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  201 

18589  202 
fun proof_position_of state = 
203 
(case node_of state of 

204 
Proof (prf, _) => ProofHistory.position prf 

205 
 _ => raise UNDEF); 

6664  206 

21007  207 
val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward; 
5828  208 

209 

16815  210 
(* print state *) 
211 

25292  212 
val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I; 
16815  213 

23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

214 
fun print_state_context state = 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

215 
(case try node_of state of 
21506  216 
NONE => [] 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

217 
 SOME (Theory (gthy, _)) => pretty_context gthy 
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

218 
 SOME (Proof (_, (_, gthy))) => pretty_context gthy 
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

219 
 SOME (SkipProof (_, (gthy, _))) => pretty_context gthy) 
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

220 
> Pretty.chunks > Pretty.writeln; 
16815  221 

23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

222 
fun print_state prf_only state = 
23701  223 
(case try node_of state of 
224 
NONE => [] 

225 
 SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy 

226 
 SOME (Proof (prf, _)) => 

227 
Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf) 

228 
 SOME (SkipProof (h, _)) => 

229 
[Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))]) 

230 
> Pretty.markup_chunks Markup.state > Pretty.writeln; 

16815  231 

232 

15668  233 

5828  234 
(** toplevel transitions **) 
235 

16682  236 
val quiet = ref false; 
22135  237 
val debug = Output.debugging; 
17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

238 
val interact = ref false; 
16682  239 
val timing = Output.timing; 
240 
val profiling = ref 0; 

16815  241 
val skip_proofs = ref false; 
25584  242 
val crashes = ref ([]: exn list); 
16682  243 

5828  244 
exception TERMINATE; 
5990  245 
exception RESTART; 
7022  246 
exception EXCURSION_FAIL of exn * string; 
6689  247 
exception FAILURE of state * exn; 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

248 
exception TOPLEVEL_ERROR; 
5828  249 

20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

250 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

251 
(* print exceptions *) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

252 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

253 
exception CONTEXT of Proof.context * exn; 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

254 

3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

255 
fun exn_context NONE exn = exn 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

256 
 exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn); 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

257 

20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

258 
local 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

259 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

260 
fun if_context NONE _ _ = [] 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

261 
 if_context (SOME ctxt) f xs = map (f ctxt) xs; 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

262 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

263 
fun raised name [] = "exception " ^ name ^ " raised" 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

264 
 raised name [msg] = "exception " ^ name ^ " raised: " ^ msg 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

265 
 raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

266 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

267 
in 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

268 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

269 
fun exn_message e = 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

270 
let 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

271 
val detailed = ! debug; 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

272 

3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

273 
fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

274 
 exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

275 
 exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg]) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

276 
 exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = exn_msg ctxt exn ^ 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

277 
Output.escape (Markup.enclose Markup.location (Output.output ("\n" ^ loc))) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

278 
 exn_msg _ TERMINATE = "Exit." 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

279 
 exn_msg _ RESTART = "Restart." 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

280 
 exn_msg _ Interrupt = "Interrupt." 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

281 
 exn_msg _ TimeLimit.TimeOut = "Timeout." 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

282 
 exn_msg _ TOPLEVEL_ERROR = "Error." 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

283 
 exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

284 
 exn_msg _ (ERROR msg) = msg 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

285 
 exn_msg _ (Fail msg) = raised "Fail" [msg] 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

286 
 exn_msg _ (THEORY (msg, thys)) = 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

287 
raised "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else [])) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

288 
 exn_msg _ (Syntax.AST (msg, asts)) = raised "AST" (msg :: 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

289 
(if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else [])) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

290 
 exn_msg ctxt (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

291 
(if detailed then 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

292 
if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

293 
else [])) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

294 
 exn_msg ctxt (TERM (msg, ts)) = raised "TERM" (msg :: 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

295 
(if detailed then if_context ctxt Syntax.string_of_term ts else [])) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

296 
 exn_msg ctxt (THM (msg, i, thms)) = raised ("THM " ^ string_of_int i) (msg :: 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

297 
(if detailed then if_context ctxt ProofContext.string_of_thm thms else [])) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

298 
 exn_msg _ exn = raised (General.exnMessage exn) [] 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

299 
in exn_msg NONE e end; 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

300 

3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

301 
fun print_exn exn_info = Output.error_msg (exn_message (EXCURSION_FAIL exn_info)); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

302 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

303 
end; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

304 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

305 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

306 
(* controlled execution *) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

307 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

308 
local 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

309 

18685  310 
fun debugging f x = 
23940  311 
if ! debug then exception_trace (fn () => f x) 
18685  312 
else f x; 
313 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

314 
fun toplevel_error f x = 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

315 
let val ctxt = try ML_Context.the_local_context () in 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

316 
f x handle exn => 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

317 
(Output.error_msg (exn_message (exn_context ctxt exn)); raise TOPLEVEL_ERROR) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

318 
end; 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

319 

20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

320 
in 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

321 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

322 
fun controlled_execution f = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

323 
f 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

324 
> debugging 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

325 
> interruptible; 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

326 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

327 
fun program f = 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

328 
(f 
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

329 
> debugging 
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

330 
> toplevel_error) (); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

331 

8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

332 
end; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

333 

5828  334 

16815  335 
(* node transactions and recovery from stale theories *) 
6689  336 

16815  337 
(*NB: proof commands should be nondestructive!*) 
7022  338 

6689  339 
local 
340 

16452  341 
fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false; 
6689  342 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

343 
val stale_theory = ERROR "Stale theory encountered after successful execution!"; 
16815  344 

23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

345 
fun map_theory f = History.map_current 
21177  346 
(fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE) 
347 
 node => node); 

6689  348 

15531  349 
fun return (result, NONE) = result 
350 
 return (result, SOME exn) = raise FAILURE (result, exn); 

7022  351 

6689  352 
in 
353 

23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

354 
fun transaction hist pos f (node, term) = 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

355 
let 
21177  356 
val cont_node = map_theory Theory.checkpoint node; 
357 
val back_node = map_theory Theory.copy cont_node; 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

358 
fun state nd = State (nd, term); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

359 
fun normal_state nd = (state nd, NONE); 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

360 
fun error_state nd exn = (state nd, SOME exn); 
6689  361 

20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

362 
val (result, err) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

363 
cont_node 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

364 
> (f 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

365 
> (if hist then History.apply' (History.current back_node) else History.map_current) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

366 
> controlled_execution) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

367 
> normal_state 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

368 
handle exn => error_state cont_node exn; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

369 
in 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

370 
if is_stale result 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

371 
then return (error_state back_node (the_default stale_theory err)) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

372 
else return (result, err) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

373 
end; 
6689  374 

375 
end; 

376 

377 

378 
(* primitive transitions *) 

379 

18563  380 
(*Note: Recovery from stale theories is provided only for theorylevel 
18589  381 
operations via Transaction. Other node or state operations should 
382 
not touch theories at all. Interrupts are enabled only for Keep and 

383 
Transaction.*) 

5828  384 

385 
datatype trans = 

22056  386 
Init of (bool > theory) * ((theory > unit) * (theory > unit))  
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

387 
(*init node; with exit/kill operation*) 
25441
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

388 
InitEmpty of (state > bool) * (unit > unit)  (*init empty toplevel*) 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

389 
Exit  (*conclude node  deferred until init*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

390 
UndoExit  (*continue after conclusion*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

391 
Kill  (*abort node*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

392 
History of node History.T > node History.T  (*history operation (undo etc.)*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

393 
Keep of bool > state > unit  (*peek at state*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

394 
Transaction of bool * (bool > node > node); (*node transaction*) 
6689  395 

15531  396 
fun undo_limit int = if int then NONE else SOME 0; 
6689  397 

22056  398 
fun safe_exit (Toplevel (SOME (node, (exit, _)))) = 
399 
(case try the_global_theory (History.current node) of 

25219  400 
SOME thy => controlled_execution exit thy 
22056  401 
 NONE => ()) 
402 
 safe_exit _ = (); 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

403 

6689  404 
local 
5828  405 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

406 
fun keep_state int f = controlled_execution (fn x => tap (f int) x); 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

407 

23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

408 
fun apply_tr int _ (Init (f, term)) (state as Toplevel _) = 
22056  409 
let val node = Theory (Context.Theory (f int), NONE) 
410 
in safe_exit state; State (History.init (undo_limit int) node, term) end 

25441
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

411 
 apply_tr int _ (InitEmpty (check, f)) (state as Toplevel _) = 
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

412 
if check state then (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel) 
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

413 
else raise UNDEF 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

414 
 apply_tr _ _ Exit (State (node, term)) = 
22056  415 
(the_global_theory (History.current node); Toplevel (SOME (node, term))) 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

416 
 apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

417 
 apply_tr _ _ Kill (State (node, (_, kill))) = 
22056  418 
(kill (the_global_theory (History.current node)); toplevel) 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

419 
 apply_tr _ _ (History f) (State (node, term)) = State (f node, term) 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

420 
 apply_tr int _ (Keep f) state = keep_state int f state 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

421 
 apply_tr int pos (Transaction (hist, f)) (State state) = 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

422 
transaction hist pos (fn x => f int x) state 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

423 
 apply_tr _ _ _ _ = raise UNDEF; 
5828  424 

23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

425 
fun apply_union _ _ [] state = raise FAILURE (state, UNDEF) 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

426 
 apply_union int pos (tr :: trs) state = 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

427 
apply_tr int pos tr state 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

428 
handle UNDEF => apply_union int pos trs state 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

429 
 FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state 
6689  430 
 exn as FAILURE _ => raise exn 
431 
 exn => raise FAILURE (state, exn); 

432 

433 
in 

434 

23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

435 
fun apply_trans int pos trs state = (apply_union int pos trs state, NONE) 
15531  436 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  437 

438 
end; 

5828  439 

440 

441 
(* datatype transition *) 

442 

443 
datatype transition = Transition of 

16815  444 
{name: string, (*command name*) 
445 
pos: Position.T, (*source position*) 

446 
source: OuterLex.token list option, (*source text*) 

447 
int_only: bool, (*interactiveonly*) 

448 
print: string list, (*print modes (union)*) 

449 
no_timing: bool, (*suppress timing*) 

450 
trans: trans list}; (*primitive transitions (union)*) 

5828  451 

25960  452 
fun make_transition (name, pos, source, int_only, print, no_timing, trans) = 
453 
Transition {name = name, pos = pos, source = source, 

14923  454 
int_only = int_only, print = print, no_timing = no_timing, trans = trans}; 
5828  455 

25960  456 
fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) = 
457 
make_transition (f (name, pos, source, int_only, print, no_timing, trans)); 

5828  458 

25960  459 
val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []); 
14923  460 

461 
fun name_of (Transition {name, ...}) = name; 

462 
fun source_of (Transition {source, ...}) = source; 

5828  463 

464 

465 
(* diagnostics *) 

466 

467 
fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; 

468 

469 
fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr; 

470 
fun at_command tr = command_msg "At " tr ^ "."; 

471 

472 
fun type_error tr state = 

18685  473 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  474 

475 

476 
(* modify transitions *) 

477 

25960  478 
fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) => 
479 
(nm, pos, source, int_only, print, no_timing, trans)); 

5828  480 

25960  481 
fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) => 
482 
(name, pos, source, int_only, print, no_timing, trans)); 

9010  483 

25960  484 
fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => 
485 
(name, pos, SOME src, int_only, print, no_timing, trans)); 

5828  486 

25960  487 
fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) => 
488 
(name, pos, source, int_only, print, no_timing, trans)); 

14923  489 

25960  490 
val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) => 
491 
(name, pos, source, int_only, print, true, trans)); 

17363  492 

25960  493 
fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 
494 
(name, pos, source, int_only, print, no_timing, trans @ [tr])); 

17363  495 

25960  496 
fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 
497 
(name, pos, source, int_only, insert (op =) mode print, no_timing, trans)); 

16607  498 

499 
val print = print' ""; 

5828  500 

17363  501 
val three_buffersN = "three_buffers"; 
502 
val print3 = print' three_buffersN; 

5828  503 

504 

21007  505 
(* basic transitions *) 
5828  506 

22056  507 
fun init_theory f exit kill = add_trans (Init (f, (exit, kill))); 
25441
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

508 
fun init_empty check f = add_trans (InitEmpty (check, f)); 
6689  509 
val exit = add_trans Exit; 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

510 
val undo_exit = add_trans UndoExit; 
6689  511 
val kill = add_trans Kill; 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

512 
val history = add_trans o History; 
7612  513 
val keep' = add_trans o Keep; 
18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

514 
fun map_current f = add_trans (Transaction (false, f)); 
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

515 
fun app_current f = add_trans (Transaction (true, f)); 
5828  516 

7612  517 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  518 
fun imperative f = keep (fn _ => f ()); 
519 

21007  520 
val unknown_theory = imperative (fn () => warning "Unknown theory context"); 
521 
val unknown_proof = imperative (fn () => warning "Unknown proof context"); 

522 
val unknown_context = imperative (fn () => warning "Unknown context"); 

15668  523 

21007  524 

525 
(* theory transitions *) 

15668  526 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

527 
fun theory' f = app_current (fn int => 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

528 
(fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE) 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

529 
 _ => raise UNDEF)); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

530 

a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

531 
fun theory f = theory' (K f); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

532 

21294  533 
fun begin_local_theory begin f = app_current (fn _ => 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

534 
(fn Theory (Context.Theory thy, _) => 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

535 
let 
20985  536 
val lthy = f thy; 
21294  537 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
538 
in Theory (gthy, SOME lthy) end 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

539 
 _ => raise UNDEF)); 
17076  540 

21294  541 
val end_local_theory = app_current (fn _ => 
542 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) 

21007  543 
 _ => raise UNDEF)); 
544 

545 
local 

546 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

547 
fun local_theory_presentation loc f g = app_current (fn int => 
21294  548 
(fn Theory (gthy, _) => 
549 
let 

550 
val finish = loc_finish loc gthy; 

25960  551 
val lthy' = f (loc_begin loc gthy); 
21294  552 
in Theory (finish lthy', SOME lthy') end 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

553 
 _ => raise UNDEF) #> tap (g int)); 
15668  554 

21007  555 
in 
556 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

557 
fun local_theory loc f = local_theory_presentation loc f (K I); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

558 
fun present_local_theory loc g = local_theory_presentation loc I g; 
18955  559 

21007  560 
end; 
561 

562 

563 
(* proof transitions *) 

564 

565 
fun end_proof f = map_current (fn int => 

24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

566 
(fn Proof (prf, (finish, _)) => 
21007  567 
let val state = ProofHistory.current prf in 
568 
if can (Proof.assert_bottom true) state then 

569 
let 

570 
val ctxt' = f int state; 

571 
val gthy' = finish ctxt'; 

572 
in Theory (gthy', SOME ctxt') end 

573 
else raise UNDEF 

574 
end 

575 
 SkipProof (h, (gthy, _)) => 

576 
if History.current h = 0 then Theory (gthy, NONE) else raise UNDEF 

577 
 _ => raise UNDEF)); 

578 

21294  579 
local 
580 

581 
fun begin_proof init finish = app_current (fn int => 

582 
(fn Theory (gthy, _) => 

583 
let 

24453  584 
val prf = init int gthy; 
21294  585 
val schematic = Proof.schematic_goal prf; 
586 
in 

587 
if ! skip_proofs andalso schematic then 

588 
warning "Cannot skip proof of schematic goal statement" 

589 
else (); 

590 
if ! skip_proofs andalso not schematic then 

591 
SkipProof 

592 
(History.init (undo_limit int) 0, (finish gthy (Proof.global_skip_proof int prf), gthy)) 

593 
else Proof (ProofHistory.init (undo_limit int) prf, (finish gthy, gthy)) 

594 
end 

595 
 _ => raise UNDEF)); 

596 

597 
in 

598 

24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

599 
fun local_theory_to_proof' loc f = begin_proof 
25960  600 
(fn int => fn gthy => f int (loc_begin loc gthy)) 
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

601 
(loc_finish loc); 
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

602 

24453  603 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  604 

605 
fun theory_to_proof f = begin_proof 

24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

606 
(K (fn Context.Theory thy => f thy  _ => raise UNDEF)) 
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

607 
(K (Context.Theory o ProofContext.theory_of)); 
21294  608 

609 
end; 

610 

21007  611 
val forget_proof = map_current (fn _ => 
612 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

613 
 SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

614 
 _ => raise UNDEF)); 

615 

21177  616 
fun present_proof f = map_current (fn int => 
617 
(fn Proof (prf, x) => Proof (ProofHistory.apply I prf, x) 

618 
 SkipProof (h, x) => SkipProof (History.apply I h, x) 

619 
 _ => raise UNDEF) #> tap (f int)); 

620 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

621 
fun proofs' f = map_current (fn int => 
21007  622 
(fn Proof (prf, x) => Proof (ProofHistory.applys (f int) prf, x) 
623 
 SkipProof (h, x) => SkipProof (History.apply I h, x) 

16815  624 
 _ => raise UNDEF)); 
15668  625 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

626 
fun proof' f = proofs' (Seq.single oo f); 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

627 
val proofs = proofs' o K; 
6689  628 
val proof = proof' o K; 
16815  629 

630 
fun actual_proof f = map_current (fn _ => 

21007  631 
(fn Proof (prf, x) => Proof (f prf, x) 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

632 
 _ => raise UNDEF)); 
16815  633 

634 
fun skip_proof f = map_current (fn _ => 

21007  635 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  636 
 _ => raise UNDEF)); 
637 

16815  638 
fun skip_proof_to_theory p = map_current (fn _ => 
21007  639 
(fn SkipProof (h, (gthy, _)) => 
640 
if p (History.current h) then Theory (gthy, NONE) 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

641 
else raise UNDEF 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

642 
 _ => raise UNDEF)); 
5828  643 

644 

645 

646 
(** toplevel transactions **) 

647 

25960  648 
(* thread position *) 
25799  649 

25960  650 
fun setmp_thread_position (Transition {pos, ...}) f x = 
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset

651 
Position.setmp_thread_data pos f x; 
25799  652 

653 

5828  654 
(* apply transitions *) 
655 

6664  656 
local 
657 

25799  658 
fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) = 
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset

659 
setmp_thread_position tr (fn state => 
25799  660 
let 
661 
val _ = 

662 
if not int andalso int_only then warning (command_msg "Interactiveonly " tr) 

663 
else (); 

16682  664 

25799  665 
fun do_timing f x = (warning (command_msg "" tr); timeap f x); 
666 
fun do_profiling f x = profile (! profiling) f x; 

667 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

668 
val (result, status) = 
25799  669 
state > (apply_trans int pos trans 
670 
> (if ! profiling > 0 andalso not no_timing then do_profiling else I) 

671 
> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); 

672 
val _ = 

673 
if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ()) 

674 
then print_state false result else (); 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

675 

3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

676 
in (result, Option.map (fn UNDEF => type_error tr state  exn => exn) status) end); 
6664  677 

678 
in 

5828  679 

6689  680 
fun apply int tr st = 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

681 
let val ctxt = try context_of st in 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

682 
(case app int tr st of 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

683 
(_, SOME TERMINATE) => NONE 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

684 
 (_, SOME RESTART) => SOME (toplevel, NONE) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

685 
 (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

686 
 (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr)) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

687 
 (state', NONE) => SOME (state', NONE)) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

688 
end; 
6664  689 

690 
end; 

5828  691 

692 

17076  693 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  694 

6664  695 
local 
696 

5828  697 
fun excur [] x = x 
17076  698 
 excur ((tr, pr) :: trs) (st, res) = 
17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

699 
(case apply (! interact) tr st of 
15531  700 
SOME (st', NONE) => 
18685  701 
excur trs (st', pr st st' res handle exn => 
10324  702 
raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) 
15531  703 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 
704 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

5828  705 

17076  706 
fun no_pr _ _ _ = (); 
707 

6664  708 
in 
709 

17076  710 
fun present_excursion trs res = 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

711 
(case excur trs (toplevel, res) of 
22056  712 
(state as Toplevel _, res') => (safe_exit state; res') 
18685  713 
 _ => error "Unfinished development at end of input") 
9134  714 
handle exn => error (exn_message exn); 
715 

17076  716 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  717 

6664  718 
end; 
719 

5828  720 

721 

722 
(** interactive transformations **) 

723 

724 
(* the global state reference *) 

725 

15531  726 
val global_state = ref (toplevel, NONE: (exn * string) option); 
5828  727 

15531  728 
fun set_state state = global_state := (state, NONE); 
5828  729 
fun get_state () = fst (! global_state); 
730 
fun exn () = snd (! global_state); 

731 

732 

24295
af8dbc7a2305
global state transformation: noncritical, but also nonthreadsafe;
wenzelm
parents:
24058
diff
changeset

733 
(* apply transformers to global state  NOT THREADSAFE! *) 
5828  734 

14985  735 
nonfix >> >>>; 
5828  736 

24295
af8dbc7a2305
global state transformation: noncritical, but also nonthreadsafe;
wenzelm
parents:
24058
diff
changeset

737 
fun >> tr = 
5828  738 
(case apply true tr (get_state ()) of 
15531  739 
NONE => false 
740 
 SOME (state', exn_info) => 

5828  741 
(global_state := (state', exn_info); 
25809
decb98ff92dd
toplevel print_exn: proper setmp_thread_properties;
wenzelm
parents:
25799
diff
changeset

742 
(case exn_info of 
decb98ff92dd
toplevel print_exn: proper setmp_thread_properties;
wenzelm
parents:
25799
diff
changeset

743 
NONE => () 
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset

744 
 SOME err => setmp_thread_position tr print_exn err); 
24295
af8dbc7a2305
global state transformation: noncritical, but also nonthreadsafe;
wenzelm
parents:
24058
diff
changeset

745 
true)); 
5828  746 

14985  747 
fun >>> [] = () 
748 
 >>> (tr :: trs) = if >> tr then >>> trs else (); 

749 

25441
4028958d19ff
init_empty: check before change (avoids nonlinear update);
wenzelm
parents:
25292
diff
changeset

750 
fun init_state () = (>> (init_empty (K true) (K ()) empty); ()); 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

751 

9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

752 

9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

753 
(* the Isar source of transitions *) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

754 

9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

755 
type 'a isar = 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

756 
(transition, (transition option, 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

757 
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

758 
Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

759 
Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

760 

25527
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

761 
local 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

762 

17513
0393718c2f1c
get_interrupt: special handling of IO.io now in MLSystems/smlnjbasiscompat.ML;
wenzelm
parents:
17500
diff
changeset

763 
(*Spurious interrupts ahead! Race condition?*) 
0393718c2f1c
get_interrupt: special handling of IO.io now in MLSystems/smlnjbasiscompat.ML;
wenzelm
parents:
17500
diff
changeset

764 
fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE; 
7602  765 

25527
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

766 
fun raw_loop secure src = 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

767 
let 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

768 
fun check_secure () = 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

769 
(if secure then warning "Secure loop  cannot exit to ML" else (); secure); 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

770 
in 
25847  771 
(case get_interrupt (Source.set_prompt Source.default_prompt src) of 
25527
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

772 
NONE => (writeln "\nInterrupt."; raw_loop secure src) 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

773 
 SOME NONE => if secure then quit () else () 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

774 
 SOME (SOME (tr, src')) => if >> tr orelse check_secure () then raw_loop secure src' else ()) 
25584  775 
handle exn => (CRITICAL (fn () => change crashes (cons exn)); 
776 
warning "Recovering after Isar toplevel crash  see also Toplevel.crashes"; 

777 
raw_loop secure src) 

23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

778 
end; 
5828  779 

25527
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

780 
in 
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

781 

26081  782 
fun loop secure src = uninterruptible (fn _ => raw_loop secure) src; 
5828  783 

784 
end; 

25527
330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

785 

330ca6e1dca8
Toplevel.loop: explicit argument for secure loop, no warning on quit;
wenzelm
parents:
25441
diff
changeset

786 
end; 