# HG changeset patch
# User wenzelm
# Date 938026952 -7200
# Node ID e1e2d07287d8e5546275f6a55eed0a0bce890b0d
# Parent  5bcb7fc31caa6ca3bc05eb0ea53a7db43c59f4a3
improved output;

diff -r 5bcb7fc31caa -r e1e2d07287d8 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 22 20:59:22 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 22 21:02:32 1999 +0200
@@ -289,32 +289,35 @@
 
 fun print_facts _ None = ()
   | print_facts s (Some ths) =
-      Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
+     (Pretty.writeln (Pretty.big_list (s ^ "this:") (map pretty_thm ths)); writeln "");
 
 fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) =
   let
     val ref (_, _, begin_goal) = Goals.current_goals_markers;
 
     fun levels_up 0 = ""
-      | levels_up 1 = " (1 level up)"
-      | levels_up i = " (" ^ string_of_int i ^ " levels up)";
+      | levels_up 1 = ", 1 level up"
+      | levels_up i = ", " ^ string_of_int i ^ " levels up";
 
     fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
-      (print_facts "Using"
+      (print_facts "using "
           (if mode <> Backward orelse null goal_facts then None else Some goal_facts);
-        writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
+        writeln ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^
+          levels_up (i div 2) ^ "):");
         Locale.print_goals_marker begin_goal (! goals_limit) thm);
 
-    val ctxt_strings = ProofContext.strings_of_context context;
+    val ctxt_strings =
+      if ! verbose orelse mode = Forward then ProofContext.strings_of_context context
+      else if mode = Backward then ProofContext.strings_of_prems context
+      else [];
   in
     writeln ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
       ", depth " ^ string_of_int (length nodes div 2));
     writeln "";
+    if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
     if ! verbose orelse mode = Forward then
-      (if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
-        print_facts "Current" facts;
-        print_goal (find_goal 0 state))
-    else if mode = ForwardChain then print_facts "Picking" facts
+      (print_facts "" facts; print_goal (find_goal 0 state))
+    else if mode = ForwardChain then print_facts "picking " facts
     else print_goal (find_goal 0 state)
   end;
 
diff -r 5bcb7fc31caa -r e1e2d07287d8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Sep 22 20:59:22 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 22 21:02:32 1999 +0200
@@ -17,6 +17,7 @@
   val verbose: bool ref
   val print_binds: context -> unit
   val print_thms: context -> unit
+  val strings_of_prems: context -> string list
   val strings_of_context: context -> string list
   val print_proof_data: theory -> unit
   val init: theory -> context
@@ -112,7 +113,10 @@
 (** print context information **)
 
 val show_hyps = ref false;
