src/Pure/Isar/toplevel.ML
changeset 28453 06702e7acd1d
parent 28451 0586b855c2b5
child 28458 0966ac3f4a40
equal deleted inserted replaced
28452:a72670460833 28453:06702e7acd1d
   453   (name, pos, int_only, print, no_timing, tr :: trans));
   453   (name, pos, int_only, print, no_timing, tr :: trans));
   454 
   454 
   455 val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
   455 val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
   456   (name, pos, int_only, print, no_timing, []));
   456   (name, pos, int_only, print, no_timing, []));
   457 
   457 
   458 val print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
   458 fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
   459   (name, pos, int_only, true, no_timing, trans));
   459   (name, pos, int_only, print, no_timing, trans));
       
   460 
       
   461 val print = set_print true;
   460 
   462 
   461 
   463 
   462 (* basic transitions *)
   464 (* basic transitions *)
   463 
   465 
   464 fun init_theory name f exit = add_trans (Init (name, f, exit));
   466 fun init_theory name f exit = add_trans (Init (name, f, exit));
   694   let val st' = command tr st
   696   let val st' = command tr st
   695   in (st', st') end;
   697   in (st', st') end;
   696 
   698 
   697 fun unit_result immediate (tr, proof_trs) st =
   699 fun unit_result immediate (tr, proof_trs) st =
   698   let val st' = command tr st in
   700   let val st' = command tr st in
   699     if not immediate andalso not (null proof_trs) andalso
   701     if immediate orelse null proof_trs orelse
   700       can proof_of st' andalso Proof.can_defer (proof_of st')
   702       not (can proof_of st') orelse Proof.is_relevant (proof_of st')
   701     then
   703     then
       
   704       let val (states, st'') = fold_map command_result proof_trs st'
       
   705       in (fn () => (tr, st') :: (proof_trs ~~ states), st'') end
       
   706     else
   702       let
   707       let
   703         val (body_trs, end_tr) = split_last proof_trs;
   708         val (body_trs, end_tr) = split_last proof_trs;
   704         val body_states = ref ([]: state list);
   709         val body_states = ref ([]: state list);
       
   710         val finish = Context.Theory o ProofContext.theory_of;
   705         fun make_result prf =
   711         fun make_result prf =
   706           let val (states, result_state) =
   712           let val (states, State (result_node, _)) =
   707             (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
   713             (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
   708               => State (SOME (Proof (ProofNode.init prf, (Context.Proof, orig_gthy)), exit), prev))
   714               => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
   709             |> fold_map command_result body_trs ||> command end_tr
   715             |> fold_map command_result body_trs
   710           in body_states := states; context_of result_state end;
   716             ||> command (end_tr |> set_print false)
   711         val proof_future =
   717           in body_states := states; presentation_context (Option.map #1 result_node) NONE end;
   712           end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result));
   718         val st'' = st'
   713         val st'' = command proof_future st';
   719           |> command (end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result)));
   714       in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
   720       in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
   715     else
       
   716       let val (states, st'') = fold_map command_result proof_trs st'
       
   717       in (fn () => (tr, st') :: (proof_trs ~~ states), st'') end
       
   718   end;
   721   end;
   719 
   722 
   720 fun excursion input =
   723 fun excursion input =
   721   let
   724   let
   722     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
   725     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));