--- 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 ***
--- 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"
--- 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"
--- 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
--- 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}.
*}
--- 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"
--- 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))) @
--- 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
--- 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"