added depth_of;
authorwenzelm
Wed Jun 22 19:41:27 2005 +0200 (2005-06-22)
changeset 1653960adb8b28377
parent 16538 7318c205a67f
child 16540 e3d61eff7c12
added depth_of;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jun 22 19:41:24 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jun 22 19:41:27 2005 +0200
     1.3 @@ -40,10 +40,11 @@
     1.4    val assert_forward_or_chain: state -> state
     1.5    val assert_backward: state -> state
     1.6    val assert_no_chain: state -> state
     1.7 -  val atp_hook: (ProofContext.context * Thm.thm -> unit) ref
     1.8 +  val atp_hook: (context * thm -> unit) ref
     1.9    val enter_forward: state -> state
    1.10 +  val show_main_goal: bool ref
    1.11    val verbose: bool ref
    1.12 -  val show_main_goal: bool ref
    1.13 +  val depth_of: state -> int
    1.14    val pretty_state: int -> state -> Pretty.T list
    1.15    val pretty_goals: bool -> state -> Pretty.T list
    1.16    val level: state -> int
    1.17 @@ -382,8 +383,10 @@
    1.18  (** pretty_state **)
    1.19  
    1.20  val show_main_goal = ref false;
    1.21 +val verbose = ProofContext.verbose;
    1.22  
    1.23 -val verbose = ProofContext.verbose;
    1.24 +
    1.25 +fun depth_of (State (_, nodes)) = length nodes div 2 - 1;
    1.26  
    1.27  val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp;
    1.28  
    1.29 @@ -391,7 +394,7 @@
    1.30    | pretty_facts s ctxt (SOME ths) =
    1.31        [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
    1.32  
    1.33 -fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) =
    1.34 +fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, _)) =
    1.35    let
    1.36      val ref (_, _, begin_goal) = Display.current_goals_markers;
    1.37  
    1.38 @@ -422,7 +425,7 @@
    1.39  
    1.40      val prts =
    1.41       [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.42 -        (if ! verbose then ", depth " ^ string_of_int (length nodes div 2 - 1)
    1.43 +        (if ! verbose then ", depth " ^ string_of_int (depth_of state)
    1.44          else "")), Pretty.str ""] @
    1.45       (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
    1.46       (if ! verbose orelse mode = Forward then