author  wenzelm 
Mon, 14 Jul 2008 17:51:43 +0200  
changeset 27576  7afff36043e6 
parent 27564  fc6d34e49e17 
child 27583  9109f0d8a565 
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 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

41 
exception CONTEXT of Proof.context * exn 
24055
f7483532537b
added TOPLEVEL_ERROR (simplified version from output.ML);
wenzelm
parents:
23975
diff
changeset

42 
exception TOPLEVEL_ERROR 
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 
27500  49 
val str_of: transition > string 
5828  50 
val name: string > transition > transition 
51 
val position: Position.T > transition > transition 

52 
val interactive: bool > transition > transition 

53 
val print: transition > transition 

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

55 
val init_theory: string > (bool > theory) > (theory > unit) > transition > transition 
6689  56 
val exit: transition > transition 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

57 
val commit_exit: 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 
61 
val theory: (theory > theory) > transition > transition 

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

66 
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

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

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

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

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

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

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

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

81 
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

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

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

87 
val unknown_context: transition > transition 

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

88 
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

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

93 

6965  94 
structure Toplevel: TOPLEVEL = 
5828  95 
struct 
96 

97 
(** toplevel state **) 

98 

19063  99 
exception UNDEF; 
100 

101 

21294  102 
(* local theory wrappers *) 
5828  103 

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

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

105 

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

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

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

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

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

21294  117 

118 

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

119 
(* datatype node *) 
21294  120 

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

122 
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

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

124 
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

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

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

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

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

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

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

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

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

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

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

138 
 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

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

141 
 presentation_context NONE _ = raise UNDEF; 
19063  142 

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

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

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

145 

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

146 

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

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

148 

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

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

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

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

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

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

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

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

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

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

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

160 
 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

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

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

163 
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

164 
 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

165 
 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

166 
 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

167 
 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

168 

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

169 

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

170 
(* current node *) 
5828  171 

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

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

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

174 
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

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

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

179 

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

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

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

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

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

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

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

194 

16815  195 
(* print state *) 
196 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

216 

15668  217 

5828  218 
(** toplevel transitions **) 
219 

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

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

16815  225 
val skip_proofs = ref false; 
16682  226 

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

230 
exception TOPLEVEL_ERROR; 
5828  231 

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

232 

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

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

234 

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

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

236 

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

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

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

239 

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

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

241 

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

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

243 
 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

244 

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

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

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

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

248 

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

249 
in 
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 exn_message e = 
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

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

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

254 

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

255 
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

256 
 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

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

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

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

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

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

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

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

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

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

268 
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

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

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

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

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

273 
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

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

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

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

277 
 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

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

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

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

281 

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

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

283 

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

286 

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

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

288 

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

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

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

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

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

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

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

298 

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

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

300 

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

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

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

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

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

305 

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

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

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

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

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

310 

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

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

312 

5828  313 

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

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

6689  318 
local 
319 

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

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

322 
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

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

324 

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

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

326 
 stale_error some = some; 
16815  327 

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

328 
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

329 
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

330 
 map_theory _ node = node; 
6689  331 

332 
in 

333 

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

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

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

336 
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

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

338 
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

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

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

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

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

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

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

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

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

347 

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

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

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

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

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

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

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

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

355 
end; 
6689  356 

357 
end; 

358 

359 

360 
(* primitive transitions *) 

361 

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

365 
Transaction.*) 

5828  366 

367 
datatype trans = 

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

368 
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

369 
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

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

371 
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

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

373 

6689  374 
local 
5828  375 

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

376 
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

377 
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

378 
 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

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

380 
 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

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

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

383 
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

384 
 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

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

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

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

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

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

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

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

392 
 FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state 
6689  393 
 exn as FAILURE _ => raise exn 
394 
 exn => raise FAILURE (state, exn); 

395 

396 
in 

397 

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

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

401 
end; 

5828  402 

403 

404 
(* datatype transition *) 

405 

406 
datatype transition = Transition of 

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

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

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

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

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

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

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

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

414 
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

415 
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

416 
trans = trans}; 
5828  417 

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

418 
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

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

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

423 

424 
(* diagnostics *) 

425 

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

428 

27427  429 
fun name_of (Transition {name, ...}) = name; 
430 
fun str_of (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; 

5828  431 

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

435 
fun type_error tr state = 

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

438 

439 
(* modify transitions *) 

440 

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

441 
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

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

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

444 
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

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

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

447 
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

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

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

450 
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

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

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

453 
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

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

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

456 
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

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

459 

21007  460 
(* basic transitions *) 
5828  461 

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

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

464 
val commit_exit = add_trans CommitExit (name "end" empty); 
7612  465 
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

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

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

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

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

15668  474 

21007  475 

476 
(* theory transitions *) 

15668  477 

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

480 
 _ => raise UNDEF)); 

481 

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

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

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

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

485 

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

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

487 

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

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

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

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

494 
 _ => raise UNDEF)); 
17076  495 

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

21007  498 
 _ => raise UNDEF)); 
499 

500 
local 

501 

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

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

505 
val finish = loc_finish loc gthy; 

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

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

21007  510 
in 
511 

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

512 
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

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

21007  515 
end; 
516 

517 

518 
(* proof transitions *) 

519 

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

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

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

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

525 
val ctxt' = f int state; 

526 
val gthy' = finish ctxt'; 

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

528 
else raise UNDEF 

529 
end 

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

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

21294  533 
local 
534 

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

536 
(fn Theory (gthy, _) => 

537 
let 

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

541 
if ! skip_proofs andalso schematic then 

542 
warning "Cannot skip proof of schematic goal statement" 

543 
else (); 

544 
if ! skip_proofs andalso not schematic then 

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

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

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

549 

550 
in 

551 

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

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

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

555 

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

558 
fun theory_to_proof f = begin_proof 

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

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

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

562 
end; 

563 

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

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

567 
 _ => raise UNDEF)); 

568 

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

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

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

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

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

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

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

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

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

579 
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

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

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

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

585 
 _ => raise UNDEF)); 
16815  586 

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

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

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

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

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

593 
 _ => raise UNDEF)); 
5828  594 

595 

596 

597 
(** toplevel transactions **) 

598 

27427  599 
(* identification *) 
600 

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

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

603 

604 

25960  605 
(* thread position *) 
25799  606 

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

608 
Position.setmp_thread_data pos f x; 
25799  609 

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

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

611 
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

612 

25799  613 

5828  614 
(* apply transitions *) 
615 

6664  616 
local 
617 

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

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

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

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

625 

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

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

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

630 

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

631 
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

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

634 
in 

5828  635 

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

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

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

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

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

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

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

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

643 
end; 
6664  644 

645 
end; 

5828  646 

647 

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

6664  650 
local 
651 

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

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

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

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

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

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

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

658 
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

659 
 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

660 
 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

661 

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

662 
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

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

664 
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

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

6664  667 
in 
668 

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

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

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

6664  674 
end; 
675 

5828  676 
end; 