# HG changeset patch
# User wenzelm
# Date 1403877896 -7200
# Node ID e721124f1b1ebb3dd55fd4e1b7cd0bcdf827d39f
# Parent  fe1be2844fda1ae1de044a720ff49302b6d25681
command 'print_term_bindings' supersedes 'print_binds';

diff -r fe1be2844fda -r e721124f1b1e NEWS
--- a/NEWS	Fri Jun 27 15:41:26 2014 +0200
+++ b/NEWS	Fri Jun 27 16:04:56 2014 +0200
@@ -205,6 +205,9 @@
 (only makes sense in practice, if outer syntax is delimited
 differently).
 
+* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
+but the latter is retained some time as Proof General legacy.
+
 
 *** HOL ***
 
diff -r fe1be2844fda -r e721124f1b1e etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Jun 27 15:41:26 2014 +0200
+++ b/etc/isar-keywords-ZF.el	Fri Jun 27 16:04:56 2014 +0200
@@ -147,6 +147,7 @@
     "print_statement"
     "print_syntax"
     "print_tcset"
+    "print_term_bindings"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -316,6 +317,7 @@
     "print_statement"
     "print_syntax"
     "print_tcset"
+    "print_term_bindings"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
diff -r fe1be2844fda -r e721124f1b1e etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Jun 27 15:41:26 2014 +0200
+++ b/etc/isar-keywords.el	Fri Jun 27 16:04:56 2014 +0200
@@ -213,6 +213,7 @@
     "print_state"
     "print_statement"
     "print_syntax"
+    "print_term_bindings"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -445,6 +446,7 @@
     "print_state"
     "print_statement"
     "print_syntax"
+    "print_term_bindings"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
diff -r fe1be2844fda -r e721124f1b1e src/Doc/Isar_Ref/Misc.thy
--- a/src/Doc/Isar_Ref/Misc.thy	Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Doc/Isar_Ref/Misc.thy	Fri Jun 27 16:04:56 2014 +0200
@@ -17,7 +17,7 @@
     @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
-    @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
   @{rail \<open>
@@ -63,8 +63,8 @@
   current context, both named and unnamed ones; the ``@{text "!"}''
   option indicates extra verbosity.
   
-  \item @{command "print_binds"} prints all term abbreviations
-  present in the context.
+  \item @{command "print_term_bindings"} prints all term bindings that
+  are present in the context.
 
   \item @{command "find_theorems"}~@{text criteria} retrieves facts
   from the theory or proof context matching all of given search
diff -r fe1be2844fda -r e721124f1b1e src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri Jun 27 16:04:56 2014 +0200
@@ -960,8 +960,8 @@
   The \emph{Query} panel in \emph{Print Context} mode prints information from
   the theory or proof context, or proof state. See also the Isar commands
   @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
-  print_binds}, @{command_ref print_theorems}, @{command_ref print_state} in
-  \cite{isabelle-isar-ref}.
+  print_term_bindings}, @{command_ref print_theorems},
+  @{command_ref print_state} in \cite{isabelle-isar-ref}.
 *}
 
 
diff -r fe1be2844fda -r e721124f1b1e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 27 16:04:56 2014 +0200
@@ -897,9 +897,18 @@
     (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
+  Outer_Syntax.improper_command @{command_spec "print_binds"}
+    "print term bindings of proof context -- Proof General legacy"
     (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_binds o Toplevel.context_of)));
+      Toplevel.keep
+        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
+
+val _ =
+  Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
+    "print term bindings of proof context"
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep
+        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
diff -r fe1be2844fda -r e721124f1b1e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Jun 27 16:04:56 2014 +0200
@@ -161,7 +161,7 @@
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
-  val pretty_binds: Proof.context -> Pretty.T list
+  val pretty_term_bindings: Proof.context -> Pretty.T list
   val pretty_local_facts: Proof.context -> bool -> Pretty.T list
   val print_local_facts: Proof.context -> bool -> unit
   val pretty_cases: Proof.context -> Pretty.T list
@@ -1257,7 +1257,7 @@
 
 (* term bindings *)
 
-fun pretty_binds ctxt =
+fun pretty_term_bindings ctxt =
   let
     val binds = Variable.binds_of ctxt;
     fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t));
@@ -1408,7 +1408,7 @@
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @
     verb (pretty_abbrevs false) (K ctxt) @
-    verb pretty_binds (K ctxt) @
+    verb pretty_term_bindings (K ctxt) @
     verb (pretty_local_facts ctxt) (K true) @
     verb pretty_cases (K ctxt) @
     verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
diff -r fe1be2844fda -r e721124f1b1e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Pure/Pure.thy	Fri Jun 27 16:04:56 2014 +0200
@@ -85,10 +85,9 @@
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
-    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts"
-    "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
-    "term" "typ" "print_codesetup" "unused_thms"
-    :: diag
+    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
+    "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
+    "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
   and "cd" :: control
   and "pwd" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
diff -r fe1be2844fda -r e721124f1b1e src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Fri Jun 27 16:04:56 2014 +0200
@@ -70,7 +70,7 @@
 
 val _ =
   register "terms" "term bindings of proof context"
-    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
+    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of);
 
 val _ =
   register "theorems" "theorems of local theory or proof context"