Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
show_tags flag;
authorwenzelm
Tue, 01 Dec 1998 14:46:35 +0100
changeset 6000 aa84c30c1f61
parent 5999 84fe61a08c17
child 6001 28b0a9891852
show_tags flag;
src/Pure/attribute.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/attribute.ML	Tue Dec 01 10:39:35 1998 +0100
+++ b/src/Pure/attribute.ML	Tue Dec 01 14:46:35 1998 +0100
@@ -10,6 +10,7 @@
   type tag
   type tthm
   type 'a attribute
+  val show_tags: bool ref
 end;
 
 signature ATTRIBUTE =
@@ -70,12 +71,14 @@
 
 (* display tagged theorems *)
 
+val show_tags = ref false;
+
 fun pretty_tag (name, args) = Pretty.strs (name :: args);
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
-fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
-  | pretty_tthm (thm, tags) = Pretty.block
-      [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
+fun pretty_tthm (thm, tags) =
+  if null tags orelse not (! show_tags) then Pretty.quote (Display.pretty_thm thm)
+  else Pretty.block [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
 
 fun pretty_tthms [th] = pretty_tthm th
   | pretty_tthms ths = Pretty.block (Pretty.fbreaks (map pretty_tthm ths));
isabelle