author  wenzelm 
Wed, 10 Jan 2007 20:16:52 +0100  
changeset 22056  858016d00449 
parent 22014  4b70cbd96007 
child 22089  d9b614dc883d 
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 
5828  26 
val theory_of: state > theory 
27 
val proof_of: state > Proof.state 

18589  28 
val proof_position_of: state > int 
21007  29 
val enter_proof_body: state > Proof.state 
16815  30 
val prompt_state_default: state > string 
31 
val prompt_state_fn: (state > string) ref 

32 
val print_state_context: state > unit 

33 
val print_state_default: bool > state > unit 

34 
val print_state_fn: (bool > state > unit) ref 

35 
val print_state: bool > state > unit 

36 
val pretty_state: bool > state > Pretty.T list 

16682  37 
val quiet: bool ref 
38 
val debug: bool ref 

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

39 
val interact: bool ref 
16682  40 
val timing: bool ref 
41 
val profiling: int ref 

16815  42 
val skip_proofs: bool ref 
5828  43 
exception TERMINATE 
5990  44 
exception RESTART 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

75 
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

76 
val present_local_theory: xstring option > (bool > node > unit) > transition > transition 
21007  77 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
78 
transition > transition 

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

21177  82 
val present_proof: (bool > node > unit) > transition > transition 
83 
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

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

16815  87 
val actual_proof: (ProofHistory.T > ProofHistory.T) > transition > transition 
88 
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

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

92 
val unknown_context: transition > transition 

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

96 
val get_state: unit > state 

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

98 
val >> : transition > bool 

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

100 
val init_state: unit > unit 
14091  101 
type 'a isar 
102 
val loop: 'a isar > unit 

5828  103 
end; 
104 

6965  105 
structure Toplevel: TOPLEVEL = 
5828  106 
struct 
107 

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

108 

5828  109 
(** toplevel state **) 
110 

19063  111 
exception UNDEF; 
112 

113 

21294  114 
(* local theory wrappers *) 
5828  115 

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

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

117 

21294  118 
val loc_init = TheoryTarget.init; 
119 

120 
val loc_exit = ProofContext.theory_of o LocalTheory.exit; 

121 

122 
fun loc_begin loc (Context.Theory thy) = loc_init loc thy 

123 
 loc_begin NONE (Context.Proof lthy) = lthy 

124 
 loc_begin loc (Context.Proof lthy) = loc_init loc (loc_exit lthy); 

125 

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

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

128 
 loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o LocalTheory.reinit lthy o loc_exit; 

129 

130 

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

131 
(* datatype node *) 
21294  132 

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

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

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

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

22056  140 
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

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

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

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

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

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

149 
 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

150 
 presentation_context (SOME node) (SOME loc) = 
21294  151 
loc_init (SOME 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

152 
 presentation_context NONE _ = raise UNDEF; 
19063  153 

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

154 

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

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

156 

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

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

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

160 
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

161 
State of state_info; 
5828  162 

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

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

164 

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

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

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

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

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

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

172 
 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

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

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

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

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

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

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

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

182 

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

183 

5828  184 
(* top node *) 
185 

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

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

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

189 
val node_of = History.current o node_history_of; 

5828  190 

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

193 

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

21506  196 
val context_of = node_case Context.proof_of Proof.context_of; 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

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

18589  200 
fun proof_position_of state = 
201 
(case node_of state of 

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

203 
 _ => raise UNDEF); 

6664  204 

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

207 

16815  208 
(* prompt state *) 
209 

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

210 
fun prompt_state_default (_: state) = Source.default_prompt; 
16815  211 

212 
val prompt_state_fn = ref prompt_state_default; 

213 
fun prompt_state state = ! prompt_state_fn state; 

214 

215 

216 
(* print state *) 

217 

21294  218 
val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I; 
16815  219 

220 
fun pretty_state_context state = 

21506  221 
(case try (node_case I (Context.Proof o Proof.context_of)) state of 
222 
NONE => [] 

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

223 
 SOME gthy => pretty_context gthy); 
16815  224 

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

225 
fun pretty_node prf_only (Theory (gthy, _)) = if prf_only then [] else pretty_context gthy 
18563  226 
 pretty_node _ (Proof (prf, _)) = 
16815  227 
Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf) 
21007  228 
 pretty_node _ (SkipProof (h, _)) = 
