author  wenzelm 
Fri, 10 Nov 2006 22:18:54 +0100  
changeset 21294  5cd48242ef17 
parent 21277  ac2d7e03a3b1 
child 21310  bfcc24fc7c46 
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 
18 
val toplevel: state 

7732  19 
val is_toplevel: state > bool 
18589  20 
val is_theory: state > bool 
21 
val is_proof: state > bool 

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

26 
val node_case: (generic_theory > 'a) > (Proof.state > 'a) > state > 'a 
18641  27 
val context_of: state > Context.generic 
5828  28 
val theory_of: state > theory 
29 
val proof_of: state > Proof.state 

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

34 
val print_state_context: state > unit 

35 
val print_state_default: bool > state > unit 

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

37 
val print_state: bool > state > unit 

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

16682  39 
val quiet: bool ref 
40 
val debug: bool ref 

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

41 
val interact: bool ref 
16682  42 
val timing: bool ref 
43 
val profiling: int ref 

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

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

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

5828  54 
val name: string > transition > transition 
55 
val position: Position.T > transition > transition 

14923  56 
val source: OuterLex.token list > transition > transition 
5828  57 
val interactive: bool > transition > transition 
58 
val print: transition > transition 

16607  59 
val print': string > transition > transition 
17363  60 
val three_buffersN: string 
61 
val print3: transition > transition 

9010  62 
val no_timing: transition > transition 
5828  63 
val reset: transition > transition 
8465  64 
val init: (bool > node) > (node > unit) > (node > unit) > transition > transition 
6689  65 
val exit: transition > transition 
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 
21007  71 
val init_theory: (bool > theory) > (theory > unit) > (theory > unit) > 
72 
transition > transition 

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

77 
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

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

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

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

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

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

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

94 
val unknown_context: transition > transition 

5828  95 
val apply: bool > transition > state > (state * (exn * string) option) option 
17076  96 
val present_excursion: (transition * (state > state > 'a > 'a)) list > 'a > 'a 
5828  97 
val excursion: transition list > unit 
98 
val set_state: state > unit 

99 
val get_state: unit > state 

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

101 
val >> : transition > bool 

14985  102 
val >>> : transition list > unit 
14091  103 
type 'a isar 
104 
val loop: 'a isar > unit 

5828  105 
end; 
106 

6965  107 
structure Toplevel: TOPLEVEL = 
5828  108 
struct 
109 

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 

21294  119 
val loc_init = TheoryTarget.init; 
120 

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

122 

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

124 
 loc_begin NONE (Context.Proof lthy) = lthy 

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

126 

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

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

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

130 

131 

132 
(* datatype state *) 

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 

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 

8465  154 
datatype state = State of (node History.T * ((node > unit) * (node > unit))) option; 
5828  155 

15531  156 
val toplevel = State NONE; 
5828  157 

15531  158 
fun is_toplevel (State NONE) = true 
7732  159 
 is_toplevel _ = false; 
160 

17076  161 
fun level (State NONE) = 0 
162 
 level (State (SOME (node, _))) = 

163 
(case History.current node of 

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

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

165 
 Theory (Context.Proof _, _) => 1 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

166 
 Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1 
21007  167 
 SkipProof (h, _) => History.current h + 2); (*different notion of proof depth!*) 
17076  168 

15531  169 
fun str_of_state (State NONE) = "at top level" 
16815  170 
 str_of_state (State (SOME (node, _))) = 
171 
(case History.current node of 

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

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

173 
 Theory (Context.Proof _, _) => "in local theory mode" 
16815  174 
 Proof _ => "in proof mode" 
175 
 SkipProof _ => "in skipped proof mode"); 

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

176 

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

177 

5828  178 
(* top node *) 
179 

17266  180 
fun assert true = () 
181 
 assert false = raise UNDEF; 

182 

15531  183 
fun node_history_of (State NONE) = raise UNDEF 
184 
 node_history_of (State (SOME (node, _))) = node; 

6689  185 

186 
val node_of = History.current o node_history_of; 

5828  187 

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

190 

19063  191 
fun node_case f g state = cases_node f g (node_of state); 
5828  192 

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

193 
val context_of = node_case I (Context.Proof o Proof.context_of); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

194 
val theory_of = node_case Context.theory_of Proof.theory_of; 
18589  195 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  196 