-fun pretty_thm th = setmp Display.show_hyps (! show_hyps) Display.pretty_thm th;
+
+fun pretty_thm thm =
+  if ! show_hyps then setmp Display.show_hyps true Display.pretty_thm_no_quote thm
+  else Display.pretty_cterm (#prop (Thm.crep_thm thm));
 
 val verbose = ref false;
 fun verb f x = if ! verbose then f x else [];
@@ -130,13 +134,13 @@
 
 (* term bindings *)
 
-fun strings_of_binds (Context {thy, binds, ...}) =
+fun strings_of_binds (ctxt as Context {binds, ...}) =
   let
-    val prt_term = Sign.pretty_term (Theory.sign_of thy);
+    val prt_term = Sign.pretty_term (sign_of ctxt);
     fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
   in
     if Vartab.is_empty binds andalso not (! verbose) then []
-    else [Pretty.string_of (Pretty.big_list "Term bindings:"
+    else [Pretty.string_of (Pretty.big_list "term bindings:"
       (map pretty_bind (Vartab.dest binds)))]
   end;
 
@@ -146,18 +150,22 @@
 (* local theorems *)
 
 fun strings_of_thms (Context {thms, ...}) =
-  strings_of_items pretty_thm "Local theorems:" (Symtab.dest thms);
+  strings_of_items pretty_thm "local theorems:" (Symtab.dest thms);
 
 val print_thms = seq writeln o strings_of_thms;
 
 
 (* main context *)
 
-fun strings_of_context (ctxt as Context {thy, data = _, asms = (_, (fixes, _)), binds = _,
-    thms = _, defs = (types, sorts, maxidx, used)}) =
+fun strings_of_prems ctxt =
+  (case prems_of ctxt of
+    [] => []
+  | prems => [Pretty.string_of (Pretty.big_list "prems:" (map pretty_thm prems))]);
+
+fun strings_of_context (ctxt as Context {asms = (_, (fixes, _)),
+    defs = (types, sorts, maxidx, used), ...}) =
   let
-    val sign = Theory.sign_of thy;
-    val prems = prems_of ctxt;
+    val sign = sign_of ctxt;
 
     val prt_term = Sign.pretty_term sign;
     val prt_typ = Sign.pretty_typ sign;
@@ -167,7 +175,7 @@
     val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
 
     (*fixes*)
-    fun prt_fixes xs = Pretty.block (Pretty.str "Fixed variables:" :: Pretty.brk 1 ::
+    fun prt_fixes xs = Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
       Pretty.commas (map (fn (x, x') => Pretty.str (x ^ " = " ^ x')) xs));
 
 
@@ -186,17 +194,14 @@
     val prt_defS = prt_atom prt_varT prt_sort;
   in
     verb_string pretty_thy @
-    (if null fixes andalso not (! verbose) then []
-      else [Pretty.string_of (prt_fixes (rev fixes))]) @
-    (if null prems andalso not (! verbose) then []
-      else [Pretty.string_of (Pretty.big_list "Assumptions:"
-        (map (prt_term o #prop o Thm.rep_thm) prems))]) @
+    (if null fixes then [] else [Pretty.string_of (prt_fixes (rev fixes))]) @
+    strings_of_prems ctxt @
     verb strings_of_binds ctxt @
     verb strings_of_thms ctxt @
-    verb_string (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types))) @
-    verb_string (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts))) @
-    verb_string (Pretty.str ("Maxidx: " ^ string_of_int maxidx)) @
-    verb_string (Pretty.strs ("Used type variable names:" :: used))
+    verb_string (Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
+    verb_string (Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @
+    verb_string (Pretty.str ("maxidx: " ^ string_of_int maxidx)) @
+    verb_string (Pretty.strs ("used type variable names:" :: used))
   end;
 
 
@@ -298,11 +303,8 @@
 (** prepare types **)
 
 fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s =
-  let
-    val sign = sign_of ctxt;
-    fun def_sort xi = Vartab.lookup (sorts, xi);
-  in
-    transform_error (Sign.read_typ (sign, def_sort)) s
+  let fun def_sort xi = Vartab.lookup (sorts, xi) in
+    transform_error (Sign.read_typ (sign_of ctxt, def_sort)) s
       handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)
   end;
 
@@ -425,8 +427,6 @@
 
 fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
   let
-    val sign = sign_of ctxt;
-
     fun def_type xi =
       (case Vartab.lookup (types, xi) of
         None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
@@ -434,7 +434,7 @@
 
     fun def_sort xi = Vartab.lookup (sorts, xi);
   in
-    (transform_error (read sign (def_type, def_sort, used)) s
+    (transform_error (read (sign_of ctxt) (def_type, def_sort, used)) s
       handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
       | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
     |> app (intern_skolem ctxt true)
@@ -642,10 +642,9 @@
 fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
   let
     val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
-    val sign = sign_of ctxt';
     val Context {defs = (_, _, maxidx, _), ...} = ctxt';
 
-    val cprops = map (Thm.cterm_of sign) props;
+    val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
     val cprops_tac = map (rpair tac) cprops;
     val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops;