author  wenzelm 
Wed, 07 Jan 2009 12:08:22 +0100  
changeset 29380  a9ee3475abf4 
parent 29343  43ac99cdeb5b 
child 29386  d5849935560c 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

4 
Isabelle/Isar toplevel transactions. 
5828  5 
*) 
6 

7 
signature TOPLEVEL = 

8 
sig 

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

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

12 
val theory_node: node > generic_theory option 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

13 
val proof_node: node > ProofNode.T option 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

14 
val cases_node: (generic_theory > 'a) > (Proof.state > 'a) > node > 'a 
29066  15 
val context_node: node > Proof.context 
20963
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 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

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

17076  22 
val level: state > int 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

23 
val previous_node_of: state > node option 
5828  24 
val node_of: state > node 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

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

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

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

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

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

16815  39 
val skip_proofs: bool ref 
5828  40 
exception TERMINATE 
27583  41 
exception TOPLEVEL_ERROR 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

42 
exception CONTEXT of Proof.context * exn 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

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

44 
val program: (unit > 'a) > 'a 
16682  45 
type transition 
5828  46 
val empty: transition 
27441  47 
val init_of: transition > string option 
27427  48 
val name_of: transition > string 
28105  49 
val pos_of: transition > Position.T 
27500  50 
val str_of: transition > string 
5828  51 
val name: string > transition > transition 
52 
val position: Position.T > transition > transition 

53 
val interactive: bool > transition > transition 

54 
val print: transition > transition 

9010  55 
val no_timing: transition > transition 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

56 
val init_theory: string > (bool > theory) > (theory > unit) > transition > transition 
6689  57 
val exit: transition > transition 
5828  58 
val keep: (state > unit) > transition > transition 
7612  59 
val keep': (bool > state > unit) > transition > transition 
5828  60 
val imperative: (unit > unit) > transition > transition 
27840  61 
val ignored: Position.T > transition 
62 
val malformed: Position.T > string > transition 

5828  63 
val theory: (theory > theory) > transition > transition 
26491  64 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  65 
val theory': (bool > theory > theory) > transition > transition 
20985  66 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  67 
val end_local_theory: transition > transition 
29380  68 
val local_theory': xstring option > (bool > local_theory > local_theory) > 
69 
transition > transition 

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

70 
val local_theory: xstring option > (local_theory > local_theory) > transition > transition 
27859  71 
val present_local_theory: xstring option > (node > unit) > transition > transition 
24453  72 
val local_theory_to_proof': xstring option > (bool > local_theory > Proof.state) > 
73 
transition > transition 

21007  74 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
75 
transition > transition 

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

27859  79 
val present_proof: (node > unit) > transition > transition 
21177  80 
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

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

27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

84 
val actual_proof: (ProofNode.T > ProofNode.T) > transition > transition 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

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

86 
val skip_proof_to_theory: (int > bool) > transition > transition 
27427  87 
val get_id: transition > string option 
88 
val put_id: string > transition > transition 

9512  89 
val unknown_theory: transition > transition 
90 
val unknown_proof: transition > transition 

91 
val unknown_context: transition > transition 

28425  92 
val setmp_thread_position: transition > ('a > 'b) > 'a > 'b 
27606  93 
val status: transition > Markup.T > unit 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

94 
val error_msg: transition > exn * string > unit 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

95 
val add_hook: (transition > state > state > unit) > unit 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

96 
val transition: bool > transition > state > (state * (exn * string) option) option 
28425  97 
val commit_exit: Position.T > transition 
98 
val command: transition > state > state 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

99 
val excursion: (transition * transition list) list > (transition * state) list * (unit > unit) 
5828  100 
end; 
101 

6965  102 
structure Toplevel: TOPLEVEL = 
5828  103 
struct 
104 

105 
(** toplevel state **) 

106 

19063  107 
exception UNDEF; 
108 

109 

21294  110 
(* local theory wrappers *) 
5828  111 

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

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

113 

25292  114 
val loc_init = TheoryTarget.context; 
28394  115 
val loc_exit = LocalTheory.exit_global; 
21294  116 

25292  117 
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "" loc) thy 
21294  118 
 loc_begin NONE (Context.Proof lthy) = lthy 
