author  wenzelm 
Fri, 14 Jul 2006 14:19:48 +0200  
changeset 20128  8f0e07d7cf92 
parent 19996  a4332e71c1de 
child 20363  f34c5dbe74d5 
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 
18589  11 
type node 
12 
val theory_node: node > theory option 

13 
val proof_node: node > ProofHistory.T option 

19063  14 
val cases_node: (theory > 'a) > (Proof.state > 'a) > node > 'a 
15 
val body_context_node: node option > xstring option > Proof.context 

5828  16 
type state 
17 
val toplevel: 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 
17266  22 
val assert: bool > unit 
6689  23 
val node_history_of: state > node History.T 
5828  24 
val node_of: state > node 
6664  25 
val node_case: (theory > 'a) > (Proof.state > 'a) > state > 'a 
18641  26 
val context_of: state > Context.generic 
5828  27 
val theory_of: state > theory 
28 
val proof_of: state > Proof.state 

18589  29 
val proof_position_of: state > int 
9453  30 
val enter_forward_proof: state > Proof.state 
16815  31 
val prompt_state_default: state > string 
32 
val prompt_state_fn: (state > string) ref 

33 
val print_state_context: state > unit 

34 
val print_state_default: bool > state > unit 

35 
val print_state_hook: (bool > state > unit) > 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 
18589  49 
val checkpoint: state > state 
50 
val copy: state > state 

16682  51 
type transition 
6689  52 
val undo_limit: bool > int option 
5828  53 
val empty: transition 
14923  54 
val name_of: transition > string 
55 
val source_of: transition > OuterLex.token list option 

5828  56 
val name: string > transition > transition 
57 
val position: Position.T > transition > transition 

14923  58 
val source: OuterLex.token list > transition > transition 
5828  59 
val interactive: bool > transition > transition 
60 
val print: transition > transition 

16607  61 
val print': string > transition > transition 
17363  62 
val three_buffersN: string 
63 
val print3: transition > transition 

9010  64 
val no_timing: transition > transition 
5828  65 
val reset: transition > transition 
8465  66 
val init: (bool > node) > (node > unit) > (node > unit) > transition > transition 
6689  67 
val exit: transition > transition 
68 
val kill: transition > transition 

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

69 
val history: (node History.T > node History.T) > transition > transition 
5828  70 
val keep: (state > unit) > transition > transition 
7612  71 
val keep': (bool > state > unit) > transition > transition 
5828  72 
val imperative: (unit > unit) > transition > transition 
7105  73 
val init_theory: (bool > theory) > (theory > unit) > (theory > unit) 
6689  74 
> transition > transition 
5828  75 
val theory: (theory > theory) > transition > transition 
7612  76 
val theory': (bool > theory > theory) > transition > transition 
18811  77 
val theory_context: (theory > Proof.context * theory) > transition > transition 
19063  78 
val local_theory: xstring option > (local_theory > local_theory) > 
79 
transition > transition 

17363  80 
val theory_to_proof: (theory > Proof.state) > transition > transition 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

81 
val proof: (Proof.state > Proof.state) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

82 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

83 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

84 
val proofs': (bool > Proof.state > Proof.state Seq.seq) > transition > transition 
16815  85 
val actual_proof: (ProofHistory.T > ProofHistory.T) > transition > transition 
86 
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

87 
val proof_to_theory: (Proof.state > theory) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

88 
val proof_to_theory': (bool > Proof.state > theory) > transition > transition 
18811  89 
val proof_to_theory_context: (bool > Proof.state > Proof.context * theory) 
17076  90 
> 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 
18563  92 
val forget_proof: transition > transition 
19063  93 
val present_local_theory: xstring option > (bool > node > unit) > transition > transition 
94 
val present_proof: (bool > node > unit) > transition > transition 

9512  95 
val unknown_theory: transition > transition 
96 
val unknown_proof: transition > transition 

97 
val unknown_context: transition > transition 

5828  98 
val apply: bool > transition > state > (state * (exn * string) option) option 
17076  99 
val present_excursion: (transition * (state > state > 'a > 'a)) list > 'a > 'a 
5828  100 
val excursion: transition list > unit 
101 
val set_state: state > unit 

102 
val get_state: unit > state 

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

104 
val >> : transition > bool 

14985  105 
val >>> : transition list > unit 
14091  106 
type 'a isar 
107 
val loop: 'a isar > unit 

5828  108 
end; 
109 

6965  110 
structure Toplevel: TOPLEVEL = 
5828  111 
struct 
112 

113 

114 
(** toplevel state **) 

115 

19063  116 
exception UNDEF; 
117 

118 

16815  119 
(* datatype state *) 
5828  120 

121 
datatype node = 