16815  229 
[Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))]; 
230 

231 
fun pretty_state prf_only state = 

232 
let val ref (begin_state, end_state, _) = Display.current_goals_markers in 

233 
(case try node_of state of NONE => [] 

234 
 SOME node => 

235 
(if begin_state = "" then [] else [Pretty.str begin_state]) @ 

236 
pretty_node prf_only node @ 

237 
(if end_state = "" then [] else [Pretty.str end_state])) 

238 
end; 

239 

240 
val print_state_context = Pretty.writelns o pretty_state_context; 

241 
fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state); 

242 

243 
val print_state_fn = ref print_state_default; 

21231  244 
fun print_state prf_only state = ! print_state_fn prf_only state; 
16815  245 

246 

15668  247 

5828  248 
(** toplevel transitions **) 
249 

16682  250 
val quiet = ref false; 
251 
val debug = ref false; 

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

252 
val interact = ref false; 
16682  253 
val timing = Output.timing; 
254 
val profiling = ref 0; 

16815  255 
val skip_proofs = ref false; 
16682  256 

5828  257 
exception TERMINATE; 
5990  258 
exception RESTART; 
7022  259 
exception EXCURSION_FAIL of exn * string; 
6689  260 
exception FAILURE of state * exn; 
5828  261 

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 
(* print exceptions *) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

264 

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

265 
local 
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 
fun with_context f xs = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

268 
(case Context.get_context () of NONE => [] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

269 
 SOME thy => map (f thy) xs); 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

270 

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

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

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

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

274 

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

275 
fun exn_msg _ TERMINATE = "Exit." 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

276 
 exn_msg _ RESTART = "Restart." 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

277 
 exn_msg _ Interrupt = "Interrupt." 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

278 
 exn_msg _ Output.TOPLEVEL_ERROR = "Error." 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

279 
 exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

280 
 exn_msg _ (ERROR msg) = msg 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

281 
 exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

282 
 exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

283 
 exn_msg false (THEORY (msg, _)) = msg 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

284 
 exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

285 
 exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

286 
fail_msg detailed "simproc" ((name, Position.none), exn) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

287 
 exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

288 
 exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

289 
 exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

290 
 exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

291 
 exn_msg true (Syntax.AST (msg, asts)) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

292 
raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

293 
 exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

294 
 exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

295 
with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

296 
 exn_msg false (TERM (msg, _)) = raised "TERM" [msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

297 
 exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

298 
 exn_msg false (THM (msg, _, _)) = raised "THM" [msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

299 
 exn_msg true (THM (msg, i, thms)) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

300 
raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

301 
 exn_msg _ Option.Option = raised "Option" [] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

302 
 exn_msg _ Library.UnequalLengths = raised "UnequalLengths" [] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

303 
 exn_msg _ Empty = raised "Empty" [] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

304 
 exn_msg _ Subscript = raised "Subscript" [] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

305 
 exn_msg _ (Fail msg) = raised "Fail" [msg] 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

306 
 exn_msg _ exn = General.exnMessage exn 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

307 
and fail_msg detailed kind ((name, pos), exn) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

308 
"Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

309 

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

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

311 

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

312 
fun exn_message exn = exn_msg (! debug) exn; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

313 

22014
4b70cbd96007
removed Toplevel.print_exn hook  existing error_msg_fn does the job;
wenzelm
parents:
21986
diff
changeset

314 
fun print_exn NONE = () 
4b70cbd96007
removed Toplevel.print_exn hook  existing error_msg_fn does the job;
wenzelm
parents:
21986
diff
changeset

315 
 print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

316 

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

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

318 

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

319 

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

320 
(* controlled execution *) 
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 
local 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

323 

18685  324 
fun debugging f x = 
325 
if ! debug then 

326 
setmp Library.do_transform_failure false 

327 
exception_trace (fn () => f x) 

328 
else f x; 

329 

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

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

331 
let val y = ref x 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

332 
in raise_interrupt (fn () => y := f x) (); ! y end; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

333 

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

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

335 

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

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

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

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

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

340 
> setmp Output.do_toplevel_errors false; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

341 

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

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

343 
Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) (); 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

344 

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

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

346 

5828  347 

16815  348 
(* node transactions and recovery from stale theories *) 
6689  349 

16815  350 
(*NB: proof commands should be nondestructive!*) 
7022  351 

6689  352 
local 
353 

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

18685  356 
val stale_theory = ERROR "Stale theory encountered after succesful execution!"; 
16815  357 

21177  358 
fun map_theory f = History.map 
359 
(fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE) 

360 
 node => node); 

