clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
authorwenzelm
Fri Aug 22 12:05:47 2014 +0200 (2014-08-22)
changeset 58032e92cdae8b3b5
parent 58031 b2b93903ab6b
child 58033 154ae20ead35
child 58036 f23045003476
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
src/Pure/General/binding.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/binding.ML	Fri Aug 22 11:31:19 2014 +0200
     1.2 +++ b/src/Pure/General/binding.ML	Fri Aug 22 12:05:47 2014 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val conceal: binding -> binding
     1.5    val pretty: binding -> Pretty.T
     1.6    val print: binding -> string
     1.7 +  val pp: binding -> Pretty.T
     1.8    val bad: binding -> string
     1.9    val check: binding -> unit
    1.10  end;
    1.11 @@ -133,6 +134,8 @@
    1.12  
    1.13  val print = Pretty.str_of o pretty;
    1.14  
    1.15 +val pp = pretty o set_pos Position.none;
    1.16 +
    1.17  
    1.18  (* check *)
    1.19  
     2.1 --- a/src/Pure/ROOT.ML	Fri Aug 22 11:31:19 2014 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Fri Aug 22 12:05:47 2014 +0200
     2.3 @@ -343,7 +343,7 @@
     2.4  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
     2.5  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
     2.6  toplevel_pp ["Position", "T"] "Pretty.position";
     2.7 -toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
     2.8 +toplevel_pp ["Binding", "binding"] "Binding.pp";
     2.9  toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
    2.10  toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
    2.11  toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";