18563  122 
Theory of theory * Proof.context option  (*theory with optional body context*) 
123 
Proof of ProofHistory.T * theory  (*history of proof states, original theory*) 

124 
SkipProof of (int History.T * theory) * theory; 

125 
(*history of proof depths, resulting theory, original theory*) 

5828  126 

18589  127 
val theory_node = fn Theory (thy, _) => SOME thy  _ => NONE; 
128 
val proof_node = fn Proof (prf, _) => SOME prf  _ => NONE; 

129 

19063  130 
fun cases_node f _ (Theory (thy, _)) = f thy 
131 
 cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf) 

132 
 cases_node f _ (SkipProof ((_, thy), _)) = f thy; 

133 

134 
fun body_context_node (SOME (Theory (_, SOME ctxt))) NONE = ctxt 

135 
 body_context_node (SOME node) loc = 

136 
node > cases_node (LocalTheory.init loc) 

137 
(if is_some loc then LocalTheory.init loc o Proof.theory_of 

138 
else Proof.context_of) 

139 
 body_context_node NONE _ = raise UNDEF; 

140 

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

15531  143 
val toplevel = State NONE; 
5828  144 

15531  145 
fun is_toplevel (State NONE) = true 
7732  146 
 is_toplevel _ = false; 
147 

17076  148 
fun level (State NONE) = 0 
149 
 level (State (SOME (node, _))) = 

150 
(case History.current node of 

151 
Theory _ => 0 

18563  152 
 Proof (prf, _) => Proof.level (ProofHistory.current prf) 
153 
 SkipProof ((h, _), _) => History.current h + 1); (*different notion of proof depth!*) 

17076  154 

15531  155 
fun str_of_state (State NONE) = "at top level" 
16815  156 
 str_of_state (State (SOME (node, _))) = 
157 
(case History.current node of 

158 
Theory _ => "in theory mode" 

159 
 Proof _ => "in proof mode" 

160 
 SkipProof _ => "in skipped proof mode"); 

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

161 

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

162 

5828  163 
(* top node *) 
164 

17266  165 
fun assert true = () 
166 
 assert false = raise UNDEF; 

167 

15531  168 
fun node_history_of (State NONE) = raise UNDEF 
169 
 node_history_of (State (SOME (node, _))) = node; 

6689  170 

171 
val node_of = History.current o node_history_of; 

5828  172 

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

175 

19063  176 
fun node_case f g state = cases_node f g (node_of state); 
5828  177 

18641  178 
val context_of = node_case Context.Theory (Context.Proof o Proof.context_of); 
6664  179 
val theory_of = node_case I Proof.theory_of; 
18589  180 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  181 

18589  182 
fun proof_position_of state = 
183 
(case node_of state of 

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

185 
 _ => raise UNDEF); 

6664  186 

17363  187 
val enter_forward_proof = node_case (Proof.init o ProofContext.init) Proof.enter_forward; 
5828  188 

189 

16815  190 
(* prompt state *) 
191 

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

193 

194 
val prompt_state_fn = ref prompt_state_default; 

195 
fun prompt_state state = ! prompt_state_fn state; 

196 

197 

198 
(* print state *) 

199 

200 
fun pretty_context thy = [Pretty.block 

201 
[Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy), 

202 
Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]; 

203 

204 
fun pretty_state_context state = 

205 
(case try theory_of state of NONE => [] 

206 
 SOME thy => pretty_context thy); 

207 

17076  208 
fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy 
18563  209 
 pretty_node _ (Proof (prf, _)) = 
16815  210 
Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf) 
18563  211 
 pretty_node _ (SkipProof ((h, _), _)) = 
16815  212 
[Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))]; 
213 

214 
fun pretty_state prf_only state = 

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

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

217 
 SOME node => 

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

219 
pretty_node prf_only node @ 

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

221 
end; 

222 

223 
val print_state_context = Pretty.writelns o pretty_state_context; 

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

225 

226 
val print_state_hooks = ref ([]: (bool > state > unit) list); 

227 
fun print_state_hook f = change print_state_hooks (cons f); 

228 
val print_state_fn = ref print_state_default; 

229 

230 
fun print_state prf_only state = 

231 
(List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks); 

232 
! print_state_fn prf_only state); 

233 

234 

15668  235 

5828  236 
(** toplevel transitions **) 
237 

16682  238 
val quiet = ref false; 
239 
val debug = ref false; 

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

240 
val interact = ref false; 
16682  241 
val timing = Output.timing; 
242 
val profiling = ref 0; 

16815  243 
val skip_proofs = ref false; 
16682  244 

5828  245 
exception TERMINATE; 
5990  246 
exception RESTART; 
7022  247 
exception EXCURSION_FAIL of exn * string; 
6689  248 
exception FAILURE of state * exn; 
5828  249 

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

