author  wenzelm 
Mon, 14 Jul 2008 19:57:09 +0200  
changeset 27583  9109f0d8a565 
parent 27576  7afff36043e6 
child 27601  6683cdb94af8 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

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

5 
Isabelle/Isar toplevel transactions. 
5828  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 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

14 
val proof_node: node > ProofNode.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 
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 EXCURSION_FAIL of exn * string 
42 
exception TOPLEVEL_ERROR 

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

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

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

45 
val program: (unit > 'a) > 'a 
16682  46 
type transition 
5828  47 
val empty: transition 
27441  48 
val init_of: transition > string option 
27427  49 
val name_of: transition > string 
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 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

58 
val commit_exit: transition 
5828  59 
val keep: (state > unit) > transition > transition 
7612  60 
val keep': (bool > state > unit) > transition > transition 
5828  61 
val imperative: (unit > unit) > transition > transition 
62 
val theory: (theory > theory) > transition > transition 

26491  63 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  64 
val theory': (bool > theory > theory) > transition > transition 
20985  65 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  66 
val end_local_theory: transition > transition 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

67 
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

68 
val present_local_theory: xstring option > (bool > node > unit) > transition > transition 
24453  69 
val local_theory_to_proof': xstring option > (bool > local_theory > Proof.state) > 
70 
transition > transition 

21007  71 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
72 
transition > transition 

17363  73 
val theory_to_proof: (theory > Proof.state) > transition > transition 
21007  74 
val end_proof: (bool > Proof.state > Proof.context) > transition > transition 
75 
val forget_proof: transition > transition 

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

78 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21177  79 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
80 
val proof: (Proof.state > Proof.state) > transition > transition 

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

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

82 
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

83 
val skip_proof_to_theory: (int > bool) > transition > transition 
27427  84 
val get_id: transition > string option 
85 
val put_id: string > transition > transition 

9512  86 
val unknown_theory: transition > transition 
87 
val unknown_proof: transition > transition 

88 
val unknown_context: transition > transition 

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

89 
val error_msg: transition > exn * string > unit 
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

90 
val transition: bool > transition > state > (state * (exn * string) option) option 
17076  91 
val present_excursion: (transition * (state > state > 'a > 'a)) list > 'a > 'a 
5828  92 
val excursion: transition list > unit 
93 
end; 

94 

6965  95 
structure Toplevel: TOPLEVEL = 
5828  96 
struct 
97 

98 
(** toplevel state **) 

99 

19063  100 
exception UNDEF; 
101 

102 

21294  103 
(* local theory wrappers *) 
5828  104 

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

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

106 

25292  107 
val loc_init = TheoryTarget.context; 
21294  108 
val loc_exit = ProofContext.theory_of o LocalTheory.exit; 
109 

25292  110 
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "" loc) thy 
21294  111 
 loc_begin NONE (Context.Proof lthy) = lthy 
25269  112 
 loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); 
21294  113 

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

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

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

21294  118 

119 

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

120 
(* datatype node *) 
21294  121 

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

123 
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

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

125 
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

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

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

128 
(*proof depth, resulting theory, original theory*) 
5828  129 

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

131 
val theory_node = fn Theory (gthy, _) => SOME gthy  _ => NONE; 
18589  132 
val proof_node = fn Proof (prf, _) => SOME prf  _ => NONE; 
133 

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

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

135 
 cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf) 
21007  136 
 cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; 
19063  137 

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

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

139 
 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

140 
 presentation_context (SOME node) (SOME loc) = 
25269  141 
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

142 
 presentation_context NONE _ = raise UNDEF; 
19063  143 

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

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

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

146 

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

147 

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

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

149 

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

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

