author  wenzelm 
Thu, 18 Aug 2011 17:53:32 +0200  
changeset 44270  3eaad39e520c 
parent 44200  ce0112e26b3b 
child 44304  7ee000ce5390 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

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

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

7 
signature TOPLEVEL = 

8 
sig 

19063  9 
exception UNDEF 
5828  10 
type state 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

11 
val toplevel: state 
7732  12 
val is_toplevel: state > bool 
18589  13 
val is_theory: state > bool 
14 
val is_proof: state > bool 

17076  15 
val level: state > int 
30398  16 
val presentation_context_of: state > Proof.context 
30801  17 
val previous_context_of: state > Proof.context option 
21506  18 
val context_of: state > Proof.context 
22089  19 
val generic_theory_of: state > generic_theory 
5828  20 
val theory_of: state > theory 
21 
val proof_of: state > Proof.state 

18589  22 
val proof_position_of: state > int 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

23 
val end_theory: Position.T > state > theory 
16815  24 
val print_state_context: state > unit 
25 
val print_state: bool > state > unit 

37858  26 
val pretty_abstract: state > Pretty.T 
32738  27 
val quiet: bool Unsynchronized.ref 
28 
val debug: bool Unsynchronized.ref 

29 
val interact: bool Unsynchronized.ref 

30 
val timing: bool Unsynchronized.ref 

31 
val profiling: int Unsynchronized.ref 

32 
val skip_proofs: bool Unsynchronized.ref 

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

33 
val program: (unit > 'a) > 'a 
33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

34 
val thread: bool > (unit > unit) > Thread.thread 
16682  35 
type transition 
5828  36 
val empty: transition 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

37 
val print_of: transition > bool 
27427  38 
val name_of: transition > string 
28105  39 
val pos_of: transition > Position.T 
27500  40 
val str_of: transition > string 
5828  41 
val name: string > transition > transition 
42 
val position: Position.T > transition > transition 

43 
val interactive: bool > transition > transition 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

44 
val set_print: bool > transition > transition 
5828  45 
val print: transition > transition 
9010  46 
val no_timing: transition > transition 
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

47 
val init_theory: (unit > theory) > transition > transition 
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

48 
val is_init: transition > bool 
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset

49 
val modify_init: (unit > theory) > transition > transition 
6689  50 
val exit: transition > transition 
5828  51 
val keep: (state > unit) > transition > transition 
7612  52 
val keep': (bool > state > unit) > transition > transition 
5828  53 
val imperative: (unit > unit) > transition > transition 
27840  54 
val ignored: Position.T > transition 
55 
val malformed: Position.T > string > transition 

5828  56 
val theory: (theory > theory) > transition > transition 
26491  57 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  58 
val theory': (bool > theory > theory) > transition > transition 
20985  59 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  60 
val end_local_theory: transition > transition 
29380  61 
val local_theory': xstring option > (bool > local_theory > local_theory) > 
62 
transition > transition 

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

63 
val local_theory: xstring option > (local_theory > local_theory) > transition > transition 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

64 
val present_local_theory: xstring option > (state > unit) > transition > transition 
24453  65 
val local_theory_to_proof': xstring option > (bool > local_theory > Proof.state) > 
66 
transition > transition 

21007  67 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
68 
transition > transition 

17363  69 
val theory_to_proof: (theory > Proof.state) > transition > transition 
21007  70 
val end_proof: (bool > Proof.state > Proof.context) > transition > transition 
71 
val forget_proof: transition > transition 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

72 
val present_proof: (state > unit) > transition > transition 
21177  73 
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

74 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21177  75 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
76 
val proof: (Proof.state > Proof.state) > transition > transition 

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

78 
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

79 
val skip_proof_to_theory: (int > bool) > transition > transition 
27427  80 
val get_id: transition > string option 
81 
val put_id: string > transition > transition 

9512  82 
val unknown_theory: transition > transition 
83 
val unknown_proof: transition > transition 

84 
val unknown_context: transition > transition 

28425  85 
val setmp_thread_position: transition > ('a > 'b) > 'a > 'b 
27606  86 
val status: transition > Markup.T > unit 
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44200
diff
changeset

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

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

89 
val transition: bool > transition > state > (state * (exn * string) option) option 
28425  90 
val command: transition > state > state 
42129
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42012
diff
changeset

91 
val excursion: 
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42012
diff
changeset

92 
(transition * transition list) list > (transition * state) list future list * theory 
5828  93 
end; 
94 

6965  95 
structure Toplevel: TOPLEVEL = 
5828  96 
struct 
97 

98 
(** toplevel state **) 

99 

31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

100 
exception UNDEF = Runtime.UNDEF; 
19063  101 

102 

21294  103 
(* local theory wrappers *) 
5828  104 

38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38236
diff
changeset

105 
val loc_init = Named_Target.context_cmd; 
33671  106 
val loc_exit = Local_Theory.exit_global; 
21294  107 

25292  108 
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "" loc) thy 
21294  109 
 loc_begin NONE (Context.Proof lthy) = lthy 
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset

