# HG changeset patch
# User wenzelm
# Date 1408701947 -7200
# Node ID e92cdae8b3b5981dc394ccabd9ae4012433719da
# Parent  b2b93903ab6b5108d5fcf22066f91275c52755d0
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;

diff -r b2b93903ab6b -r e92cdae8b3b5 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Aug 22 11:31:19 2014 +0200
+++ b/src/Pure/General/binding.ML	Fri Aug 22 12:05:47 2014 +0200
@@ -31,6 +31,7 @@
   val conceal: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
+  val pp: binding -> Pretty.T
   val bad: binding -> string
   val check: binding -> unit
 end;
@@ -133,6 +134,8 @@
 
 val print = Pretty.str_of o pretty;
 
+val pp = pretty o set_pos Position.none;
+
 
 (* check *)
 
diff -r b2b93903ab6b -r e92cdae8b3b5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Aug 22 11:31:19 2014 +0200
+++ b/src/Pure/ROOT.ML	Fri Aug 22 12:05:47 2014 +0200
@@ -343,7 +343,7 @@
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
+toplevel_pp ["Binding", "binding"] "Binding.pp";
 toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
 toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
 toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";