151 
(node * (theory > unit)) option * (*current node with exit operation*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

152 
node option; (*previous node*) 
5828  153 

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

154 
val toplevel = State (NONE, NONE); 
5828  155 

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

156 
fun is_toplevel (State (NONE, _)) = true 
7732  157 
 is_toplevel _ = false; 
158 

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

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

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

161 
 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

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

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

164 
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

165 
 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

166 
 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

167 
 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

168 
 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

169 

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

170 

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

171 
(* current node *) 
5828  172 

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

173 
fun previous_node_of (State (_, prev_node)) = prev_node; 
6689  174 

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

175 
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

176 
 node_of (State (SOME (node, _), _)) = node; 
5828  177 

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

180 

19063  181 
fun node_case f g state = cases_node f g (node_of state); 
5828  182 

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

185 
val theory_of = node_case Context.theory_of Proof.theory_of; 
18589  186 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  187 

18589  188 
fun proof_position_of state = 
189 
(case node_of state of 

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

190 
Proof (prf, _) => ProofNode.position prf 
18589  191 
 _ => raise UNDEF); 
6664  192 

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

195 

16815  196 
(* print state *) 
197 

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

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

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

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

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

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

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

206 
> Pretty.chunks > Pretty.writeln; 
16815  207 

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

208 
fun print_state prf_only state = 
23701  209 
(case try node_of state of 
210 
NONE => [] 

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

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

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

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

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

217 

15668  218 

5828  219 
(** toplevel transitions **) 
220 

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

223 
val interact = ref false; 
16682  224 
val timing = Output.timing; 
225 
val profiling = ref 0; 

16815  226 
val skip_proofs = ref false; 
16682  227 

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

231 
exception TOPLEVEL_ERROR; 
5828  232 

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

233 

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

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

235 

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

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

237 

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

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

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

240 

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

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

242 

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

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

244 
 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

245 

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

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

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

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

251 

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

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

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

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

255 

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

256 
fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

257 
 exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

258 
 exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg]) 
26293  259 
 exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = 
260 
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

261 
 exn_msg _ TERMINATE = "Exit." 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

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

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

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

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

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

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

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

269 
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

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

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

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

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

274 
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

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

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

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

278 
 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

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

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

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

282 

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

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

284 

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

285 

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

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

287 

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

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

289 

18685  290 
fun debugging f x = 
23940  291 
if ! debug then exception_trace (fn () => f x) 
18685  292 
else f x; 
293 

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

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

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

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

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

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

299 

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

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

301 

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

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

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

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

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

306 

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

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

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

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

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

311 

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

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

313 

5828  314 

16815  315 
(* node transactions and recovery from stale theories *) 
6689  316 

16815  317 
(*NB: proof commands should be nondestructive!*) 
7022  318 

6689  319 
local 
320 

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

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

323 
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

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

325 

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

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

327 
 stale_error some = some; 
16815  328 

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

329 
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

330 
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

331 
 map_theory _ node = node; 
6689  332 

333 
in 

334 

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

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

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

337 
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

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

339 
val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

340 
fun state_error e nd = (State (SOME (nd, exit), SOME node), e); 
6689  341 

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

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

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

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

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

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

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

348 

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

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

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

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

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

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

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

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

356 
end; 
6689  357 

358 
end; 

359 

360 

361 
(* primitive transitions *) 

362 

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

366 
Transaction.*) 

5828  367 

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) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

379 
 apply_tr _ _ Exit (State (SOME (node as Theory (Context.Theory _, _), _), _)) = 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

380 
State (NONE, SOME node) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

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

386 
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 = 
9981199bf865
transaction: context_position (nondestructive only);
wenzelm
parents:
22588
diff
changeset

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

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

393 
 FAILURE (alt_state, UNDEF) => apply_union int pos trs 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; 
431 
fun str_of (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; 

5828  432 

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

436 
fun type_error tr state = 

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

439 

440 
(* modify transitions *) 

441 

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

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

443 
(nm, pos, int_only, print, no_timing, trans)); 
9010  444 

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

445 
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

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

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

448 
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

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

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

451 
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

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

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

454 
fun add_trans tr = map_transition (fn (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

455 
(name, pos, int_only, print, no_timing, trans @ [tr])); 
16607  456 

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

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

458 
(name, pos, int_only, true, no_timing, trans)); 
5828  459 

460 

21007  461 
(* basic transitions *) 
5828  462 

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

463 
fun init_theory name f exit = add_trans (Init (name, f, exit)); 
6689  464 
val exit = add_trans Exit; 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

465 
val commit_exit = add_trans CommitExit (name "end" empty); 
7612  466 
val keep' = add_trans o Keep; 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

467 
fun app_current f = add_trans (Transaction f); 
5828  468 

7612  469 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  470 
fun imperative f = keep (fn _ => f ()); 
471 

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

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

15668  475 

21007  476 

477 
(* theory transitions *) 

15668  478 

26491  479 
fun generic_theory f = app_current (fn _ => 
480 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 

481 
 _ => raise UNDEF)); 

482 

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

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

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

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

486 

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

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

488 

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

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

491 
let 
20985  492 
val lthy = f thy; 
21294  493 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
494 
in Theory (gthy, SOME lthy) end 

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

495 
 _ => raise UNDEF)); 
17076  496 

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

21007  499 
 _ => raise UNDEF)); 
500 

501 
local 

502 

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

