author  wenzelm 
Sun, 18 Nov 2007 16:10:11 +0100  
changeset 25441  4028958d19ff 
parent 25292  f082e59551b0 
child 25527  330ca6e1dca8 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
The Isabelle/Isar toplevel. 

6 
*) 

7 

8 
signature TOPLEVEL = 

9 
sig 

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

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

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

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

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

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

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

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

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

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

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

16815  38 
val skip_proofs: bool ref 
5828  39 
exception TERMINATE 
5990  40 
exception RESTART 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

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

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

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

5828  49 
val name: string > transition > transition 
50 
val position: Position.T > transition > transition 

14923  51 
val source: OuterLex.token list > transition > transition 
5828  52 
val interactive: bool > transition > transition 
53 
val print: transition > transition 

16607  54 
val print': string > transition > transition 
17363  55 
val three_buffersN: string 
56 
val print3: transition > transition 

9010  57 
val no_timing: transition > transition 
22056  58 
val init_theory: (bool > theory) > (theory > unit) > (theory > unit) > 
59 
transition > transition 

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

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

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

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

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

72 
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

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

21007  76 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
77 
transition > transition 

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

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

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

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

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

91 
val unknown_context: transition > transition 

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

95 
val get_state: unit > state 

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

97 
val >> : transition > bool 

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

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

5828  102 
end; 
103 

6965  104 
structure Toplevel: TOPLEVEL = 
5828  105 
struct 
106 

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

107 

5828  108 
(** toplevel state **) 
109 

19063  110 
exception UNDEF; 
111 

112 

21294  113 
(* local theory wrappers *) 
5828  114 

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

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

116 

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

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

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

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

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

21294  128 

129 

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

130 
(* datatype node *) 
21294  131 

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

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

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

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

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

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

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

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

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

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

148 
 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

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

151 
 presentation_context NONE _ = raise UNDEF; 
19063  152 

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

153 

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

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

155 

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

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

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

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

160 
State of state_info; 
5828  161 

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

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

163 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

181 

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

182 

5828  183 
(* top node *) 
184 

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

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

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

188 
val node_of = History.current o node_history_of; 

5828  189 

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

192 

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

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

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

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

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

203 
 _ => raise UNDEF); 

6664  204 

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

207 

16815  208 
(* print state *) 
209 

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

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

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

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

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

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

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

218 
> Pretty.chunks > Pretty.writeln; 
16815  219 

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

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

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

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

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

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

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

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

16815  229 

230 

15668  231 

5828  232 
(** toplevel transitions **) 
233 

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

236 
val interact = ref false; 
16682  237 
val timing = Output.timing; 
238 
val profiling = ref 0; 

16815  239 
val skip_proofs = ref false; 
16682  240 

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

245 
exception TOPLEVEL_ERROR; 
5828  246 

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

247 

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

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

249 

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

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

251 

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

252 
fun with_context f xs = 
22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
22089
diff
changeset

253 
(case ML_Context.get_context () of NONE => [] 
22089  254 
 SOME context => map (f (Context.proof_of context)) xs); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

255 

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

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

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

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

259 

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

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

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

262 
 exn_msg _ Interrupt = "Interrupt." 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

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

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

265 
 exn_msg _ (ERROR msg) = msg 
23975  266 
 exn_msg detailed (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg detailed) exns) 
23963
c2ee97a963db
moved exception capture/release to structure Exn;
wenzelm
parents:
23940
diff
changeset

267 
 exn_msg detailed (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg detailed) exns @ [msg]) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

268 
 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

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

270 
 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

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

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

273 
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

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

275 
 exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: 
24920  276 
with_context Syntax.string_of_typ Ts @ with_context Syntax.string_of_term ts) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

277 
 exn_msg false (TERM (msg, _)) = raised "TERM" [msg] 
22089  278 
 exn_msg true (TERM (msg, ts)) = 