25269  119 
 loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); 
21294  120 

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

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

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

21294  125 

126 

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

127 
(* datatype node *) 
21294  128 

5828  129 
datatype node = 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

130 
Theory of generic_theory * Proof.context option 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

131 
(*theory with presentation context*)  
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

132 
Proof of ProofNode.T * ((Proof.context > generic_theory) * generic_theory) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

133 
(*proof node, finish, original theory*)  
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

134 
SkipProof of int * (generic_theory * generic_theory); 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

135 
(*proof depth, resulting theory, original theory*) 
5828  136 

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

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

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

141 
fun cases_node f _ (Theory (gthy, _)) = f gthy 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

142 
 cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf) 
21007  143 
 cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; 
19063  144 

29066  145 
val context_node = cases_node Context.proof_of Proof.context_of; 
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 
29066  148 
 presentation_context (SOME node) NONE = context_node node 
20963
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 

26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

153 
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

154 
 reset_presentation node = node; 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

155 

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

156 

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

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

158 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

159 
type node_info = node * (theory > unit); (*node with exit operation*) 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

160 
datatype state = State of node_info option * node_info option; (*current, previous*) 
5828  161 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

162 
val toplevel = State (NONE, NONE); 
5828  163 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

164 
fun is_toplevel (State (NONE, _)) = true 
7732  165 
 is_toplevel _ = false; 
166 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

167 
fun level (State (NONE, _)) = 0 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

168 
 level (State (SOME (Theory _, _), _)) = 0 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

169 
 level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

170 
 level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*) 
17076  171 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

172 
fun str_of_state (State (NONE, _)) = "at top level" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

173 
 str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

174 
 str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

175 
 str_of_state (State (SOME (Proof _, _), _)) = "in proof mode" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

176 
 str_of_state (State (SOME (SkipProof _, _), _)) = "in skipped proof mode"; 
5946
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

177 

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

178 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

179 
(* current node *) 
5828  180 

27603  181 
fun previous_node_of (State (_, prev)) = Option.map #1 prev; 
6689  182 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

183 
fun node_of (State (NONE, _)) = raise UNDEF 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

184 
 node_of (State (SOME (node, _), _)) = node; 
5828  185 

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

188 

19063  189 
fun node_case f g state = cases_node f g (node_of state); 
5828  190 

21506  191 
val context_of = node_case Context.proof_of Proof.context_of; 
22089  192 
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

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

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

27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

198 
Proof (prf, _) => ProofNode.position prf 
18589  199 
 _ => raise UNDEF); 
6664  200 

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

203 

16815  204 
(* print state *) 
205 

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

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

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

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

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

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

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

214 
> Pretty.chunks > Pretty.writeln; 
16815  215 

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

216 
fun print_state prf_only state = 
23701  217 
(case try node_of state of 
218 
NONE => [] 

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

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

27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

221 
Proof.pretty_state (ProofNode.position prf) (ProofNode.current prf) 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

222 
 SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) 
23701  223 
> Pretty.markup_chunks Markup.state > Pretty.writeln; 
16815  224 

225 

15668  226 

5828  227 
(** toplevel transitions **) 
228 

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

231 
val interact = ref false; 
16682  232 
val timing = Output.timing; 
233 
val profiling = ref 0; 

16815  234 
val skip_proofs = ref false; 
16682  235 

5828  236 
exception TERMINATE; 
7022  237 
exception EXCURSION_FAIL of exn * string; 
6689  238 
exception FAILURE of state * exn; 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

239 
exception TOPLEVEL_ERROR; 
5828  240 

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

241 

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

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

243 

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

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

245 

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

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

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

248 

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

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

250 

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

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

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

253 

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

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

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

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

257 

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

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

