# HG changeset patch
# User wenzelm
# Date 1399410498 -7200
# Node ID 1ca814da47aebb4d271d2f18643922204652a37f
# Parent  87ebb99786ed02c878e560782b3ecc72de268196
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;

diff -r 87ebb99786ed -r 1ca814da47ae src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue May 06 22:55:44 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue May 06 23:08:18 2014 +0200
@@ -998,9 +998,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_state"}
     "print current proof state (if present)"
-    (opt_modes >> (fn modes =>
-      Toplevel.keep (fn state =>
-        Print_Mode.with_modes modes (Toplevel.print_state true) state)));
+    (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
 
 val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*)
   Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
@@ -1009,7 +1007,7 @@
        (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
         case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
         Toplevel.quiet := false;
-        Print_Mode.with_modes modes (Toplevel.print_state true) state))));
+        Print_Mode.with_modes modes Toplevel.print_state state))));
 
 val _ = (*Proof General legacy*)
   Outer_Syntax.improper_command @{command_spec "disable_pr"}
diff -r 87ebb99786ed -r 1ca814da47ae src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue May 06 22:55:44 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue May 06 23:08:18 2014 +0200
@@ -23,8 +23,8 @@
   val proof_position_of: state -> int
   val end_theory: Position.T -> state -> theory
   val pretty_state_context: state -> Pretty.T list
-  val pretty_state: bool -> state -> Pretty.T list
-  val print_state: bool -> state -> unit
+  val pretty_state: state -> Pretty.T list
+  val print_state: state -> unit
   val pretty_abstract: state -> Pretty.T
   val quiet: bool Unsynchronized.ref
   val interact: bool Unsynchronized.ref
@@ -207,16 +207,15 @@
   | SOME (Proof (_, (_, gthy))) => pretty_context gthy
   | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
 
-fun pretty_state prf_only state =
+fun pretty_state state =
   (case try node_of state of
     NONE => []
-  | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
+  | SOME (Theory _) => []
   | SOME (Proof (prf, _)) =>
       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
   | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
 
-fun print_state prf_only =
-  pretty_state prf_only #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
+val print_state = pretty_state #> Pretty.markup_chunks Markup.state #> Pretty.writeln;
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
@@ -592,7 +591,7 @@
 
       val (result, opt_err) =
          state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-      val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
+      val _ = if int andalso not (! quiet) andalso print then print_state result else ();
 
       val timing_result = Timing.result timing_start;
       val timing_props =
diff -r 87ebb99786ed -r 1ca814da47ae src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue May 06 22:55:44 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Tue May 06 23:08:18 2014 +0200
@@ -384,7 +384,7 @@
             val do_print =
               not is_init andalso
                 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-          in if do_print then Toplevel.print_state false st' else () end});
+          in if do_print then Toplevel.print_state st' else () end});
 
 
 (* combined execution *)
diff -r 87ebb99786ed -r 1ca814da47ae src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue May 06 22:55:44 2014 +0200
+++ b/src/Pure/System/isar.ML	Tue May 06 23:08:18 2014 +0200
@@ -60,7 +60,7 @@
 fun goal () = Proof.goal (Toplevel.proof_of (state ()))
   handle Toplevel.UNDEF => error "No goal present";
 
-fun print () = Toplevel.print_state false (state ());
+fun print () = Toplevel.print_state (state ());
 
 
 (* history navigation *)
diff -r 87ebb99786ed -r 1ca814da47ae src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Tue May 06 22:55:44 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Tue May 06 23:08:18 2014 +0200
@@ -78,7 +78,7 @@
 
 val _ =
   register "state" "proof state"
-    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state true);
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state);
 
 end;
 
diff -r 87ebb99786ed -r 1ca814da47ae src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Tue May 06 22:55:44 2014 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Tue May 06 23:08:18 2014 +0200
@@ -193,7 +193,7 @@
     (Scan.succeed (Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state
       then ProofGeneral.tell_clear_goals ()
-      else (Toplevel.quiet := false; Toplevel.print_state true state))));
+      else (Toplevel.quiet := false; Toplevel.print_state state))));
 
 val _ = (*undo without output -- historical*)
   Outer_Syntax.improper_command