6689  361 

15531  362 
fun return (result, NONE) = result 
363 
 return (result, SOME exn) = raise FAILURE (result, exn); 

7022  364 

6689  365 
in 
366 

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

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

368 
let 
21177  369 
val cont_node = map_theory Theory.checkpoint node; 
370 
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

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

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

373 
fun error_state nd exn = (state nd, SOME exn); 
6689  374 

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

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

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

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

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

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

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

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

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

384 
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

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

386 
end; 
6689  387 

388 
end; 

389 

390 

391 
(* primitive transitions *) 

392 

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

396 
Transaction.*) 

5828  397 

398 
datatype trans = 

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

400 
(*init node; with exit/kill operation*) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

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

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

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

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

405 
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

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

407 
Transaction of bool * (bool > node > node); (*node transaction*) 
6689  408 

15531  409 
fun undo_limit int = if int then NONE else SOME 0; 
6689  410 

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

413 
SOME thy => exit thy 

414 
 NONE => ()) 

415 
 safe_exit _ = (); 

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

416 

6689  417 
local 
5828  418 

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

419 
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

420 

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

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

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

424 
 apply_tr int (InitEmpty f) state = 
22056  425 
(keep_state int (K f) state; safe_exit state; toplevel) 
426 
 apply_tr _ Exit (State (node, term)) = 

427 
(the_global_theory (History.current node); Toplevel (SOME (node, term))) 

428 
 apply_tr _ UndoExit (Toplevel (SOME state_info)) = State state_info 

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

429 
 apply_tr _ Kill (State (node, (_, kill))) = 
22056  430 
(kill (the_global_theory (History.current node)); toplevel) 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

431 
 apply_tr _ (History f) (State (node, term)) = State (f node, term) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

432 
 apply_tr int (Keep f) state = keep_state int f state 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

433 
 apply_tr int (Transaction (hist, f)) (State state) = 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

434 
transaction hist (fn x => f int x) state 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

435 
 apply_tr _ _ _ = raise UNDEF; 
5828  436 

6689  437 
fun apply_union _ [] state = raise FAILURE (state, UNDEF) 
438 
 apply_union int (tr :: trs) state = 

18685  439 
apply_tr int tr state 
6689  440 
handle UNDEF => apply_union int trs state 
441 
 FAILURE (alt_state, UNDEF) => apply_union int trs alt_state 

442 
 exn as FAILURE _ => raise exn 

443 
 exn => raise FAILURE (state, exn); 

444 

445 
in 

446 

15531  447 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
448 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 

6689  449 

450 
end; 

5828  451 

452 

453 
(* datatype transition *) 

454 

455 
datatype transition = Transition of 

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

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

459 
int_only: bool, (*interactiveonly*) 

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

461 
no_timing: bool, (*suppress timing*) 

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

5828  463 

14923  464 
fun make_transition (name, pos, source, int_only, print, no_timing, trans) = 
465 
Transition {name = name, pos = pos, source = source, 

466 
int_only = int_only, print = print, no_timing = no_timing, trans = trans}; 

5828  467 

14923  468 
fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) = 
469 
make_transition (f (name, pos, source, int_only, print, no_timing, trans)); 