110 
 loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy; 
21294  111 

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

33671  113 
 loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore 
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset

114 
 loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy; 
21294  115 

116 

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

117 
(* datatype node *) 
21294  118 

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

120 
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

121 
(*theory with presentation context*)  
33390  122 
Proof of Proof_Node.T * ((Proof.context > generic_theory) * generic_theory) 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

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

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

125 
(*proof depth, resulting theory, original theory*) 
5828  126 

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

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

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

130 
fun cases_node f _ (Theory (gthy, _)) = f gthy 
33390  131 
 cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) 
21007  132 
 cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; 
19063  133 

29066  134 
val context_node = cases_node Context.proof_of Proof.context_of; 
135 

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

136 

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

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

138 

37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

139 
datatype state = State of node option * node option; (*current, previous*) 
5828  140 

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

141 
val toplevel = State (NONE, NONE); 
5828  142 

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

143 
fun is_toplevel (State (NONE, _)) = true 
7732  144 
 is_toplevel _ = false; 
145 

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

146 
fun level (State (NONE, _)) = 0 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

147 
 level (State (SOME (Theory _), _)) = 0 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

148 
 level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

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

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

151 
fun str_of_state (State (NONE, _)) = "at top level" 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

152 
 str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode" 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

153 
 str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode" 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

154 
 str_of_state (State (SOME (Proof _), _)) = "in proof mode" 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

155 
 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

156 

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

157 

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

158 
(* current node *) 
5828  159 

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

160 
fun node_of (State (NONE, _)) = raise UNDEF 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

161 
 node_of (State (SOME node, _)) = node; 
5828  162 

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

165 

19063  166 
fun node_case f g state = cases_node f g (node_of state); 
5828  167 

30398  168 
fun presentation_context_of state = 
169 
(case try node_of state of 

170 
SOME (Theory (_, SOME ctxt)) => ctxt 

171 
 SOME node => context_node node 

172 
 NONE => raise UNDEF); 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

173 

30801  174 
fun previous_context_of (State (_, NONE)) = NONE 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

175 
 previous_context_of (State (_, SOME prev)) = SOME (context_node prev); 
30801  176 

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

179 
val theory_of = node_case Context.theory_of Proof.theory_of; 
18589  180 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  181 

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

33390  184 
Proof (prf, _) => Proof_Node.position prf 
18589  185 
 _ => raise UNDEF); 
6664  186 

43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

187 
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy 
44200  188 
 end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos) 
189 
 end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos); 

37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

190 

5828  191 

16815  192 
(* print state *) 
193 

38388  194 
val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; 
16815  195 

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

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

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

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

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

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

202 
> Pretty.chunks > Pretty.writeln; 
16815  203 

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

204 
fun print_state prf_only state = 
23701  205 
(case try node_of state of 
206 
NONE => [] 

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

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

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

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

37858  213 
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); 
214 

16815  215 

15668  216 

5828  217 
(** toplevel transitions **) 
218 

32738  219 
val quiet = Unsynchronized.ref false; 
39513
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
39285
diff
changeset

220 
val debug = Runtime.debug; 
32738  221 
val interact = Unsynchronized.ref false; 
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41703
diff
changeset

222 
val timing = Unsynchronized.ref false; 
32738  223 
val profiling = Unsynchronized.ref 0; 
224 
val skip_proofs = Unsynchronized.ref false; 

16682  225 

33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

226 
fun program body = 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

227 
(body 
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

228 
> Runtime.controlled_execution 
33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

229 
> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) (); 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

230 

d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

231 
fun thread interrupts body = 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

232 
Thread.fork 
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn  hardly ever need to mention Interrupt literally;
wenzelm
parents:
38888
diff
changeset

233 
(((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn) 
33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

234 
> Runtime.debugging 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

235 
> Runtime.toplevel_error 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset

236 
(fn exn => 
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset

237 
Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))), 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37208
diff
changeset

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

239 

5828  240 

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