259 

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

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

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

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

263 

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

264 
fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn 
28458  265 
 exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) 
26293  266 
 exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = 
267 
exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) 

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

268 
 exn_msg _ TERMINATE = "Exit." 
28443  269 
 exn_msg _ Exn.Interrupt = "Interrupt." 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

289 

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

290 
end; 
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 

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

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

294 

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

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

296 

18685  297 
fun debugging f x = 
23940  298 
if ! debug then exception_trace (fn () => f x) 
18685  299 
else f x; 
300 

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

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

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

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

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

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

306 

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

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

308 

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

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

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

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

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

313 

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

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

315 
(f 
28463
b8f16c92122a
program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
wenzelm
parents:
28458
diff
changeset

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

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

318 

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

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

320 

5828  321 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

322 
(* node transactions  maintaining stable checkpoints *) 
7022  323 

6689  324 
local 
325 

26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

326 
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy) 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

327 
 is_draft_theory _ = false; 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

328 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

329 
fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false; 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

330 

26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

331 
fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!") 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

332 
 stale_error some = some; 
16815  333 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

334 
fun map_theory f (Theory (gthy, ctxt)) = 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

335 
Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, ctxt) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

336 
 map_theory _ node = node; 
6689  337 

338 
in 

339 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

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

341 
let 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

342 
val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state"; 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

343 
val cont_node = reset_presentation node; 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

344 
val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

345 
fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e); 
6689  346 

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

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

348 
cont_node 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

349 
> controlled_execution f 
26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

350 
> map_theory Theory.checkpoint 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

351 
> state_error NONE 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

352 
handle exn => state_error (SOME exn) cont_node; 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

353 

770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

354 
val (result', err') = 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

355 
if is_stale result then state_error (stale_error err) back_node 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

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

357 
in 
26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

358 
(case err' of 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

359 
NONE => result' 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

360 
 SOME exn => raise FAILURE (result', exn)) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

361 
end; 
6689  362 

363 
end; 

364 

365 

366 
(* primitive transitions *) 

367 

5828  368 
datatype trans = 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

369 
Init of string * (bool > theory) * (theory > unit)  (*theory name, init, exit*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

370 
Exit  (*formal exit of theory  without committing*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

371 
CommitExit  (*exit and commit final theory*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

372 
Keep of bool > state > unit  (*peek at state*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

373 
Transaction of bool > node > node; (*node transaction*) 
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

374 

6689  375 
local 
5828  376 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

377 
fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) = 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

378 
State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE) 
27603  379 
 apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) = 
380 
State (NONE, prev) 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

381 
 apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) = 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

382 
(controlled_execution exit thy; toplevel) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

383 
 apply_tr int _ (Keep f) state = 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

384 
controlled_execution (fn x => tap (f int) x) state 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

385 
 apply_tr int pos (Transaction f) (State (SOME state, _)) = 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

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

387 
 apply_tr _ _ _ _ = raise UNDEF; 
5828  388 

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

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

390 
 apply_union int pos (tr :: trs) state = 
28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

391 
apply_union int pos trs state 
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

392 
handle UNDEF => apply_tr int pos tr state 
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

393 
 FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state 
6689  394 
 exn as FAILURE _ => raise exn 
395 
 exn => raise FAILURE (state, exn); 

396 

397 
in 

398 

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

399 
fun apply_trans int pos trs state = (apply_union int pos trs state, NONE) 
15531  400 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  401 

402 
end; 

5828  403 

404 

405 
(* datatype transition *) 

406 

407 
datatype transition = Transition of 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

408 
{name: string, (*command name*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

409 
pos: Position.T, (*source position*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

410 
int_only: bool, (*interactiveonly*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

411 
print: bool, (*print result state*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

412 
no_timing: bool, (*suppress timing*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

413 
trans: trans list}; (*primitive transitions (union)*) 
5828  414 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

415 
fun make_transition (name, pos, int_only, print, no_timing, trans) = 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

416 
Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing, 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

417 
trans = trans}; 
5828  418 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

419 
fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) = 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

420 
make_transition (f (name, pos, int_only, print, no_timing, trans)); 
5828  421 

27441  422 
val empty = make_transition ("", Position.none, false, false, false, []); 
5828  423 

424 

425 
(* diagnostics *) 

426 

27441  427 
fun init_of (Transition {trans = [Init (name, _, _)], ...}) = SOME name 
428 
 init_of _ = NONE; 

429 

27427  430 
fun name_of (Transition {name, ...}) = name; 
28105  431 
fun pos_of (Transition {pos, ...}) = pos; 
432 
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr); 

5828  433 

27427  434 
fun command_msg msg tr = msg ^ "command " ^ str_of tr; 
5828  435 
fun at_command tr = command_msg "At " tr ^ "."; 
436 

437 
fun type_error tr state = 

18685  438 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  439 

440 

441 
(* modify transitions *) 

442 

28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

443 
fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) => 
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

444 
(name, pos, int_only, print, no_timing, trans)); 
9010  445 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

446 
fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) => 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

447 
(name, pos, int_only, print, no_timing, trans)); 
5828  448 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

