# HG changeset patch
# User wenzelm
# Date 1399460355 -7200
# Node ID f058120aaad4fe7cf3be741dec73d2c640cf940b
# Parent  fa12200276bf661a8016eee5348c4b78dc87017e
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;

diff -r fa12200276bf -r f058120aaad4 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Wed May 07 11:50:30 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy	Wed May 07 12:59:15 2014 +0200
@@ -133,7 +133,6 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.theory: "(theory -> theory) ->
@@ -150,10 +149,6 @@
 
   \begin{description}
 
-  \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
-  causes the toplevel loop to echo the result state (in interactive
-  mode).
-
   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   function.
 
diff -r fa12200276bf -r f058120aaad4 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Wed May 07 12:59:15 2014 +0200
@@ -336,13 +336,11 @@
 val _ =
   Outer_Syntax.command @{command_spec "pcpodef"}
     "HOLCF type definition (requires admissibility proof)"
-    (typedef_proof_decl >>
-      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
+    (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
 
 val _ =
   Outer_Syntax.command @{command_spec "cpodef"}
     "HOLCF type definition (requires admissibility proof)"
-    (typedef_proof_decl >>
-      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
+    (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
 
 end
diff -r fa12200276bf -r f058120aaad4 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Wed May 07 12:59:15 2014 +0200
@@ -212,7 +212,6 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
-    (domaindef_decl >>
-      (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
+    (domaindef_decl >> (Toplevel.theory o mk_domaindef))
 
 end
diff -r fa12200276bf -r f058120aaad4 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed May 07 12:59:15 2014 +0200
@@ -123,8 +123,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "spark_vc"}
     "enter into proof mode for a specific verification condition"
-    (Parse.name >> (fn name =>
-      (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
+    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "spark_status"}
diff -r fa12200276bf -r f058120aaad4 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Wed May 07 12:59:15 2014 +0200
@@ -666,7 +666,6 @@
 val _ =
   Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
     (Scan.repeat1 Parse.term >> (fn ts =>
-      Toplevel.print o
       Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
 
 end;
diff -r fa12200276bf -r f058120aaad4 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Wed May 07 12:59:15 2014 +0200
@@ -201,7 +201,6 @@
   Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
     (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
       Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
-      >> (fn (cos, alt_props) => Toplevel.print o
-          (Toplevel.theory_to_proof (process_spec cos alt_props))))
+      >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
 
 end
diff -r fa12200276bf -r f058120aaad4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 07 12:59:15 2014 +0200
@@ -404,14 +404,12 @@
 val _ =
   Outer_Syntax.command @{command_spec "include"}
     "include declarations from bundle in proof body"
-    (Scan.repeat1 (Parse.position Parse.xname)
-      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "including"}
     "include declarations from bundle in goal refinement"
-    (Scan.repeat1 (Parse.position Parse.xname)
-      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_bundles"}
@@ -425,7 +423,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "context"} "begin local theory context"
     ((Parse.position Parse.xname >> (fn name =>
-        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
+        Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
       --| Parse.begin);
@@ -443,7 +441,7 @@
     (Parse.binding --
       Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
-          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+          Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
 
 fun interpretation_args mandatory =
@@ -456,24 +454,20 @@
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       interpretation_args false >> (fn (loc, (expr, equations)) =>
-        Toplevel.print o
         Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
     || interpretation_args false >> (fn (expr, equations) =>
-        Toplevel.print o
         Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_spec "interpretation"}
     "prove interpretation of locale expression in local theory"
     (interpretation_args true >> (fn (expr, equations) =>
-      Toplevel.print o
       Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_spec "interpret"}
     "prove interpretation of locale expression in proof context"
     (interpretation_args true >> (fn (expr, equations) =>
-      Toplevel.print o
       Toplevel.proof' (Expression.interpret_cmd expr equations)));
 
 
@@ -488,7 +482,7 @@
   Outer_Syntax.command @{command_spec "class"} "define type class"
    (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
-        (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+        Toplevel.begin_local_theory begin
           (Class_Declaration.class_cmd I name supclasses elems #> snd)));
 
 val _ =
@@ -498,17 +492,14 @@
 val _ =
   Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
    (Parse.multi_arity --| Parse.begin
-     >> (fn arities => Toplevel.print o
-         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
+     >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
   ((Parse.class --
     ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
-    Parse.multi_arity >> Class.instance_arity_cmd)
-    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
-    Scan.succeed
-      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+    Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
+    Scan.succeed (Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
 
 (* arbitrary overloading *)
@@ -518,8 +509,7 @@
    (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
       Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
       >> Parse.triple1) --| Parse.begin
-   >> (fn operations => Toplevel.print o
-         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
+   >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 
 (* code generation *)
@@ -559,20 +549,20 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "have"} "state local goal"
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
 
 val _ =
   Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
 
 val _ =
   Outer_Syntax.command @{command_spec "show"}
     "state local goal, solving current obligation"
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
 
 val _ =
   Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
 
 
 (* facts *)
@@ -581,42 +571,42 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "then"} "forward chaining"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
+    (Scan.succeed (Toplevel.proof Proof.chain));
 
 val _ =
   Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
+    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
+    (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "note"} "define facts"
-    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
+    (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "using"} "augment goal facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
+    (facts >> (Toplevel.proof o Proof.using_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
+    (facts >> (Toplevel.proof o Proof.unfolding_cmd));
 
 
 (* proof context *)
 
 val _ =
   Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
-    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
+    (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "assume"} "assume propositions"
-    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
+    (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
-    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
+    (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
@@ -624,26 +614,26 @@
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
           ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
-    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
+    >> (Toplevel.proof o Proof.def_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
     (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
-      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
+      >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
   Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
-    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
+    (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "let"} "bind text variables"
     (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
-      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
+      >> (Toplevel.proof o Proof.let_bind_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
+    >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
 
 val _ =
   Outer_Syntax.command @{command_spec "case"} "invoke local context"
@@ -651,22 +641,22 @@
       Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
         --| @{keyword ")"}) ||
       Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
-        Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
+        Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
 
 
 (* proof structure *)
 
 val _ =
   Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
+    (Scan.succeed (Toplevel.proof Proof.begin_block));
 
 val _ =
   Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
+    (Scan.succeed (Toplevel.proof Proof.end_block));
 
 val _ =
   Outer_Syntax.command @{command_spec "next"} "enter next proof block"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
+    (Scan.succeed (Toplevel.proof Proof.next_block));
 
 
 (* end proof *)
@@ -675,61 +665,58 @@
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
     (Scan.option Method.parse >> (fn m =>
      (Option.map Method.report m;
-      Toplevel.print o Isar_Cmd.qed m)));
+      Isar_Cmd.qed m)));
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
      (Method.report m1;
       Option.map Method.report m2;
-      Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
+      Isar_Cmd.terminal_proof (m1, m2))));
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
+    (Scan.succeed Isar_Cmd.default_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "."} "immediate proof"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
+    (Scan.succeed Isar_Cmd.immediate_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "done"} "done proof"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
+    (Scan.succeed Isar_Cmd.done_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
+    (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "oops"} "forget proof"
-    (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
+    (Scan.succeed Toplevel.forget_proof);
 
 
 (* proof steps *)
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
+    (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
 
 val _ =
   Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
-    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
+    (Parse.nat >> (Toplevel.proof o Proof.prefer));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse >> (fn m =>
-      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m))));
+    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
-    (Method.parse >> (fn m =>
-      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m))));
+    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof step"
     (Scan.option Method.parse >> (fn m =>
       (Option.map Method.report m;
-        Toplevel.print o
         Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
         Toplevel.skip_proof (fn i => i + 1))));
 
@@ -741,8 +728,8 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
-    (Scan.succeed (Toplevel.print o
-      Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
+    (Scan.succeed
+     (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
       Toplevel.skip_proof (fn h => (report_back (); h))));
 
 
diff -r fa12200276bf -r f058120aaad4 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/Isar/keyword.ML	Wed May 07 12:59:15 2014 +0200
@@ -67,6 +67,7 @@
   val is_proof_goal: string -> bool
   val is_qed: string -> bool
   val is_qed_global: string -> bool
+  val is_printed: string -> bool
 end;
 
 structure Keyword: KEYWORD =
@@ -263,5 +264,7 @@
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
+val is_printed = is_theory_goal orf is_proof;
+
 end;
 
diff -r fa12200276bf -r f058120aaad4 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 07 12:59:15 2014 +0200
@@ -203,14 +203,13 @@
 
 (* local_theory commands *)
 
-fun local_theory_command do_print trans command_spec comment parse =
-  command command_spec comment (Parse.opt_target -- parse
-    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
+fun local_theory_command trans command_spec comment parse =
+  command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
 
-val local_theory' = local_theory_command false Toplevel.local_theory';
-val local_theory = local_theory_command false Toplevel.local_theory;
-val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
-val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
+val local_theory' = local_theory_command Toplevel.local_theory';
+val local_theory = local_theory_command Toplevel.local_theory;
+val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
+val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
 
 
 (* inspect syntax *)
diff -r fa12200276bf -r f058120aaad4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 07 12:59:15 2014 +0200
@@ -32,14 +32,11 @@
   val profiling: int Unsynchronized.ref
   type transition
   val empty: transition
-  val print_of: transition -> bool
   val name_of: transition -> string
   val pos_of: transition -> Position.T
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
-  val set_print: bool -> transition -> transition
-  val print: transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
@@ -316,23 +313,21 @@
  {name: string,              (*command name*)
   pos: Position.T,           (*source position*)
   int_only: bool,            (*interactive-only*)  (* TTY / Proof General legacy*)
-  print: bool,               (*print result state*)
   timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, int_only, print, timing, trans) =
-  Transition {name = name, pos = pos, int_only = int_only, print = print,
+fun make_transition (name, pos, int_only, timing, trans) =
+  Transition {name = name, pos = pos, int_only = int_only,
     timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
-  make_transition (f (name, pos, int_only, print, timing, trans));
+fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
+  make_transition (f (name, pos, int_only, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, NONE, []);
+val empty = make_transition ("", Position.none, false, NONE, []);
 
 
 (* diagnostics *)
 
-fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
 
@@ -345,25 +340,20 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
+  (name, pos, int_only, timing, trans));
 
-fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
-
-fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
+  (name, pos, int_only, timing, trans));
 
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
-  (name, pos, int_only, print, timing, tr :: trans));
+fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
+  (name, pos, int_only, timing, trans));
 
-val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
-  (name, pos, int_only, print, timing, []));
+fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
+  (name, pos, int_only, timing, tr :: trans));
 
-fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
-
-val print = set_print true;
+val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
+  (name, pos, int_only, timing, []));
 
 
 (* basic transitions *)
@@ -583,19 +573,22 @@
 (* apply transitions *)
 
 fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
-  (name, pos, int_only, print, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
+  (name, pos, int_only, timing, trans));
 
 local
 
-fun app int (tr as Transition {trans, print, ...}) =
+fun app int (tr as Transition {name, trans, ...}) =
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
 
       val (result, opt_err) =
          state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-      val _ = if int andalso not (! quiet) andalso print then print_state result else ();
+
+      val _ =
+        if int andalso not (! quiet) andalso Keyword.is_printed name
+        then print_state result else ();
 
       val timing_result = Timing.result timing_start;
       val timing_props =
@@ -743,7 +736,7 @@
                 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
 
             val st'' = st'
-              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
+              |> command (head_tr |> reset_trans |> forked_proof);
             val end_result = Result (end_tr, st'');
             val result =
               Result_List [head_result, Result.get (presentation_context_of st''), end_result];
diff -r fa12200276bf -r f058120aaad4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Wed May 07 12:59:15 2014 +0200
@@ -231,7 +231,7 @@
 
       val _ = Multithreading.interrupted ();
       val _ = status tr Markup.running;
-      val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+      val (errs1, result) = run (is_init orelse is_proof) tr st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
       val errs = errs1 @ errs2;
       val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
@@ -376,15 +376,10 @@
 val _ =
   print_function "print_state"
     (fn {command_name, ...} =>
-      SOME {delay = NONE, pri = 1, persistent = false, strict = true,
-        print_fn = fn tr => fn st' =>
-          let
-            val is_init = Keyword.is_theory_begin command_name;
-            val is_proof = Keyword.is_proof command_name;
-            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 st' else () end});
+      if Keyword.is_printed command_name then
+        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+          print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
+      else NONE);
 
 
 (* combined execution *)
diff -r fa12200276bf -r f058120aaad4 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed May 07 12:59:15 2014 +0200
@@ -200,7 +200,7 @@
     val channel = rendezvous ();
     val msg_channel = init_channels channel;
     val _ = Session.init_protocol_handlers ();
-    val _ = loop channel;
+    val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel;
   in Message_Channel.shutdown msg_channel end);
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
diff -r fa12200276bf -r f058120aaad4 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/pure_syn.ML	Wed May 07 12:59:15 2014 +0200
@@ -11,9 +11,8 @@
   Outer_Syntax.command
     (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
     (Thy_Header.args >> (fn header =>
-      Toplevel.print o
-        Toplevel.init_theory
-          (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
+      Toplevel.init_theory
+        (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
 
 val _ =
   Outer_Syntax.command