24920  279 
raised "TERM" (msg :: with_context Syntax.string_of_term ts) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

281 
 exn_msg true (THM (msg, i, thms)) = 
22089  282 
raised ("THM " ^ string_of_int i) (msg :: with_context ProofContext.string_of_thm thms) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

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

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

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

287 
 exn_msg _ (Fail msg) = raised "Fail" [msg] 
23940  288 
 exn_msg _ exn = General.exnMessage exn; 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

289 

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

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

291 

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

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

293 

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

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

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

296 

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

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

298 

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

303 

18685  304 
fun debugging f x = 
23940  305 
if ! debug then exception_trace (fn () => f x) 
18685  306 
else f x; 
307 

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

308 
fun interruptible f x = 
25219  309 
let val y = ref NONE 
310 
in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end; 

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

311 

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

312 
fun toplevel_error f x = f x 
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

313 
handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR); 
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

314 

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

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

316 

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

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

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

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

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

321 

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

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

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

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

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

326 

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

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

328 

5828  329 

16815  330 
(* node transactions and recovery from stale theories *) 
6689  331 

16815  332 
(*NB: proof commands should be nondestructive!*) 
7022  333 

6689  334 
local 
335 

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

18685  338 
val stale_theory = ERROR "Stale theory encountered after succesful execution!"; 
16815  339 

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

340 
fun map_theory f = History.map_current 
21177  341 
(fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE) 
342 
 node => node); 

6689  343 

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

344 
fun context_position pos = History.map_current 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

345 
(fn Theory (gthy, ctxt) => Theory (ContextPosition.put pos gthy, ctxt) 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

346 
 Proof (prf, x) => 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

347 
Proof (ProofHistory.map_current (Proof.map_context (ContextPosition.put_ctxt pos)) prf, x) 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

348 
 node => node); 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

349 

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

7022  352 

6689  353 
in 
354 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

375 
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

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

377 
end; 
6689  378 

379 
end; 

380 

381 

382 
(* primitive transitions *) 

383 

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

387 
Transaction.*) 

5828  388 

389 
datatype trans = 

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

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

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

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

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

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

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

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

398 
Transaction of bool * (bool > node > node); (*node transaction*) 
6689  399 

15531  400 
fun undo_limit int = if int then NONE else SOME 0; 
6689  401 

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

25219  404 
SOME thy => controlled_execution exit thy 
22056  405 
 NONE => ()) 
406 
 safe_exit _ = (); 

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

407 

6689  408 
local 
5828  409 

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

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

411 

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

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

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

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

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

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

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

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

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

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

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

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

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

427 
 apply_tr _ _ _ _ = raise UNDEF; 
5828  428 

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

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

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

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

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

433 
 FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state 
6689  434 
 exn as FAILURE _ => raise exn 
435 
 exn => raise FAILURE (state, exn); 

436 

437 
in 

438 

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

439 
fun apply_trans int pos trs state = (apply_union int pos trs state, NONE) 
15531  440 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  441 

442 
end; 

5828  443 

444 

445 
(* datatype transition *) 

446 

447 
datatype transition = Transition of 

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

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

451 
int_only: bool, (*interactiveonly*) 

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

453 
no_timing: bool, (*suppress timing*) 

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

5828  455 

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

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

5828  459 

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

5828  462 

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

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

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

5828  467 

468 

469 
(* diagnostics *) 

470 

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

472 

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

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

475 

476 
fun type_error tr state = 

18685  477 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  478 

479 

480 
(* modify transitions *) 

481 

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

5828  484 

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

9010  487 

14923  488 
fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => 
15531  489 
(name, pos, SOME src, int_only, print, no_timing, trans)); 
5828  490 

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

493 

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

496 

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

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

499 

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

502 

503 
val print = print' ""; 

5828  504 

17363  505 
val three_buffersN = "three_buffers"; 
506 
val print3 = print' three_buffersN; 

5828  507 

508 