449 
fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) => 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

450 
(name, pos, int_only, print, no_timing, trans)); 
14923  451 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

452 
val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) => 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

453 
(name, pos, int_only, print, true, trans)); 
17363  454 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

455 
fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) => 
28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

456 
(name, pos, int_only, print, no_timing, tr :: trans)); 
16607  457 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

458 
val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) => 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

459 
(name, pos, int_only, print, no_timing, [])); 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

460 

28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

461 
fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) => 
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

462 
(name, pos, int_only, print, no_timing, trans)); 
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

463 

06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

464 
val print = set_print true; 
5828  465 

466 

21007  467 
(* basic transitions *) 
5828  468 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

469 
fun init_theory name f exit = add_trans (Init (name, f, exit)); 
6689  470 
val exit = add_trans Exit; 
7612  471 
val keep' = add_trans o Keep; 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

472 
fun transaction f = add_trans (Transaction f); 
5828  473 

7612  474 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  475 
fun imperative f = keep (fn _ => f ()); 
476 

27840  477 
fun ignored pos = empty > name "<ignored>" > position pos > imperative I; 
478 
fun malformed pos msg = 

479 
empty > name "<malformed>" > position pos > imperative (fn () => error msg); 

480 

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

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

15668  484 

21007  485 

486 
(* theory transitions *) 

15668  487 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

488 
fun generic_theory f = transaction (fn _ => 
26491  489 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 
490 
 _ => raise UNDEF)); 

491 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

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

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

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

495 

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

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

497 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

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

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

500 
let 
20985  501 
val lthy = f thy; 
21294  502 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
503 
in Theory (gthy, SOME lthy) end 

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

504 
 _ => raise UNDEF)); 
17076  505 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

506 
val end_local_theory = transaction (fn _ => 
21294  507 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) 
21007  508 
 _ => raise UNDEF)); 
509 

510 
local 

511 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