241 
(* node transactions  maintaining stable checkpoints *) 
7022  242 

31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

243 
exception FAILURE of state * exn; 
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

244 

6689  245 
local 
246 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

247 
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) 
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

248 
 reset_presentation node = node; 
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

249 

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

250 
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

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

252 

31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

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

254 

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

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

256 
 stale_error some = some; 
16815  257 

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

258 
fun map_theory f (Theory (gthy, ctxt)) = 
33671  259 
Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt) 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

260 
 map_theory _ node = node; 
6689  261 

262 
in 

263 

37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

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

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

266 
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

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

268 
val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

269 
fun state_error e nd = (State (SOME nd, SOME node), e); 
6689  270 

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

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

272 
cont_node 
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

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

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

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

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

277 

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

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

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

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

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

282 
(case err' of 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

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

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

285 
end; 
6689  286 

43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

287 
val exit_transaction = 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

288 
apply_transaction 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

289 
(fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE) 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

290 
 node => node) (K ()) 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

291 
#> (fn State (node', _) => State (NONE, node')); 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

292 

6689  293 
end; 
294 

295 

296 
(* primitive transitions *) 

297 

5828  298 
datatype trans = 
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

299 
Init of unit > theory  (*init theory*) 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

300 
Exit  (*formal exit of theory*) 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

301 
Keep of bool > state > unit  (*peek at state*) 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

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

303 

6689  304 
local 
5828  305 

44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

306 
fun apply_tr _ (Init f) (State (NONE, _)) = 
33727
e2d5d7f51aa3
init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents:
33725
diff
changeset

307 
State (SOME (Theory (Context.Theory 
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset

308 
(Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE) 
43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

309 
 apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) = 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

310 
exit_transaction state 
32792  311 
 apply_tr int (Keep f) state = 
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

312 
Runtime.controlled_execution (fn x => tap (f int) x) state 
32792  313 
 apply_tr int (Transaction (f, g)) (State (SOME state, _)) = 
314 
apply_transaction (fn x => f int x) g state 

315 
 apply_tr _ _ _ = raise UNDEF; 

5828  316 

32792  317 
fun apply_union _ [] state = raise FAILURE (state, UNDEF) 
318 
 apply_union int (tr :: trs) state = 

319 
apply_union int trs state 

320 
handle Runtime.UNDEF => apply_tr int tr state 

321 
 FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state 

6689  322 
 exn as FAILURE _ => raise exn 
323 
 exn => raise FAILURE (state, exn); 

324 

325 
in 

326 

32792  327 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
15531  328 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  329 

330 
end; 

5828  331 

332 

333 
(* datatype transition *) 

334 

335 
datatype transition = Transition of 

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

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

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

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

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

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

341 
trans: trans list}; (*primitive transitions (union)*) 
5828  342 

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

343 
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

344 
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

345 
trans = trans}; 
5828  346 

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

347 
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

348 
make_transition (f (name, pos, int_only, print, no_timing, trans)); 
5828  349 

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

352 

353 
(* diagnostics *) 

354 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

355 
fun print_of (Transition {print, ...}) = print; 
27427  356 
fun name_of (Transition {name, ...}) = name; 
28105  357 
fun pos_of (Transition {pos, ...}) = pos; 
358 
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr); 

5828  359 

27427  360 
fun command_msg msg tr = msg ^ "command " ^ str_of tr; 
38875
c7a66b584147
tuned messages: discontinued spurious fullstops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38721
diff
changeset

361 
fun at_command tr = command_msg "At " tr; 
5828  362 

363 
fun type_error tr state = 

18685  364 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  365 

366 

367 
(* modify transitions *) 

368 

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

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

370 
(name, pos, int_only, print, no_timing, trans)); 
9010  371 

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

372 
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

373 
(name, pos, int_only, print, no_timing, trans)); 
5828  374 

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

375 
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

376 
(name, pos, int_only, print, no_timing, trans)); 
14923  377 

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

378 
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

379 
(name, pos, int_only, print, true, trans)); 
17363  380 

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

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

382 
(name, pos, int_only, print, no_timing, tr :: trans)); 
16607  383 

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

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

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

386 

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

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

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

389 

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

390 
val print = set_print true; 
5828  391 

392 

21007  393 
(* basic transitions *) 
5828  394 

44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

395 
fun init_theory f = add_trans (Init f); 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37953
diff
changeset

396 

44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

397 
fun is_init (Transition {trans = [Init _], ...}) = true 
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

398 
 is_init _ = false; 
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

399 

88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

400 
fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37953
diff
changeset