503 
fun local_theory_presentation loc f g = app_current (fn int => 
21294  504 
(fn Theory (gthy, _) => 
505 
let 

506 
val finish = loc_finish loc gthy; 

25960  507 
val lthy' = f (loc_begin loc gthy); 
21294  508 
in Theory (finish lthy', SOME lthy') end 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

509 
 _ => raise UNDEF) #> tap (g int)); 
15668  510 

21007  511 
in 
512 

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

513 
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

514 
fun present_local_theory loc g = local_theory_presentation loc I g; 
18955  515 

21007  516 
end; 
517 

518 

519 
(* proof transitions *) 

520 

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

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

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

523 
let val state = ProofNode.current prf in 
21007  524 
if can (Proof.assert_bottom true) state then 
525 
let 

526 
val ctxt' = f int state; 

527 
val gthy' = finish ctxt'; 

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

529 
else raise UNDEF 

530 
end 

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

531 
 SkipProof (0, (gthy, _)) => Theory (gthy, NONE) 
21007  532 
 _ => raise UNDEF)); 
533 

21294  534 
local 
535 

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

537 
(fn Theory (gthy, _) => 

538 
let 

24453  539 
val prf = init int gthy; 
21294  540 
val schematic = Proof.schematic_goal prf; 
541 
in 

542 
if ! skip_proofs andalso schematic then 

543 
warning "Cannot skip proof of schematic goal statement" 

544 
else (); 

545 
if ! skip_proofs andalso not schematic then 

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

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

547 
else Proof (ProofNode.init prf, (finish gthy, gthy)) 
21294  548 
end 
549 
 _ => raise UNDEF)); 

550 

551 
in 

552 

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

553 
fun local_theory_to_proof' loc f = begin_proof 
25960  554 
(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

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

556 

24453  557 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  558 

559 
fun theory_to_proof f = begin_proof 

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

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

561 
(K (Context.Theory o ProofContext.theory_of)); 
21294  562 

563 
end; 

564 

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

565 
val forget_proof = app_current (fn _ => 
21007  566 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
567 
 SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

568 
 _ => raise UNDEF)); 

569 

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

570 
fun present_proof f = app_current (fn int => 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

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

572 
 skip as SkipProof _ => skip 
21177  573 
 _ => raise UNDEF) #> tap (f int)); 
574 

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

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

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

577 
 skip as SkipProof _ => skip 
16815  578 
 _ => raise UNDEF)); 
15668  579 

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

580 
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

581 
val proofs = proofs' o K; 
6689  582 
val proof = proof' o K; 
16815  583 

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

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

586 
 _ => raise UNDEF)); 
16815  587 

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

588 
fun skip_proof f = app_current (fn _ => 
21007  589 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  590 
 _ => raise UNDEF)); 
591 

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

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

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

594 
 _ => raise UNDEF)); 
5828  595 

596 

597 

598 
(** toplevel transactions **) 

599 

27427  600 
(* identification *) 
601 

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

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

604 

605 

25960  606 
(* thread position *) 
25799  607 

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

609 
Position.setmp_thread_data pos f x; 
25799  610 

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

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

612 
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

613 

25799  614 

5828  615 
(* apply transitions *) 
616 

6664  617 
local 
618 

25799  619 
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

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

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

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

626 

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

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

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

631 

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

632 
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

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

635 
in 

5828  636 

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

637 
fun transition int tr st = 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

638 
let val ctxt = try context_of st in 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

639 
(case app int tr st of 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

640 
(_, SOME TERMINATE) => NONE 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

641 
 (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

642 
 (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr)) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

643 
 (state', NONE) => SOME (state', NONE)) 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

644 
end; 
6664  645 

646 
end; 

5828  647 

648 

17076  649 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  650 

6664  651 
local 
652 

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

653 
fun no_pr _ _ _ = (); 
5828  654 

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

655 
fun excur (tr, pr) st res = 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

656 
(case transition (! interact) tr st of 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

657 
SOME (st', NONE) => 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

658 
(st, st', setmp_thread_position tr (fn () => pr st st' res) () handle exn => 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

659 
raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

660 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

661 
 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

662 

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

663 
fun excurs (tr :: trs) (_, st, res) = excurs trs (excur tr st res) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

664 
 excurs [] (st, st', res') = 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

665 
if is_toplevel st' then (excur (commit_exit, no_pr) st (); res') 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

666 
else error "Unfinished development at end of input"; 
17076  667 

6664  668 
in 
669 

17076  670 
fun present_excursion trs res = 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

671 
excurs trs (toplevel, toplevel, res) handle exn => error (exn_message exn); 
9134  672 

17076  673 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  674 

6664  675 
end; 
676 

5828  677 
end; 