clarified Toplevel.element_result: scheduling policies happen here;
authorwenzelm
Mon Feb 25 12:52:27 2013 +0100 (2013-02-25 ago)
changeset 51273d54ee0cad2ab
parent 51272 9c8d63b4b6be
child 51274 cfc83ad52571
clarified Toplevel.element_result: scheduling policies happen here;
tuned;
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:17:50 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4    val put_timing: Time.time -> transition -> transition
     1.5    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.6    val command: transition -> state -> state
     1.7 -  val proof_result: bool -> transition * transition list -> state ->
     1.8 +  val element_result: transition Thy_Syntax.element -> state ->
     1.9      (transition * state) list future * state
    1.10  end;
    1.11  
    1.12 @@ -694,10 +694,6 @@
    1.13        if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.14    | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.15  
    1.16 -fun command_result tr st =
    1.17 -  let val st' = command tr st
    1.18 -  in ((tr, st'), st') end;
    1.19 -
    1.20  
    1.21  (* scheduled proof result *)
    1.22  
    1.23 @@ -708,13 +704,27 @@
    1.24    fun init _ = empty;
    1.25  );
    1.26  
    1.27 -fun proof_result immediate (tr, proof_trs) st =
    1.28 -  let val st' = command tr st in
    1.29 -    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
    1.30 -      Proof.is_relevant (proof_of st')
    1.31 +fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.32 +  let
    1.33 +    val future_enabled = Goal.future_enabled ();
    1.34 +
    1.35 +    fun atom_result tr st =
    1.36 +      let val st' = command tr st
    1.37 +      in ((tr, st'), st') end;
    1.38 +
    1.39 +    val proof_trs =
    1.40 +      (case opt_proof of
    1.41 +        NONE => []
    1.42 +      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
    1.43 +
    1.44 +    val st' = command head_tr st;
    1.45 +  in
    1.46 +    if not future_enabled orelse is_ignored head_tr orelse
    1.47 +      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
    1.48 +      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.49      then
    1.50 -      let val (results, st'') = fold_map command_result proof_trs st'
    1.51 -      in (Future.value ((tr, st') :: results), st'') end
    1.52 +      let val (results, st'') = fold_map atom_result proof_trs st'
    1.53 +      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
    1.54      else
    1.55        let
    1.56          val (body_trs, end_tr) = split_last proof_trs;
    1.57 @@ -732,15 +742,15 @@
    1.58                  let val (result, result_state) =
    1.59                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.60                      => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.61 -                  |> fold_map command_result body_trs ||> command end_tr;
    1.62 +                  |> fold_map atom_result body_trs ||> command end_tr;
    1.63                  in (result, presentation_context_of result_state) end))
    1.64            #-> Result.put;
    1.65  
    1.66          val st'' = st'
    1.67 -          |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.68 +          |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.69          val result =
    1.70            Result.get (presentation_context_of st'')
    1.71 -          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
    1.72 +          |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
    1.73  
    1.74        in (result, st'') end
    1.75    end;
     2.1 --- a/src/Pure/Thy/thy_load.ML	Mon Feb 25 12:17:50 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Feb 25 12:52:27 2013 +0100
     2.3 @@ -216,8 +216,6 @@
     2.4  
     2.5  fun excursion last_timing init elements =
     2.6    let
     2.7 -    val immediate = not (Goal.future_enabled ());
     2.8 -
     2.9      fun prepare_span span =
    2.10        Thy_Syntax.span_content span
    2.11        |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
    2.12 @@ -226,28 +224,16 @@
    2.13  
    2.14      fun element_result span_elem (st, _) =
    2.15        let
    2.16 -        val tr_elem = Thy_Syntax.map_element prepare_span span_elem;
    2.17 -        val Thy_Syntax.Element (tr, opt_proof) = tr_elem;
    2.18 -        val proof_trs =
    2.19 -          (case opt_proof of
    2.20 -            NONE => []
    2.21 -          | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out Toplevel.is_ignored);
    2.22 -
    2.23 -        val elems =
    2.24 -          if Toplevel.is_ignored tr then map (rpair []) proof_trs
    2.25 -          else if Keyword.is_schematic_goal (Toplevel.name_of tr)
    2.26 -          then map (rpair []) (tr :: proof_trs)
    2.27 -          else [(tr, proof_trs)];
    2.28 -
    2.29 -        val (results, st') = fold_map (Toplevel.proof_result immediate) elems st;
    2.30 -        val pos' = Toplevel.pos_of (Thy_Syntax.last_element tr_elem);
    2.31 +        val elem = Thy_Syntax.map_element prepare_span span_elem;
    2.32 +        val (results, st') = Toplevel.element_result elem st;
    2.33 +        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
    2.34        in (results, (st', pos')) end;
    2.35  
    2.36      val (results, (end_state, end_pos)) =
    2.37        fold_map element_result elements (Toplevel.toplevel, Position.none);
    2.38  
    2.39      val thy = Toplevel.end_theory end_pos end_state;
    2.40 -  in (flat results, thy) end;
    2.41 +  in (results, thy) end;
    2.42  
    2.43  fun load_thy last_timing update_time master_dir header text_pos text parents =
    2.44    let