401 

6689  402 
val exit = add_trans Exit; 
7612  403 
val keep' = add_trans o Keep; 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

404 

e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

405 
fun present_transaction f g = add_trans (Transaction (f, g)); 
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

406 
fun transaction f = present_transaction f (K ()); 
5828  407 

7612  408 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  409 
fun imperative f = keep (fn _ => f ()); 
410 

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

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

414 

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

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

15668  418 

21007  419 

420 
(* theory transitions *) 

15668  421 

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

422 
fun generic_theory f = transaction (fn _ => 
26491  423 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 
424 
 _ => raise UNDEF)); 

425 

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

426 
fun theory' f = transaction (fn int => 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

427 
(fn Theory (Context.Theory thy, _) => 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

428 
let val thy' = thy 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

429 
> Sign.new_group 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

430 
> Theory.checkpoint 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

431 
> f int 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

432 
> Sign.reset_group; 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

433 
in Theory (Context.Theory thy', NONE) end 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

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

435 

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

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

437 

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

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

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

440 
let 
20985  441 
val lthy = f thy; 
21294  442 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
443 
in Theory (gthy, SOME lthy) end 

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

444 
 _ => raise UNDEF)); 
17076  445 

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

446 
val end_local_theory = transaction (fn _ => 
21294  447 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) 
21007  448 
 _ => raise UNDEF)); 
449 

450 
local 

451 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

452 
fun local_theory_presentation loc f = present_transaction (fn int => 
21294  453 
(fn Theory (gthy, _) => 
454 
let 

455 
val finish = loc_finish loc gthy; 

33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

456 
val lthy' = loc_begin loc gthy 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

457 
> Local_Theory.new_group 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

458 
> f int 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

459 
> Local_Theory.reset_group; 
21294  460 
in Theory (finish lthy', SOME lthy') end 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

461 
 _ => raise UNDEF)); 
15668  462 

21007  463 
in 
464 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

465 
fun local_theory' loc f = local_theory_presentation loc f (K ()); 
29380  466 
fun local_theory loc f = local_theory' loc (K f); 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

467 
fun present_local_theory loc = local_theory_presentation loc (K I); 
18955  468 

21007  469 
end; 
470 

471 

472 
(* proof transitions *) 

473 

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

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

475 
(fn Proof (prf, (finish, _)) => 
33390  476 
let val state = Proof_Node.current prf in 
21007  477 
if can (Proof.assert_bottom true) state then 
478 
let 

479 
val ctxt' = f int state; 

480 
val gthy' = finish ctxt'; 

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

482 
else raise UNDEF 

483 
end 

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

484 
 SkipProof (0, (gthy, _)) => Theory (gthy, NONE) 
21007  485 
 _ => raise UNDEF)); 
486 

21294  487 
local 
488 

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

489 
fun begin_proof init finish = transaction (fn int => 
21294  490 
(fn Theory (gthy, _) => 
491 
let 

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

493 
val skip = ! skip_proofs; 
40960  494 
val (is_goal, no_skip) = 
495 
(true, Proof.schematic_goal prf) handle ERROR _ => (false, true); 

21294  496 
in 
40960  497 
if is_goal andalso skip andalso no_skip then 
21294  498 
warning "Cannot skip proof of schematic goal statement" 
499 
else (); 

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

501 
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) 
33390  502 
else Proof (Proof_Node.init prf, (finish gthy, gthy)) 
21294  503 
end 
504 
 _ => raise UNDEF)); 

505 

506 
in 

507 

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

508 
fun local_theory_to_proof' loc f = begin_proof 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

509 
(fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy))) 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

510 
(fn gthy => loc_finish loc gthy o Local_Theory.reset_group); 
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

511 

24453  512 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  513 

514 
fun theory_to_proof f = begin_proof 

33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

515 
(K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))  _ => raise UNDEF)) 
42360  516 
(K (Context.Theory o Sign.reset_group o Proof_Context.theory_of)); 
21294  517 

518 
end; 

519 

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

520 
val forget_proof = transaction (fn _ => 
21007  521 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
522 
 SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

523 
 _ => raise UNDEF)); 

524 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

525 
val present_proof = present_transaction (fn _ => 
33390  526 
(fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

527 
 skip as SkipProof _ => skip 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

528 
 _ => raise UNDEF)); 
21177  529 

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

530 
fun proofs' f = transaction (fn int => 
33390  531 
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

532 
 skip as SkipProof _ => skip 
16815  533 
 _ => raise UNDEF)); 
15668  534 

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

