tuned signature;
authorwenzelm
Tue Jun 09 12:32:01 2015 +0200 (2015-06-09 ago)
changeset 604039be917b2f376
parent 60402 2cfd1ead74c3
child 60404 422b63ef0147
tuned signature;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 12:17:50 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 12:32:01 2015 +0200
     1.3 @@ -187,7 +187,7 @@
     1.4  (* local endings *)
     1.5  
     1.6  fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
     1.7 -val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
     1.8 +val local_terminal_proof = Toplevel.proof o Proof.local_future_terminal_proof;
     1.9  val local_default_proof = Toplevel.proof Proof.local_default_proof;
    1.10  val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
    1.11  val local_done_proof = Toplevel.proof Proof.local_done_proof;
    1.12 @@ -199,7 +199,7 @@
    1.13  (* global endings *)
    1.14  
    1.15  fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
    1.16 -val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
    1.17 +val global_terminal_proof = Toplevel.end_proof o K o Proof.global_future_terminal_proof;
    1.18  val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
    1.19  val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
    1.20  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
     2.1 --- a/src/Pure/Isar/proof.ML	Tue Jun 09 12:17:50 2015 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Tue Jun 09 12:32:01 2015 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4    val enter_chain: state -> state
     2.5    val enter_backward: state -> state
     2.6    val has_bottom_goal: state -> bool
     2.7 -  val pretty_state: int -> state -> Pretty.T list
     2.8 +  val pretty_state: state -> Pretty.T list
     2.9    val refine: Method.text -> state -> state Seq.seq
    2.10    val refine_end: Method.text -> state -> state Seq.seq
    2.11    val refine_insert: thm list -> state -> state
    2.12 @@ -121,10 +121,8 @@
    2.13    val schematic_goal: state -> bool
    2.14    val is_relevant: state -> bool
    2.15    val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
    2.16 -  val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
    2.17 -    state -> state
    2.18 -  val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
    2.19 -    state -> context
    2.20 +  val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
    2.21 +  val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
    2.22  end;
    2.23  
    2.24  structure Proof: PROOF =
    2.25 @@ -362,13 +360,12 @@
    2.26  
    2.27  in
    2.28  
    2.29 -fun pretty_state nr state =
    2.30 +fun pretty_state state =
    2.31    let
    2.32      val {context = ctxt, facts, mode, goal = _} = top state;
    2.33      val verbose = Config.get ctxt Proof_Context.verbose;
    2.34  
    2.35 -    fun prt_goal (SOME (_, (_,
    2.36 -      {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
    2.37 +    fun prt_goal (SOME (_, (_, {statement = _, using, goal, before_qed = _, after_qed = _}))) =
    2.38            pretty_sep
    2.39              (pretty_facts ctxt "using"
    2.40                (if mode <> Backward orelse null using then NONE else SOME using))
    2.41 @@ -1195,7 +1192,7 @@
    2.42  
    2.43  local
    2.44  
    2.45 -fun future_terminal_proof proof1 proof2 done int state =
    2.46 +fun future_terminal_proof proof1 proof2 done state =
    2.47    if Goal.future_enabled 3 andalso not (is_relevant state) then
    2.48      state |> future_proof (fn state' =>
    2.49        let
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jun 09 12:17:50 2015 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jun 09 12:32:01 2015 +0200
     3.3 @@ -192,8 +192,7 @@
     3.4    (case try node_of state of
     3.5      NONE => []
     3.6    | SOME (Theory _) => []
     3.7 -  | SOME (Proof (prf, _)) =>
     3.8 -      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
     3.9 +  | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
    3.10    | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
    3.11  
    3.12  val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;