# HG changeset patch
# User wenzelm
# Date 958669444 -7200
# Node ID 111476895bf2401ed1fc4cfa0eef281a697698c6
# Parent  19ab913a6a6aa31e1d948ec8a5a8d6384b5a36b0
print_state: flag for proof only;

diff -r 19ab913a6a6a -r 111476895bf2 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Thu May 18 18:48:55 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Thu May 18 19:04:04 2000 +0200
@@ -113,7 +113,8 @@
       val begin_state = oct_char "366";
       val end_state= oct_char "367";
     in (begin_state, end_state, "") end;
-  Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
+  Toplevel.print_state_fn := (fn x => fn y =>
+    plain_writeln (fn () => Toplevel.print_state_default x y) ());
   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default);
   Goals.print_current_goals_fn := print_current_goals);
 
diff -r 19ab913a6a6a -r 111476895bf2 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu May 18 18:48:55 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu May 18 19:04:04 2000 +0200
@@ -90,7 +90,7 @@
 
 fun pr (ms, limit) = Toplevel.keep (fn state =>
   ((case limit of Some n => goals_limit := n | None => ()); Toplevel.quiet := false;
-    with_modes ms (fn () => Toplevel.print_state state)));
+    with_modes ms (fn () => Toplevel.print_state true state)));
 
 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
diff -r 19ab913a6a6a -r 111476895bf2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu May 18 18:48:55 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu May 18 19:04:04 2000 +0200
@@ -589,7 +589,7 @@
     K.diag (P.name >> IsarCmd.kill_thy);
 
 val prP =
-  OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
+  OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
     (opt_modes -- Scan.option P.nat >> IsarCmd.pr);
 
 val disable_prP =
diff -r 19ab913a6a6a -r 111476895bf2 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu May 18 18:48:55 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu May 18 19:04:04 2000 +0200
@@ -15,9 +15,9 @@
   val prompt_state_default: state -> string
   val prompt_state_fn: (state -> string) ref
   val print_state_context: state -> unit
-  val print_state_default: state -> unit
-  val print_state_fn: (state -> unit) ref
-  val print_state: state -> unit
+  val print_state_default: bool -> state -> unit
+  val print_state_fn: (bool -> state -> unit) ref
+  val print_state: bool -> state -> unit
   exception UNDEF
   val node_history_of: state -> node History.T
   val node_of: state -> node
@@ -84,12 +84,13 @@
   [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
     Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
 
+fun print_prf prf = Proof.print_state (ProofHistory.position prf) (ProofHistory.current prf);
+
 fun print_node_ctxt (Theory thy) = print_ctxt thy
   | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf));
 
-fun print_node (Theory thy) = print_ctxt thy
-  | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf)
-      (ProofHistory.current prf);
+fun print_node prf_only (Theory thy) = if prf_only then () else print_ctxt thy
+  | print_node _ (Proof prf) = print_prf prf;
 
 
 (* datatype state *)
@@ -120,10 +121,10 @@
 
 val print_state_context = print_current_node print_node_ctxt;
 
-fun print_state_default state =
+fun print_state_default prf_only state =
   let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
     if begin_state = "" then () else writeln begin_state;
-    print_current_node print_node state;
+    print_current_node (print_node prf_only) state;
     if end_state = "" then () else writeln end_state
   end;
 
@@ -389,7 +390,7 @@
       else warning (command_msg "Interactive-only " tr);
     val (result, opt_exn) =
       (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
-    val _ = if int andalso print andalso not (! quiet) then print_state result else ();
+    val _ = if int andalso print andalso not (! quiet) then print_state false result else ();
   in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
 
 in