18589  197 
fun proof_position_of state = 
198 
(case node_of state of 

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

200 
 _ => raise UNDEF); 

6664  201 

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

204 

16815  205 
(* prompt state *) 
206 

207 
fun prompt_state_default (State _) = Source.default_prompt; 

208 

209 
val prompt_state_fn = ref prompt_state_default; 

210 
fun prompt_state state = ! prompt_state_fn state; 

211 

212 

213 
(* print state *) 

214 

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

217 
fun pretty_state_context state = 

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

218 
(case try context_of state of NONE => [] 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

219 
 SOME gthy => pretty_context gthy); 
16815  220 

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

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

227 
fun pretty_state prf_only state = 

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

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

230 
 SOME node => 

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

232 
pretty_node prf_only node @ 

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

234 
end; 

235 

236 
val print_state_context = Pretty.writelns o pretty_state_context; 

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

238 

239 
val print_state_fn = ref print_state_default; 

21231  240 
fun print_state prf_only state = ! print_state_fn prf_only state; 
16815  241 

242 

15668  243 

5828  244 
(** toplevel transitions **) 
245 

16682  246 
val quiet = ref false; 
247 
val debug = ref false; 

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

248 
val interact = ref false; 
16682  249 
val timing = Output.timing; 
250 
val profiling = ref 0; 

16815  251 
val skip_proofs = ref false; 
16682  252 

5828  253 
exception TERMINATE; 
5990  254 
exception RESTART; 
7022  255 
exception EXCURSION_FAIL of exn * string; 
6689  256 
exception FAILURE of state * exn; 
5828  257 

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

258 

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

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

260 

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

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

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

265 
 SOME thy => map (f thy) xs); 
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 raised name [] = "exception " ^ name ^ " raised" 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

269 
 raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); 
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 exn_msg _ TERMINATE = "Exit." 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

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

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

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

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

277 
 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

278 
 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

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

280 
 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

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

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

283 
 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

284 
 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

285 
 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

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

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

288 
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

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

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

291 
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

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

293 
 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

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

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

296 
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

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

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

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

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

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

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

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

304 
"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

305 

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

306 
in 
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 
fun exn_message exn = exn_msg (! debug) 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 
fun print_exn NONE = () 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

312 

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

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

314 

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

315 

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

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

317 

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

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

319 

18685  320 
fun debugging f x = 
321 
if ! debug then 

322 
setmp Library.do_transform_failure false 

323 
exception_trace (fn () => f x) 

324 
else f x; 

325 

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

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

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

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

329 

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

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

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

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

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

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

337 

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

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

339 
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

340 

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

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

342 

5828  343 

16815  344 
(* node transactions and recovery from stale theories *) 
6689  345 

16815  346 
(*NB: proof commands should be nondestructive!*) 
7022  347 

6689  348 
local 
349 

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

18685  352 
val stale_theory = ERROR "Stale theory encountered after succesful execution!"; 
16815  353 

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

356 
 node => node); 

6689  357 

15531  358 
fun return (result, NONE) = result 
359 
 return (result, SOME exn) = raise FAILURE (result, exn); 

7022  360 

6689  361 
in 
362 

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

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

364 
let 
21177  365 
val cont_node = map_theory Theory.checkpoint node; 
366 
val back_node = map_theory Theory.copy cont_node; 

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

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

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

369 
fun error_state nd exn = (state nd, SOME exn); 
6689  370 

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

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

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

373 
> (f 
21177  374 
> (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

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

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

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

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

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

380 
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

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

382 
end; 
6689  383 

384 
end; 

385 

386 

387 
(* primitive transitions *) 

388 

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

392 
Transaction.*) 

5828  393 

394 
datatype trans = 

18563  395 
Reset  (*empty toplevel*) 
8465  396 
Init of (bool > node) * ((node > unit) * (node > unit))  
18563  397 
(*init node; with exit/kill operation*) 
398 
Exit  (*conclude node*) 

399 
Kill  (*abort node*) 

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

400 
History of node History.T > node History.T  (*history operation (undo etc.)*) 
18563  401 
Keep of bool > state > unit  (*peek at state*) 
18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

402 
Transaction of bool * (bool > node > node); (*node transaction*) 
6689  403 

15531  404 
fun undo_limit int = if int then NONE else SOME 0; 
6689  405 

406 
local 

5828  407 

6689  408 
fun apply_tr _ Reset _ = toplevel 
15531  409 
 apply_tr int (Init (f, term)) (State NONE) = 
410 
State (SOME (History.init (undo_limit int) (f int), term)) 

411 
 apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF 

412 
 apply_tr _ Exit (State NONE) = raise UNDEF 

413 
 apply_tr _ Exit (State (SOME (node, (exit, _)))) = 

414 
(exit (History.current node); State NONE) 

415 
 apply_tr _ Kill (State NONE) = raise UNDEF 

416 
 apply_tr _ Kill (State (SOME (node, (_, kill)))) = 

417 
(kill (History.current node); State NONE) 

418 
 apply_tr _ (History _) (State NONE) = raise UNDEF 

419 
 apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) 

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