5828  470 

16607  471 
val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []); 
14923  472 

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

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

5828  475 

476 

477 
(* diagnostics *) 

478 

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

480 

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

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

483 

484 
fun type_error tr state = 

18685  485 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  486 

487 

488 
(* modify transitions *) 

489 

14923  490 
fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) => 
491 
(nm, pos, source, int_only, print, no_timing, trans)); 

5828  492 

14923  493 
fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) => 
494 
(name, pos, source, int_only, print, no_timing, trans)); 

9010  495 

14923  496 
fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => 
15531  497 
(name, pos, SOME src, int_only, print, no_timing, trans)); 
5828  498 

14923  499 
fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) => 
500 
(name, pos, source, int_only, print, no_timing, trans)); 

501 

17363  502 
val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) => 
503 
(name, pos, source, int_only, print, true, trans)); 

504 

505 
fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 

506 
(name, pos, source, int_only, print, no_timing, trans @ [tr])); 

507 

16607  508 
fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 
509 
(name, pos, source, int_only, insert (op =) mode print, no_timing, trans)); 

510 

511 
val print = print' ""; 

5828  512 

17363  513 
val three_buffersN = "three_buffers"; 
514 
val print3 = print' three_buffersN; 

5828  515 

516 

21007  517 
(* basic transitions *) 
5828  518 

22056  519 
fun init_theory f exit kill = add_trans (Init (f, (exit, kill))); 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

520 
val init_empty = add_trans o InitEmpty; 
6689  521 
val exit = add_trans Exit; 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

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

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

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

527 
fun app_current f = add_trans (Transaction (true, f)); 
5828  528 

7612  529 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  530 
fun imperative f = keep (fn _ => f ()); 
531 

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

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

15668  535 

21007  536 

537 
(* theory transitions *) 

15668  538 

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

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

540 
(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

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

542 

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

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

544 

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

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

547 
let 
20985  548 
val lthy = f thy; 
21294  549 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
550 
in Theory (gthy, SOME lthy) end 

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

551 
 _ => raise UNDEF)); 
17076  552 

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

21007  555 
 _ => raise UNDEF)); 
556 

557 
local 

558 

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

559 
fun local_theory_presentation loc f g = app_current (fn int => 
21294  560 
(fn Theory (gthy, _) => 
561 
let 

562 
val finish = loc_finish loc gthy; 

563 
val lthy' = f (loc_begin loc gthy); 

564 
in Theory (finish lthy', SOME lthy') end 

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

565 
 _ => raise UNDEF) #> tap (g int)); 
15668  566 

21007  567 
in 
568 

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

569 
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

570 
fun present_local_theory loc g = local_theory_presentation loc I g; 
18955  571 

21007  572 
end; 
573 

574 

575 
(* proof transitions *) 

576 

577 
fun end_proof f = map_current (fn int => 

578 
(fn Proof (prf, (finish, orig_gthy)) => 

579 
let val state = ProofHistory.current prf in 

580 
if can (Proof.assert_bottom true) state then 

581 
let 

582 
val ctxt' = f int state; 

583 
val gthy' = finish ctxt'; 

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

585 
else raise UNDEF 

586 
end 

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

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

589 
 _ => raise UNDEF)); 

590 

21294  591 
local 
592 

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

594 
(fn Theory (gthy, _) => 

595 
let 

596 
val prf = init gthy; 

597 
val schematic = Proof.schematic_goal prf; 

598 
in 

599 
if ! skip_proofs andalso schematic then 

600 
warning "Cannot skip proof of schematic goal statement" 

601 
else (); 

602 
if ! skip_proofs andalso not schematic then 

603 
SkipProof 

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

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

606 
end 

607 
 _ => raise UNDEF)); 

608 

609 
in 

610 

611 
fun local_theory_to_proof loc f = begin_proof (f o loc_begin loc) (loc_finish loc); 

612 

613 
fun theory_to_proof f = begin_proof 

614 
(fn Context.Theory thy => f thy  _ => raise UNDEF) 