535 
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

536 
val proofs = proofs' o K; 
6689  537 
val proof = proof' o K; 
16815  538 

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

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

541 
 _ => raise UNDEF)); 
16815  542 

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

543 
fun skip_proof f = transaction (fn _ => 
21007  544 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  545 
 _ => raise UNDEF)); 
546 

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

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

548 
(fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

549 
 _ => raise UNDEF)); 
5828  550 

551 

552 

553 
(** toplevel transactions **) 

554 

27427  555 
(* identification *) 
556 

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

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

559 

560 

25960  561 
(* thread position *) 
25799  562 

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

564 
Position.setmp_thread_data pos f x; 
25799  565 

27606  566 
fun status tr m = 
43665  567 
setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); 
27606  568 

38876
ec7045139e70
Toplevel.run_command: more careful treatment of interrupts stemming from nested multiexceptions etc.;
wenzelm
parents:
38875
diff
changeset

569 
fun error_msg tr msg = 
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44200
diff
changeset

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

571 

25799  572 

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

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

574 

37905  575 
local 
576 
val hooks = Unsynchronized.ref ([]: (transition > state > state > unit) list); 

577 
in 

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

578 

32738  579 
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f)); 
33223  580 
fun get_hooks () = ! hooks; 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

581 

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

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

583 

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

584 

5828  585 
(* apply transitions *) 
586 

6664  587 
local 
588 

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

590 
setmp_thread_position tr (fn state => 
25799  591 
let 
592 
fun do_timing f x = (warning (command_msg "" tr); timeap f x); 

593 
fun do_profiling f x = profile (! profiling) f x; 

594 

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

595 
val (result, status) = 
37905  596 
state > 
597 
(apply_trans int trans 

598 
> (! profiling > 0 andalso not no_timing) ? do_profiling 

599 
> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing); 

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

600 

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

601 
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

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

604 
in 

5828  605 

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

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

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

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

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

610 

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

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

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

613 
(case app int tr st of 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

614 
(_, SOME Runtime.TERMINATE) => NONE 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

615 
 (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info) 
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

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

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

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

619 
in res end; 
6664  620 

621 
end; 

5828  622 

623 

28425  624 
(* nested commands *) 
5828  625 

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

627 
(case transition (! interact) tr st of 
28425  628 
SOME (st', NONE) => st' 
39285  629 
 SOME (_, SOME (exn, info)) => 
630 
if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info) 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

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

632 

29483  633 
fun command_result tr st = 
634 
let val st' = command tr st 

635 
in (st', st') end; 

636 

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

637 

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

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

639 

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

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

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

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

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

645 

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

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

647 
let val st' = command tr st in 
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

648 
if immediate orelse 
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

649 
null proof_trs orelse 
36950  650 
Keyword.is_schematic_goal (name_of tr) orelse 
651 
exists (Keyword.is_qed_global o name_of) proof_trs orelse 

36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

652 
not (can proof_of st') orelse 
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

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

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

655 
let val (states, st'') = fold_map command_result proof_trs st' 
42129
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42012
diff
changeset

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

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

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

659 
val (body_trs, end_tr) = split_last proof_trs; 
42360  660 
val finish = Context.Theory o Proof_Context.theory_of; 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

661 

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

663 
(fn prf => 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41674
diff
changeset

664 
Goal.fork_name "Toplevel.future_proof" 
41673  665 
(fn () => 
666 
let val (states, result_state) = 

667 
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) 

668 
=> State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) 

669 
> fold_map command_result body_trs 

670 
> command (end_tr > set_print false); 

671 
in (states, presentation_context_of result_state) end)) 

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

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

673 

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

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

675 

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

676 
val states = 
30398  677 
(case States.get (presentation_context_of st'') of 
37852
a902f158b4fc
eliminated oldstyle sys_error/SYS_ERROR in favour of exception Fail  after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37711
diff
changeset

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

679 
 SOME states => states); 
42129
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42012
diff
changeset

680 
val result = states 
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42012
diff
changeset

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

682 

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

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

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

685 

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

688 
val end_pos = if null input then error "No input" else pos_of (fst (List.last input)); 
29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

689 
val immediate = not (Goal.future_enabled ()); 
29427
7ba952481e29
excursion: commit_exit internally  checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset

690 
val (results, end_state) = fold_map (proof_result immediate) input toplevel; 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

691 
val thy = end_theory end_pos end_state; 
42129
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42012
diff
changeset

692 
in (results, thy) end; 
7062  693 

6664  694 
end; 