show_consts no longer requires show_types;
authorwenzelm
Mon May 22 11:57:27 2000 +0200 (2000-05-22)
changeset 890825f2bdc02123
parent 8907 813fabceec00
child 8909 96503b90307b
show_consts no longer requires show_types;
doc-src/Ref/introduction.tex
src/Pure/display.ML
src/Pure/locale.ML
     1.1 --- a/doc-src/Ref/introduction.tex	Mon May 22 11:56:55 2000 +0200
     1.2 +++ b/doc-src/Ref/introduction.tex	Mon May 22 11:57:27 2000 +0200
     1.3 @@ -287,12 +287,10 @@
     1.4  \item[set \ttindexbold{show_sorts};] makes Isabelle show both types
     1.5    and the sorts of type variables, independently of the value of
     1.6    \texttt{show_types}.
     1.7 -
     1.8 -\item[set \ttindexbold{show_consts};] makes Isabelle show types of
     1.9 -  constants, provided that showing of types is enabled at all.  This
    1.10 -  is supported for printing of proof states only.  Note that the
    1.11 -  output can be enormous as polymorphic constants often occur at
    1.12 -  several different type instances.
    1.13 +  
    1.14 +\item[set \ttindexbold{show_consts};] makes Isabelle show types of constants
    1.15 +  when printing proof states.  Note that the output can be enormous as
    1.16 +  polymorphic constants often occur at several different type instances.
    1.17  
    1.18  \item[set \ttindexbold{long_names};] forces names of all objects
    1.19    (types, constants, theorems, etc.) to be printed in their fully
     2.1 --- a/src/Pure/display.ML	Mon May 22 11:56:55 2000 +0200
     2.2 +++ b/src/Pure/display.ML	Mon May 22 11:57:27 2000 +0200
     2.3 @@ -228,7 +228,7 @@
     2.4    end;
     2.5  
     2.6  
     2.7 -(*also show consts in case of showing types?*)
     2.8 +(*show consts with types in proof state output?*)
     2.9  val show_consts = ref false;
    2.10  
    2.11  
     3.1 --- a/src/Pure/locale.ML	Mon May 22 11:56:55 2000 +0200
     3.2 +++ b/src/Pure/locale.ML	Mon May 22 11:57:27 2000 +0200
     3.3 @@ -639,7 +639,7 @@
     3.4                [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
     3.5            else pretty_subgoals As) @
     3.6          pretty_ffpairs tpairs @
     3.7 -        (if types andalso ! show_consts then pretty_consts prop else []) @
     3.8 +        (if ! show_consts then pretty_consts prop else []) @
     3.9          (if types then pretty_vars prop else []) @
    3.10          (if sorts then pretty_varsT prop else []);
    3.11      in