420 
 apply_tr int (Keep f) state = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

421 
controlled_execution (fn x => tap (f int) x) state 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

422 
 apply_tr _ (Transaction _) (State NONE) = raise UNDEF 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

423 
 apply_tr int (Transaction (hist, f)) (State (SOME state)) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

424 
transaction hist (fn x => f int x) state; 
5828  425 

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

18685  428 
apply_tr int tr state 
6689  429 
handle UNDEF => apply_union int trs state 
430 
 FAILURE (alt_state, UNDEF) => apply_union int trs alt_state 

431 
 exn as FAILURE _ => raise exn 

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

433 

434 
in 

435 

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

6689  438 

439 
end; 

5828  440 

441 

442 
(* datatype transition *) 

443 

444 
datatype transition = Transition of 

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

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

448 
int_only: bool, (*interactiveonly*) 

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

450 
no_timing: bool, (*suppress timing*) 

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

5828  452 

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

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

5828  456 

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

5828  459 

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

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

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

5828  464 

465 

466 
(* diagnostics *) 

467 

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

469 

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

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

472 

473 
fun type_error tr state = 

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

476 

477 
(* modify transitions *) 

478 

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

5828  481 

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

9010  484 

14923  485 
fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => 
15531  486 
(name, pos, SOME src, int_only, print, no_timing, trans)); 
5828  487 

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

490 

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

493 

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

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

496 

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

499 

500 
val print = print' ""; 

5828  501 

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

5828  504 

505 

21007  506 
(* basic transitions *) 
5828  507 

508 
val reset = add_trans Reset; 

6689  509 
fun init f exit kill = add_trans (Init (f, (exit, kill))); 
510 
val exit = add_trans Exit; 

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 

6689  520 
fun init_theory f exit kill = 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

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

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

523 
(fn Theory (Context.Theory thy, _) => kill thy  _ => raise UNDEF); 
5828  524 

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

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

15668  528 

21007  529 

530 
(* theory transitions *) 

15668  531 

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

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

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

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

535 

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

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

537 

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

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

540 
let 
20985  541 
val lthy = f thy; 
21294  542 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
543 
in Theory (gthy, SOME lthy) end 

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

544 
 _ => raise UNDEF)); 
17076  545 

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

21007  548 
 _ => raise UNDEF)); 
549 

550 
local 

551 

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

552 
fun local_theory_presentation loc f g = app_current (fn int => 
21294  553 
(fn Theory (gthy, _) => 
554 
let 

555 
val finish = loc_finish loc gthy; 

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

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

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

558 
 _ => raise UNDEF) #> tap (g int)); 
15668  559 

21007  560 
in 
561 

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

562 
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

563 
fun present_local_theory loc g = local_theory_presentation loc I g; 
18955  564 

21007  565 
end; 
566 

567 

568 
(* proof transitions *) 

569 

570 
fun end_proof f = map_current (fn int => 

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

572 
let val state = ProofHistory.current prf in 

573 
if can (Proof.assert_bottom true) state then 

574 
let 

575 
val ctxt' = f int state; 

576 
val gthy' = finish ctxt'; 

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

578 
else raise UNDEF 

579 
end 

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

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

582 
 _ => raise UNDEF)); 

583 

21294  584 
local 
585 

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

587 
(fn Theory (gthy, _) => 

588 
let 

589 
val prf = init gthy; 

590 
val schematic = Proof.schematic_goal prf; 

591 
in 

592 
if ! skip_proofs andalso schematic then 

593 
warning "Cannot skip proof of schematic goal statement" 

594 
else (); 

595 
if ! skip_proofs andalso not schematic then 

596 
SkipProof 

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

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

599 
end 

600 
 _ => raise UNDEF)); 

