# HG changeset patch
# User wenzelm
# Date 1083442185 -7200
# Node ID e862cc138e9cc2a1a33ddcb8a6e1b280b2e17730
# Parent  9c78044b99c3481346bfb08dc37133d2dfd9ec15
tuned;

diff -r 9c78044b99c3 -r e862cc138e9c src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sat May 01 22:08:57 2004 +0200
+++ b/src/Pure/Isar/isar_output.ML	Sat May 01 22:09:45 2004 +0200
@@ -262,8 +262,8 @@
 val _ = add_options
  [("show_types", Library.setmp Syntax.show_types o boolean),
   ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
+  ("long_names", Library.setmp NameSpace.long_names o boolean),
   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
-  ("long_names", Library.setmp NameSpace.long_names o boolean),
   ("display", Library.setmp display o boolean),
   ("break", Library.setmp break o boolean),
   ("quotes", Library.setmp quotes o boolean),
@@ -331,14 +331,14 @@
       handle Toplevel.UNDEF => error "No proof state")))) src state;
 
 val _ = add_commands
- [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
-  ("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
-  ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
-  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
+ [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
   ("typ", args Args.local_typ_no_norm (output_with ProofContext.pretty_typ)),
+  ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   ("goals", output_goals true),
-  ("subgoals", output_goals false)];
+  ("subgoals", output_goals false),
+  ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
+  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
 
 end;
diff -r 9c78044b99c3 -r e862cc138e9c src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat May 01 22:08:57 2004 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat May 01 22:09:45 2004 +0200
@@ -111,7 +111,7 @@
       else Lexicon.const "_var" $ t
   | mark_freevars a = a;
 
-fun ast_of_term trf show_const_types no_freeTs show_types show_sorts tm =
+fun ast_of_term trf show_all_types no_freeTs show_types show_sorts tm =
   let
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
@@ -142,9 +142,9 @@
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
       | (c' as Const (c, T), ts) =>
-	if show_const_types
-	then Ast.mk_appl (constrain c' T) (map ast_of ts)
-	else trans c T ts
+          if show_all_types
+          then Ast.mk_appl (constrain c' T) (map ast_of ts)
+          else trans c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
 
     and trans a T args =
@@ -165,8 +165,8 @@
   end;
 
 fun term_to_ast trf tm =
-  ast_of_term trf (! show_all_types) (! show_no_free_types) (! show_types orelse ! show_sorts orelse ! show_all_types)
-    (! show_sorts) tm;
+  ast_of_term trf (! show_all_types) (! show_no_free_types)
+    (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
 
 
 
@@ -331,7 +331,7 @@
       in
         (case token_trans a args of     (*try token translation function*)
           Some s_len => [Pretty.raw_str s_len]
-        | None =>			(*try print translation functions*)
+        | None =>                       (*try print translation functions*)
             astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
       end