250 

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

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

252 

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

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

254 

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

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

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

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

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

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

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

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

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

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

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

269 
 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

270 
 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

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

272 
 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

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

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

275 
 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

276 
 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

277 
 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

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

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

280 
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

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

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

283 
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

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

285 
 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

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

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

288 
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

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

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

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

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

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

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

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

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

297 

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

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

299 

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

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

301 

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

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

303 
 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

304 

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

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

306 

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

311 

18685  312 
fun debugging f x = 
313 
if ! debug then 

314 
setmp Library.do_transform_failure false 

315 
exception_trace (fn () => f x) 

316 
else f x; 

317 

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

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

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

320 
in raise_interrupt (fn () => y := f x) (); ! y end; 
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 
in 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

323 

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

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

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

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

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

328 
> setmp Output.do_toplevel_errors false; 
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 
fun program f = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

331 
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

332 

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

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

334 

5828  335 

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

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

6689  340 
local 
341 

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

18685  344 
val stale_theory = ERROR "Stale theory encountered after succesful execution!"; 
16815  345 

19101  346 
fun checkpoint_node (Theory (thy, _)) = Theory (Theory.checkpoint thy, NONE) 
18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

347 
 checkpoint_node node = node; 
6689  348 

19101  349 
fun copy_node (Theory (thy, _)) = Theory (Theory.copy thy, NONE) 
18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

350 
 copy_node node = node; 
6689  351 

15531  352 
fun return (result, NONE) = result 
353 
 return (result, SOME exn) = raise FAILURE (result, exn); 

7022  354 

6689  355 
in 
356 

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

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

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

359 
val cont_node = History.map checkpoint_node node; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

360 
val back_node = History.map copy_node cont_node; 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

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

363 
fun error_state nd exn = (state nd, SOME exn); 
6689  364 

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

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

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

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

368 
> (if hist then History.apply_copy copy_node else History.map) 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

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

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

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

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

374 
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

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

376 
end; 
6689  377 

18589  378 
fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term)) 
379 
 mapping _ state = state; 

380 

18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

381 
val checkpoint = mapping checkpoint_node; 
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

382 
val copy = mapping copy_node; 
18589  383 

6689  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 

506 
(* build transitions *) 

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 = 
17076  521 
init (fn int => Theory (f int, NONE)) 
522 
(fn Theory (thy, _) => exit thy  _ => raise UNDEF) 

523 
(fn Theory (thy, _) => kill thy  _ => raise UNDEF); 

5828  524 

15668  525 

526 
(* typed transitions *) 

527 

18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

528 
fun theory f = app_current 
18563  529 
(K (fn Theory (thy, _) => Theory (f thy, NONE)  _ => raise UNDEF)); 
530 

18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

531 
fun theory' f = app_current (fn int => 
17076  532 
(fn Theory (thy, _) => Theory (f int thy, NONE)  _ => raise UNDEF)); 
533 

18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

534 
fun theory_context f = app_current 
18811  535 
(K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy)))  _ => raise UNDEF)); 
15668  536 

19063  537 
fun local_theory loc f = theory_context (LocalTheory.mapping loc f); 
18955  538 

18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

539 
fun theory_to_proof f = app_current (fn int => 
17076  540 
(fn Theory (thy, _) => 
19996
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

541 
let 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

542 
val prf = f thy; 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

543 
val schematic = Proof.schematic_goal prf; 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

544 
in 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

545 
if ! skip_proofs andalso schematic then 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

546 
warning "Cannot skip proof of schematic goal statement" 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

547 
else (); 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

548 
if ! skip_proofs andalso not schematic then 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

549 
SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy) 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

550 
else Proof (ProofHistory.init (undo_limit int) prf, thy) 
a4332e71c1de
skip_proofs: do not skip proofs of schematic goals (warning);
wenzelm
parents:
19841
diff
changeset

551 
end 
18592
451d622bb4a9
transactions now always see quasifunctional intermediate checkpoint;
wenzelm
parents:
18589
diff
changeset

552 
 _ => raise UNDEF)); 
18563  553 

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

554 
fun proofs' f = map_current (fn int => 
18563  555 
(fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy) 
556 
 SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy) 

16815  557 
 _ => raise UNDEF)); 
15668  558 

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

559 
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

560 
val proofs = proofs' o K; 
6689  561 
val proof = proof' o K; 
16815  562 

563 
fun actual_proof f = map_current (fn _ => 

18563  564 
(fn Proof (prf, orig_thy) => Proof (f prf, orig_thy)  _ => raise UNDEF)); 
16815  565 

566 
fun skip_proof f = map_current (fn _ => 

18563  567 
(fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy)  _ => raise UNDEF)); 
15668  568 

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