512 
fun local_theory_presentation loc f g = transaction (fn int => 
21294  513 
(fn Theory (gthy, _) => 
514 
let 

515 
val finish = loc_finish loc gthy; 

29380  516 
val lthy' = f int (loc_begin loc gthy); 
21294  517 
in Theory (finish lthy', SOME lthy') end 
27859  518 
 _ => raise UNDEF) #> tap g); 
15668  519 

21007  520 
in 
521 

29380  522 
fun local_theory' loc f = local_theory_presentation loc f (K I); 
523 
fun local_theory loc f = local_theory' loc (K f); 

524 
fun present_local_theory loc g = local_theory_presentation loc (K I) g; 

18955  525 

21007  526 
end; 
527 

528 

529 
(* proof transitions *) 

530 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

531 
fun end_proof f = transaction (fn int => 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

532 
(fn Proof (prf, (finish, _)) => 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

533 
let val state = ProofNode.current prf in 
21007  534 
if can (Proof.assert_bottom true) state then 
535 
let 

536 
val ctxt' = f int state; 

537 
val gthy' = finish ctxt'; 

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

539 
else raise UNDEF 

540 
end 

27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

541 
 SkipProof (0, (gthy, _)) => Theory (gthy, NONE) 
21007  542 
 _ => raise UNDEF)); 
543 

21294  544 
local 
545 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

546 
fun begin_proof init finish = transaction (fn int => 
21294  547 
(fn Theory (gthy, _) => 
548 
let 

24453  549 
val prf = init int gthy; 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

550 
val skip = ! skip_proofs; 
21294  551 
val schematic = Proof.schematic_goal prf; 
552 
in 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

553 
if skip andalso schematic then 
21294  554 
warning "Cannot skip proof of schematic goal statement" 
555 
else (); 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

556 
if skip andalso not schematic then 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

557 
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

558 
else Proof (ProofNode.init prf, (finish gthy, gthy)) 
21294  559 
end 
560 
 _ => raise UNDEF)); 

561 

562 
in 

563 

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

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

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

567 

24453  568 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  569 

570 
fun theory_to_proof f = begin_proof 

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

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

572 
(K (Context.Theory o ProofContext.theory_of)); 
21294  573 

574 
end; 

575 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

576 
val forget_proof = transaction (fn _ => 
21007  577 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
578 
 SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

579 
 _ => raise UNDEF)); 

580 

27859  581 
fun present_proof f = transaction (fn _ => 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

582 
(fn Proof (prf, x) => Proof (ProofNode.apply I prf, x) 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

583 
 skip as SkipProof _ => skip 
27859  584 
 _ => raise UNDEF) #> tap f); 
21177  585 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

586 
fun proofs' f = transaction (fn int => 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

587 
(fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x) 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

588 
 skip as SkipProof _ => skip 
16815  589 
 _ => raise UNDEF)); 
15668  590 

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

591 
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

592 
val proofs = proofs' o K; 
6689  593 
val proof = proof' o K; 
16815  594 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

595 
fun actual_proof f = transaction (fn _ => 
21007  596 
(fn Proof (prf, x) => Proof (f prf, x) 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

597 
 _ => raise UNDEF)); 
16815  598 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

599 
fun skip_proof f = transaction (fn _ => 
21007  600 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  601 
 _ => raise UNDEF)); 
602 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

603 
fun skip_proof_to_theory pred = transaction (fn _ => 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

604 
(fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

605 
 _ => raise UNDEF)); 
5828  606 

607 

608 

609 
(** toplevel transactions **) 

610 

27427  611 
(* identification *) 
612 

613 
fun get_id (Transition {pos, ...}) = Position.get_id pos; 

614 
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr; 

615 

616 

25960  617 
(* thread position *) 
25799  618 

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

620 
Position.setmp_thread_data pos f x; 
25799  621 

27606  622 
fun status tr m = 
623 
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) (); 

624 

26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

625 
fun error_msg tr exn_info = 
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

626 
setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) (); 
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

627 

25799  628 

28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

629 
(* posttransition hooks *) 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

630 

28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

631 
local val hooks = ref ([]: (transition > state > state > unit) list) in 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

632 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

633 
fun add_hook f = CRITICAL (fn () => change hooks (cons f)); 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

634 
fun get_hooks () = CRITICAL (fn () => ! hooks); 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

635 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

636 
end; 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

637 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

638 

5828  639 
(* apply transitions *) 
640 

6664  641 
local 
642 

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

644 
setmp_thread_position tr (fn state => 
25799  645 
let 
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

646 
val _ = if not int andalso int_only then warning (command_msg "Interactiveonly " tr) else (); 
16682  647 

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

650 

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

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

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

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

655 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

656 
val _ = if int andalso not (! quiet) andalso print then print_state false result else (); 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

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

659 
in 

5828  660 

26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

661 
fun transition int tr st = 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

662 
let 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

663 
val hooks = get_hooks (); 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

664 
fun apply_hooks st' = hooks > List.app (fn f => (try (fn () => f tr st st') (); ())); 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