601 

602 
in 

603 

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

605 

606 
fun theory_to_proof f = begin_proof 

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

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

609 

610 
end; 

611 

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

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

615 
 _ => raise UNDEF)); 

616 

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

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

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

621 

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

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

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

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

627 
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

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

631 
fun actual_proof f = map_current (fn _ => 

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

633 
 _ => raise UNDEF)); 
16815  634 

635 
fun skip_proof f = map_current (fn _ => 

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

16815  639 
fun skip_proof_to_theory p = map_current (fn _ => 
21007  640 
(fn SkipProof (h, (gthy, _)) => 
641 
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

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

643 
 _ => raise UNDEF)); 
5828  644 

645 

646 

647 
(** toplevel transactions **) 

648 

649 
(* apply transitions *) 

650 

6664  651 
local 
652 

9010  653 
fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = 
5828  654 
let 
16682  655 
val _ = conditional (not int andalso int_only) (fn () => 
656 
warning (command_msg "Interactiveonly " tr)); 

657 

18685  658 
fun do_timing f x = (Output.info (command_msg "" tr); timeap f x); 
16682  659 
fun do_profiling f x = profile (! profiling) f x; 
660 

6689  661 
val (result, opt_exn) = 
16729  662 
state > (apply_trans int trans 
663 
> (if ! profiling > 0 then do_profiling else I) 

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

16607  665 
val _ = conditional (int andalso not (! quiet) andalso 
20664  666 
exists (member (op =) print) ("" :: ! print_mode)) 
16607  667 
(fn () => print_state false result); 
15570  668 
in (result, Option.map (fn UNDEF => type_error tr state  exn => exn) opt_exn) end; 
6664  669 

670 
in 

5828  671 

6689  672 
fun apply int tr st = 
6965  673 
(case app int tr st of 
15531  674 
(_, SOME TERMINATE) => NONE 
675 
 (_, SOME RESTART) => SOME (toplevel, NONE) 

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

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

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

6664  679 

680 
end; 

5828  681 

682 

17076  683 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  684 

6664  685 
local 
686 

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

689 
(case apply (! interact) tr st of 
15531  690 
SOME (st', NONE) => 
18685  691 
excur trs (st', pr st st' res handle exn => 
10324  692 
raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) 
15531  693 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 
694 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

5828  695 

17076  696 
fun no_pr _ _ _ = (); 
697 

6664  698 
in 
699 

17076  700 
fun present_excursion trs res = 
15531  701 
(case excur trs (State NONE, res) of 
702 
(State NONE, res') => res' 

18685  703 
 _ => error "Unfinished development at end of input") 
9134  704 
handle exn => error (exn_message exn); 
705 

17076  706 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  707 

6664  708 
end; 
709 

5828  710 

711 

712 
(** interactive transformations **) 

713 

714 
(* the global state reference *) 

715 

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

15531  718 
fun set_state state = global_state := (state, NONE); 
5828  719 
fun get_state () = fst (! global_state); 
720 
fun exn () = snd (! global_state); 

721 

722 

6965  723 
(* the Isar source of transitions *) 
724 

14091  725 
type 'a isar = 
6965  726 
(transition, (transition option, 
12881  727 
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, 
14091  728 
Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) 
12881  729 
Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; 
6965  730 

731 

5828  732 
(* apply transformers to global state *) 
733 

14985  734 
nonfix >> >>>; 
5828  735 

736 
fun >> tr = 

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

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

5828  740 
(global_state := (state', exn_info); 
16729  741 
print_exn exn_info; 
5828  742 
true)); 
743 

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

746 

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

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

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

20928  750 
fun warn_secure () = 
751 
let val secure = Secure.is_secure () 

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

753 

5828  754 
fun raw_loop src = 
7602  755 
(case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of 
15531  756 
NONE => (writeln "\nInterrupt."; raw_loop src) 
20928  757 
 SOME NONE => if warn_secure () then quit () else () 
758 
 SOME (SOME (tr, src')) => 

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

760 
else ()); 

5828  761 

12987  762 
fun loop src = ignore_interrupt raw_loop src; 
5828  763 

764 
end; 