improved output;
authorwenzelm
Wed Sep 22 21:02:32 1999 +0200 (1999-09-22)
changeset 7575e1e2d07287d8
parent 7574 5bcb7fc31caa
child 7576 594f09166c38
improved output;
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Sep 22 20:59:22 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Sep 22 21:02:32 1999 +0200
     1.3 @@ -289,32 +289,35 @@
     1.4  
     1.5  fun print_facts _ None = ()
     1.6    | print_facts s (Some ths) =
     1.7 -      Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
     1.8 +     (Pretty.writeln (Pretty.big_list (s ^ "this:") (map pretty_thm ths)); writeln "");
     1.9  
    1.10  fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) =
    1.11    let
    1.12      val ref (_, _, begin_goal) = Goals.current_goals_markers;
    1.13  
    1.14      fun levels_up 0 = ""
    1.15 -      | levels_up 1 = " (1 level up)"
    1.16 -      | levels_up i = " (" ^ string_of_int i ^ " levels up)";
    1.17 +      | levels_up 1 = ", 1 level up"
    1.18 +      | levels_up i = ", " ^ string_of_int i ^ " levels up";
    1.19  
    1.20      fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
    1.21 -      (print_facts "Using"
    1.22 +      (print_facts "using "
    1.23            (if mode <> Backward orelse null goal_facts then None else Some goal_facts);
    1.24 -        writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
    1.25 +        writeln ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^
    1.26 +          levels_up (i div 2) ^ "):");
    1.27          Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.28  
    1.29 -    val ctxt_strings = ProofContext.strings_of_context context;
    1.30 +    val ctxt_strings =
    1.31 +      if ! verbose orelse mode = Forward then ProofContext.strings_of_context context
    1.32 +      else if mode = Backward then ProofContext.strings_of_prems context
    1.33 +      else [];
    1.34    in
    1.35      writeln ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    1.36        ", depth " ^ string_of_int (length nodes div 2));
    1.37      writeln "";
    1.38 +    if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
    1.39      if ! verbose orelse mode = Forward then
    1.40 -      (if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
    1.41 -        print_facts "Current" facts;
    1.42 -        print_goal (find_goal 0 state))
    1.43 -    else if mode = ForwardChain then print_facts "Picking" facts
    1.44 +      (print_facts "" facts; print_goal (find_goal 0 state))
    1.45 +    else if mode = ForwardChain then print_facts "picking " facts
    1.46      else print_goal (find_goal 0 state)
    1.47    end;
    1.48  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 22 20:59:22 1999 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Sep 22 21:02:32 1999 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    val verbose: bool ref
     2.5    val print_binds: context -> unit
     2.6    val print_thms: context -> unit
     2.7 +  val strings_of_prems: context -> string list
     2.8    val strings_of_context: context -> string list
     2.9    val print_proof_data: theory -> unit
    2.10    val init: theory -> context
    2.11 @@ -112,7 +113,10 @@
    2.12  (** print context information **)
    2.13  
    2.14  val show_hyps = ref false;
    2.15 -fun pretty_thm th = setmp Display.show_hyps (! show_hyps) Display.pretty_thm th;
    2.16 +
    2.17 +fun pretty_thm thm =
    2.18 +  if ! show_hyps then setmp Display.show_hyps true Display.pretty_thm_no_quote thm
    2.19 +  else Display.pretty_cterm (#prop (Thm.crep_thm thm));
    2.20  
    2.21  val verbose = ref false;
    2.22  fun verb f x = if ! verbose then f x else [];
    2.23 @@ -130,13 +134,13 @@
    2.24  
    2.25  (* term bindings *)
    2.26  
    2.27 -fun strings_of_binds (Context {thy, binds, ...}) =
    2.28 +fun strings_of_binds (ctxt as Context {binds, ...}) =
    2.29    let
    2.30 -    val prt_term = Sign.pretty_term (Theory.sign_of thy);
    2.31 +    val prt_term = Sign.pretty_term (sign_of ctxt);
    2.32      fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
    2.33    in
    2.34      if Vartab.is_empty binds andalso not (! verbose) then []
    2.35 -    else [Pretty.string_of (Pretty.big_list "Term bindings:"
    2.36 +    else [Pretty.string_of (Pretty.big_list "term bindings:"
    2.37        (map pretty_bind (Vartab.dest binds)))]
    2.38    end;
    2.39  
    2.40 @@ -146,18 +150,22 @@
    2.41  (* local theorems *)
    2.42  
    2.43  fun strings_of_thms (Context {thms, ...}) =
    2.44 -  strings_of_items pretty_thm "Local theorems:" (Symtab.dest thms);
    2.45 +  strings_of_items pretty_thm "local theorems:" (Symtab.dest thms);
    2.46  
    2.47  val print_thms = seq writeln o strings_of_thms;
    2.48  
    2.49  
    2.50  (* main context *)
    2.51  
    2.52 -fun strings_of_context (ctxt as Context {thy, data = _, asms = (_, (fixes, _)), binds = _,
    2.53 -    thms = _, defs = (types, sorts, maxidx, used)}) =
    2.54 +fun strings_of_prems ctxt =
    2.55 +  (case prems_of ctxt of
    2.56 +    [] => []
    2.57 +  | prems => [Pretty.string_of (Pretty.big_list "prems:" (map pretty_thm prems))]);
    2.58 +
    2.59 +fun strings_of_context (ctxt as Context {asms = (_, (fixes, _)),
    2.60 +    defs = (types, sorts, maxidx, used), ...}) =
    2.61    let
    2.62 -    val sign = Theory.sign_of thy;
    2.63 -    val prems = prems_of ctxt;
    2.64 +    val sign = sign_of ctxt;
    2.65  
    2.66      val prt_term = Sign.pretty_term sign;
    2.67      val prt_typ = Sign.pretty_typ sign;
    2.68 @@ -167,7 +175,7 @@
    2.69      val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
    2.70  
    2.71      (*fixes*)
    2.72 -    fun prt_fixes xs = Pretty.block (Pretty.str "Fixed variables:" :: Pretty.brk 1 ::
    2.73 +    fun prt_fixes xs = Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
    2.74        Pretty.commas (map (fn (x, x') => Pretty.str (x ^ " = " ^ x')) xs));
    2.75  
    2.76  
    2.77 @@ -186,17 +194,14 @@
    2.78      val prt_defS = prt_atom prt_varT prt_sort;
    2.79    in
    2.80      verb_string pretty_thy @
    2.81 -    (if null fixes andalso not (! verbose) then []
    2.82 -      else [Pretty.string_of (prt_fixes (rev fixes))]) @
    2.83 -    (if null prems andalso not (! verbose) then []
    2.84 -      else [Pretty.string_of (Pretty.big_list "Assumptions:"
    2.85 -        (map (prt_term o #prop o Thm.rep_thm) prems))]) @
    2.86 +    (if null fixes then [] else [Pretty.string_of (prt_fixes (rev fixes))]) @
    2.87 +    strings_of_prems ctxt @
    2.88      verb strings_of_binds ctxt @
    2.89      verb strings_of_thms ctxt @
    2.90 -    verb_string (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types))) @
    2.91 -    verb_string (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts))) @
    2.92 -    verb_string (Pretty.str ("Maxidx: " ^ string_of_int maxidx)) @
    2.93 -    verb_string (Pretty.strs ("Used type variable names:" :: used))
    2.94 +    verb_string (Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
    2.95 +    verb_string (Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @
    2.96 +    verb_string (Pretty.str ("maxidx: " ^ string_of_int maxidx)) @
    2.97 +    verb_string (Pretty.strs ("used type variable names:" :: used))
    2.98    end;
    2.99  
   2.100  
   2.101 @@ -298,11 +303,8 @@
   2.102  (** prepare types **)
   2.103  
   2.104  fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s =
   2.105 -  let
   2.106 -    val sign = sign_of ctxt;
   2.107 -    fun def_sort xi = Vartab.lookup (sorts, xi);
   2.108 -  in
   2.109 -    transform_error (Sign.read_typ (sign, def_sort)) s
   2.110 +  let fun def_sort xi = Vartab.lookup (sorts, xi) in
   2.111 +    transform_error (Sign.read_typ (sign_of ctxt, def_sort)) s
   2.112        handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)
   2.113    end;
   2.114  
   2.115 @@ -425,8 +427,6 @@
   2.116  
   2.117  fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
   2.118    let
   2.119 -    val sign = sign_of ctxt;
   2.120 -
   2.121      fun def_type xi =
   2.122        (case Vartab.lookup (types, xi) of
   2.123          None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
   2.124 @@ -434,7 +434,7 @@
   2.125  
   2.126      fun def_sort xi = Vartab.lookup (sorts, xi);
   2.127    in
   2.128 -    (transform_error (read sign (def_type, def_sort, used)) s
   2.129 +    (transform_error (read (sign_of ctxt) (def_type, def_sort, used)) s
   2.130        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   2.131        | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   2.132      |> app (intern_skolem ctxt true)
   2.133 @@ -642,10 +642,9 @@
   2.134  fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
   2.135    let
   2.136      val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
   2.137 -    val sign = sign_of ctxt';
   2.138      val Context {defs = (_, _, maxidx, _), ...} = ctxt';
   2.139  
   2.140 -    val cprops = map (Thm.cterm_of sign) props;
   2.141 +    val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
   2.142      val cprops_tac = map (rpair tac) cprops;
   2.143      val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops;
   2.144