569 
fun end_proof f = map_current (fn int => 
18563  570 
(fn Proof (prf, _) => Theory (f int (ProofHistory.current prf)) 
571 
 SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF 

572 
 _ => raise UNDEF)); 

573 

574 
val forget_proof = map_current (fn _ => 

575 
(fn Proof (_, orig_thy) => Theory (orig_thy, NONE) 

576 
 SkipProof (_, orig_thy) => Theory (orig_thy, NONE) 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
14985
diff
changeset

577 
 _ => raise UNDEF)); 
15668  578 

17076  579 
fun proof_to_theory' f = end_proof (rpair NONE oo f); 
580 
fun proof_to_theory f = proof_to_theory' (K f); 

18811  581 
fun proof_to_theory_context f = end_proof ((swap o apfst SOME) oo f); 
15668  582 

16815  583 
fun skip_proof_to_theory p = map_current (fn _ => 
18563  584 
(fn SkipProof ((h, thy), _) => 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

585 
if p (History.current h) then Theory (thy, NONE) 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

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

587 
 _ => raise UNDEF)); 
5828  588 

19063  589 
fun present_local_theory loc f = app_current (fn int => 
590 
(fn Theory (thy, _) => Theory (swap (apfst SOME (LocalTheory.mapping loc I thy))) 

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

592 

593 
fun present_proof f = map_current (fn int => 

594 
(fn node as Proof _ => node  _ => raise UNDEF) #> tap (f int)); 

595 

9512  596 
val unknown_theory = imperative (fn () => warning "Unknown theory context"); 
597 
val unknown_proof = imperative (fn () => warning "Unknown proof context"); 

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

599 

5828  600 

601 

602 
(** toplevel transactions **) 

603 

604 
(* apply transitions *) 

605 

6664  606 
local 
607 

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

612 

18685  613 
fun do_timing f x = (Output.info (command_msg "" tr); timeap f x); 
16682  614 
fun do_profiling f x = profile (! profiling) f x; 
615 

6689  616 
val (result, opt_exn) = 
16729  617 
state > (apply_trans int trans 
618 
> (if ! profiling > 0 then do_profiling else I) 

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

16607  620 
val _ = conditional (int andalso not (! quiet) andalso 
621 
exists (fn m => m mem_string print) ("" :: ! print_mode)) 

622 
(fn () => print_state false result); 

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

625 
in 

5828  626 

6689  627 
fun apply int tr st = 
6965  628 
(case app int tr st of 
15531  629 
(_, SOME TERMINATE) => NONE 
630 
 (_, SOME RESTART) => SOME (toplevel, NONE) 

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

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

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

6664  634 

635 
end; 

5828  636 

637 

17076  638 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  639 

6664  640 
local 
641 

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

644 
(case apply (! interact) tr st of 
15531  645 
SOME (st', NONE) => 
18685  646 
excur trs (st', pr st st' res handle exn => 
10324  647 
raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) 
15531  648 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 
649 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

5828  650 

17076  651 
fun no_pr _ _ _ = (); 
652 

6664  653 
in 
654 

17076  655 
fun present_excursion trs res = 
15531  656 
(case excur trs (State NONE, res) of 
657 
(State NONE, res') => res' 

18685  658 
 _ => error "Unfinished development at end of input") 
9134  659 
handle exn => error (exn_message exn); 
660 

17076  661 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  662 

6664  663 
end; 
664 

5828  665 

666 

667 
(** interactive transformations **) 

668 

669 
(* the global state reference *) 

670 

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

15531  673 
fun set_state state = global_state := (state, NONE); 
5828  674 
fun get_state () = fst (! global_state); 
675 
fun exn () = snd (! global_state); 

676 

677 

6965  678 
(* the Isar source of transitions *) 
679 

14091  680 
type 'a isar = 
6965  681 
(transition, (transition option, 
12881  682 
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, 
14091  683 
Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) 
12881  684 
Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; 
6965  685 

686 

5828  687 
(* apply transformers to global state *) 
688 

14985  689 
nonfix >> >>>; 
5828  690 

691 
fun >> tr = 

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

15531  693 
NONE => false 
694 
 SOME (state', exn_info) => 

5828  695 
(global_state := (state', exn_info); 
16729  696 
print_exn exn_info; 
5828  697 
true)); 
698 

14985  699 
fun >>> [] = () 
700 
 >>> (tr :: trs) = if >> tr then >>> trs else (); 

701 

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

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

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

5828  705 
fun raw_loop src = 
7602  706 
(case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of 
15531  707 
NONE => (writeln "\nInterrupt."; raw_loop src) 
708 
 SOME NONE => () 

709 
 SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ()); 

5828  710 

12987  711 
fun loop src = ignore_interrupt raw_loop src; 
5828  712 

713 
end; 