21007  509 
(* basic transitions *) 
5828  510 

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

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

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

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

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

519 
fun app_current f = add_trans (Transaction (true, f)); 
5828  520 

7612  521 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  522 
fun imperative f = keep (fn _ => f ()); 
523 

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

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

15668  527 

21007  528 

529 
(* theory transitions *) 

15668  530 

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

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

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

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

534 

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

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

536 

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

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

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

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

543 
 _ => raise UNDEF)); 
17076  544 

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

21007  547 
 _ => raise UNDEF)); 
548 

549 
local 

550 

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

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

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

554 
val pos = ContextPosition.get (Context.proof_of gthy); 
21294  555 
val finish = loc_finish loc gthy; 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

556 
val lthy' = f (ContextPosition.put_ctxt pos (loc_begin loc gthy)); 
21294  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 => 

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

571 
(fn Proof (prf, (finish, _)) => 
21007  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 

24453  589 
val prf = init int gthy; 
21294  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 

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

604 
fun local_theory_to_proof' loc f = begin_proof 
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

605 
(fn int => fn gthy => 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

606 
f int (ContextPosition.put_ctxt (ContextPosition.get (Context.proof_of gthy)) 
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

607 
(loc_begin loc gthy))) 
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

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

609 

24453  610 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  611 

612 
fun theory_to_proof f = begin_proof 

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

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

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

616 
end; 

617 

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

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

621 
 _ => raise UNDEF)); 

622 

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

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

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

627 

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

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

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

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

633 
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

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

637 
fun actual_proof f = map_current (fn _ => 

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

639 
 _ => raise UNDEF)); 
16815  640 

641 
fun skip_proof f = map_current (fn _ => 

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

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

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

649 
 _ => raise UNDEF)); 
5828  650 

651 

652 

653 
(** toplevel transactions **) 

654 

655 
(* apply transitions *) 

656 

6664  657 
local 
658 

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

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

663 
else (); 

16682  664 

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

6689  668 
val (result, opt_exn) = 
23363
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

669 
state > (apply_trans int pos trans 
23428  670 
> (if ! profiling > 0 andalso not no_timing then do_profiling else I) 
16729  671 
> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); 
21962  672 
val _ = 
24634  673 
if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ()) 
21962  674 
then print_state false result else (); 
15570  675 
in (result, Option.map (fn UNDEF => type_error tr state  exn => exn) opt_exn) end; 
6664  676 

677 
in 

5828  678 

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

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

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

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

6664  686 

687 
end; 

5828  688 

689 

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

6664  692 
local 
693 

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

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

5828  702 

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

6664  705 
in 
706 

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

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

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

6664  715 
end; 
716 

5828  717 

718 

719 
(** interactive transformations **) 

720 

721 
(* the global state reference *) 

722 

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

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

728 

729 

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

730 
(* apply transformers to global state  NOT THREADSAFE! *) 
5828  731 

14985  732 
nonfix >> >>>; 
5828  733 

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

734 
fun >> tr = 
5828  735 
(case apply true tr (get_state ()) of 
15531  736 
NONE => false 
737 
 SOME (state', exn_info) => 

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

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

740 
true)); 
5828  741 

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

744 

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

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

746 

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

747 

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

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

749 

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

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

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

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

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

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

755 

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

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

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

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

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

762 

5828  763 
fun raw_loop src = 
23720  764 
let val prompt = Output.escape (Markup.enclose Markup.prompt Source.default_prompt) in 
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

765 
(case get_interrupt (Source.set_prompt prompt src) of 
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

766 
NONE => (writeln "\nInterrupt."; raw_loop src) 
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

767 
 SOME NONE => if warn_secure () then quit () else () 
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

768 
 SOME (SOME (tr, src')) => 
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

769 
if >> tr orelse warn_secure () then raw_loop src' 
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

770 
else ()) 
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

771 
end; 
5828  772 

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

775 
end; 