665 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

666 
val ctxt = try context_of st; 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

667 
val res = 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

668 
(case app int tr st of 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

669 
(_, SOME TERMINATE) => NONE 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

670 
 (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info) 
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

671 
 (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr)) 
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

672 
 (st', NONE) => SOME (st', NONE)); 
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

673 
val _ = (case res of SOME (st', NONE) => apply_hooks st'  _ => ()); 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

674 
in res end; 
6664  675 

676 
end; 

5828  677 

678 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

679 
(* commit final exit *) 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

680 

28425  681 
fun commit_exit pos = 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

682 
name "end" empty 
28425  683 
> position pos 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

684 
> add_trans CommitExit 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

685 
> imperative (fn () => warning "Expected to find finished theory"); 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

686 

6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

687 

28425  688 
(* nested commands *) 
5828  689 

28425  690 
fun command tr st = 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

691 
(case transition (! interact) tr st of 
28425  692 
SOME (st', NONE) => st' 
693 
 SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

694 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

695 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

696 

b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

697 
(* excursion of units, consisting of commands with proof *) 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

698 

28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

699 
structure States = ProofDataFun 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

700 
( 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

701 
type T = state list future option; 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

702 
fun init _ = NONE; 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

703 
); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

704 

28425  705 
fun command_result tr st = 
706 
let val st' = command tr st 

707 
in (st', st') end; 

17076  708 

28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

709 
fun proof_result immediate (tr, proof_trs) st = 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

710 
let val st' = command tr st in 
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

711 
if immediate orelse null proof_trs orelse 
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

712 
not (can proof_of st') orelse Proof.is_relevant (proof_of st') 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

713 
then 
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

714 
let val (states, st'') = fold_map command_result proof_trs st' 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

715 
in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end 
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

716 
else 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

717 
let 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

718 
val (body_trs, end_tr) = split_last proof_trs; 
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

719 
val finish = Context.Theory o ProofContext.theory_of; 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

720 

d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

721 
val future_proof = Proof.future_proof 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

722 
(fn prf => 
29343
43ac99cdeb5b
future proofs: back to Future.fork_pri ~1 for improved parallelism;
wenzelm
parents:
29124
diff
changeset

723 
Future.fork_pri ~1 (fn () => 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

724 
let val (states, State (result_node, _)) = 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

725 
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev) 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

726 
=> State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev)) 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

727 
> fold_map command_result body_trs 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

728 
> command (end_tr > set_print false); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

729 
in (states, presentation_context (Option.map #1 result_node) NONE) end)) 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

730 
#> (fn (states, ctxt) => States.put (SOME states) ctxt); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

731 

d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

732 
val st'' = st' > command (end_tr > reset_trans > end_proof (K future_proof)); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

733 

d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

734 
val states = 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

735 
(case States.get (presentation_context (SOME (node_of st'')) NONE) of 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

736 
NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr)) 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

737 
 SOME states => states); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

738 
val result = Lazy.lazy 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

739 
(fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

740 

d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

741 
in (result, st'') end 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

742 
end; 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

743 

29068  744 
fun excursion input = 
28425  745 
let 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

746 
val end_pos = if null input then error "No input" else pos_of (fst (List.last input)); 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

747 

28645  748 
val immediate = not (Future.enabled ()); 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

749 
val (future_results, end_state) = fold_map (proof_result immediate) input toplevel; 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

750 
val _ = 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

751 
(case end_state of 
28999
3f7ca7fec74c
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
wenzelm
parents:
28974
diff
changeset

752 
State (NONE, SOME (Theory (Context.Theory _, _), _)) => () 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

753 
 _ => error "Unfinished development at end of input"); 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

754 
val results = maps Lazy.force future_results; 
29068  755 
in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end; 
7062  756 

6664  757 
end; 