show_tags flag;
authorwenzelm
Tue Dec 01 14:46:35 1998 +0100 (1998-12-01)
changeset 6000aa84c30c1f61
parent 5999 84fe61a08c17
child 6001 28b0a9891852
show_tags flag;
src/Pure/attribute.ML
     1.1 --- a/src/Pure/attribute.ML	Tue Dec 01 10:39:35 1998 +0100
     1.2 +++ b/src/Pure/attribute.ML	Tue Dec 01 14:46:35 1998 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    type tag
     1.5    type tthm
     1.6    type 'a attribute
     1.7 +  val show_tags: bool ref
     1.8  end;
     1.9  
    1.10  signature ATTRIBUTE =
    1.11 @@ -70,12 +71,14 @@
    1.12  
    1.13  (* display tagged theorems *)
    1.14  
    1.15 +val show_tags = ref false;
    1.16 +
    1.17  fun pretty_tag (name, args) = Pretty.strs (name :: args);
    1.18  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.19  
    1.20 -fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
    1.21 -  | pretty_tthm (thm, tags) = Pretty.block
    1.22 -      [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
    1.23 +fun pretty_tthm (thm, tags) =
    1.24 +  if null tags orelse not (! show_tags) then Pretty.quote (Display.pretty_thm thm)
    1.25 +  else Pretty.block [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
    1.26  
    1.27  fun pretty_tthms [th] = pretty_tthm th
    1.28    | pretty_tthms ths = Pretty.block (Pretty.fbreaks (map pretty_tthm ths));