615 
(K (Context.Theory o ProofContext.theory_of)); 

616 

617 
end; 

618 

21007  619 
val forget_proof = map_current (fn _ => 
620 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

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

622 
 _ => raise UNDEF)); 

623 

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

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

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

628 

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

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

16815  632 
 _ => raise UNDEF)); 
15668  633 

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

634 
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

635 
val proofs = proofs' o K; 
6689  636 
val proof = proof' o K; 
16815  637 

638 
fun actual_proof f = map_current (fn _ => 

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

640 
 _ => raise UNDEF)); 
16815  641 

642 
fun skip_proof f = map_current (fn _ => 

21007  643 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  644 
 _ => raise UNDEF)); 
645 

16815  646 
fun skip_proof_to_theory p = map_current (fn _ => 
21007  647 
(fn SkipProof (h, (gthy, _)) => 
648 
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

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

650 
 _ => raise UNDEF)); 
5828  651 

652 

653 

654 
(** toplevel transactions **) 

655 

656 
(* apply transitions *) 

657 

6664  658 
local 
659 

9010  660 
fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = 
5828  661 
let 
21962  662 
val _ = 
663 
if not int andalso int_only then warning (command_msg "Interactiveonly " tr) 

664 
else (); 

16682  665 

18685  666 
fun do_timing f x = (Output.info (command_msg "" tr); timeap f x); 
16682  667 
fun do_profiling f x = profile (! profiling) f x; 
668 

6689  669 
val (result, opt_exn) = 
16729  670 
state > (apply_trans int trans 
671 
> (if ! profiling > 0 then do_profiling else I) 

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

21962  673 
val _ = 
674 
if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode) 

675 
then print_state false result else (); 

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

678 
in 

5828  679 

6689  680 
fun apply int tr st = 
6965  681 
(case app int tr st of 
15531  682 
(_, SOME TERMINATE) => NONE 
683 
 (_, SOME RESTART) => SOME (toplevel, NONE) 

684 
 (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info) 

685 
 (state', SOME exn) => SOME (state', SOME (exn, at_command tr)) 

686 
 (state', NONE) => SOME (state', NONE)); 

6664  687 

688 
end; 

5828  689 

690 

17076  691 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  692 

6664  693 
local 
694 

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

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

5828  703 

17076  704 
fun no_pr _ _ _ = (); 
705 

6664  706 
in 
707 

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

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

17076  714 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  715 

6664  716 
end; 
717 

5828  718 

719 

720 
(** interactive transformations **) 

721 

722 
(* the global state reference *) 

723 

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

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

729 

730 

731 
(* apply transformers to global state *) 

732 

14985  733 
nonfix >> >>>; 
5828  734 

735 
fun >> tr = 

736 
(case apply true tr (get_state ()) of 

15531  737 
NONE => false 
738 
 SOME (state', exn_info) => 

5828  739 
(global_state := (state', exn_info); 
22014
4b70cbd96007
removed Toplevel.print_exn hook  existing error_msg_fn does the job;
wenzelm
parents:
21986
diff
changeset

740 
print_exn exn_info; 
5828  741 
true)); 
742 

14985  743 
fun >>> [] = () 
744 
 >>> (tr :: trs) = if >> tr then >>> trs else (); 

745 

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

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

747 

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

748 

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

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

750 

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

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

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

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

754 
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

755 
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

756 

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

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

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

20928  760 
fun warn_secure () = 
761 
let val secure = Secure.is_secure () 

762 
in if secure then warning "Cannot exit to ML in secure mode" else (); secure end; 

763 

5828  764 
fun raw_loop src = 
7602  765 
(case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of 
15531  766 
NONE => (writeln "\nInterrupt."; raw_loop src) 
20928  767 
 SOME NONE => if warn_secure () then quit () else () 
768 
 SOME (SOME (tr, src')) => 

769 
if >> tr orelse warn_secure () then raw_loop src' 

770 
else ()); 

5828  771 

12987  772 
fun loop src = ignore_interrupt raw_loop src; 
5828  773 

774 
end; 