# HG changeset patch
# User wenzelm
# Date 1160861148 -7200
# Node ID 8b21407de52624df555cb6a408da4aa8555e07e9
# Parent  b98fb9cf903b1087fecb958e28e81a479ee56801
moved pretty_attribs to attrib.ML;

diff -r b98fb9cf903b -r 8b21407de526 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Oct 14 23:25:46 2006 +0200
+++ b/src/Pure/Isar/args.ML	Sat Oct 14 23:25:48 2006 +0200
@@ -26,6 +26,7 @@
   type src
   val src: (string * T list) * Position.T -> src
   val dest_src: src -> (string * T list) * Position.T
+  val pretty_src: Proof.context -> src -> Pretty.T
   val map_name: (string -> string) -> src -> src
   val map_values: (string -> string) -> (typ -> typ) -> (term -> term) -> (thm -> thm)
     -> src -> src
@@ -85,8 +86,6 @@
   val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
   val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
     src -> Proof.context -> Proof.context * 'a
-  val pretty_src: Proof.context -> src -> Pretty.T
-  val pretty_attribs: Proof.context -> src list -> Pretty.T list
 end;
 
 structure Args: ARGS =
@@ -163,6 +162,16 @@
 val src = Src;
 fun dest_src (Src src) = src;
 
+fun pretty_src ctxt src =
+  let
+    fun prt (Arg (_, Value (SOME (Name s)))) = Pretty.str (quote s)
+      | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
+      | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
+      | prt (Arg (_, Value (SOME (Fact ths)))) = ProofContext.pretty_thms ctxt ths
+      | prt arg = Pretty.str (string_of arg);
+    val (s, args) = #1 (dest_src src);
+  in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
+
 fun map_name f (Src ((s, args), pos)) = Src ((f s, args), pos);
 fun map_args f (Src ((s, args), pos)) = Src ((s, map f args), pos);
 
@@ -387,22 +396,4 @@
 
 fun context_syntax kind scan src = apfst Context.the_proof o syntax kind scan src o Context.Proof;
 
-
-
-(** pretty printing **)
-
-fun pretty_src ctxt src =
-  let
-    fun prt (Arg (_, Value (SOME (Name s)))) = Pretty.str (quote s)
-      | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
-      | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
-      | prt (Arg (_, Value (SOME (Fact ths)))) = ProofContext.pretty_thms ctxt ths
-      | prt arg = Pretty.str (string_of arg);
-    val (s, args) = #1 (dest_src src);
-  in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
-
-fun pretty_attribs _ [] = []
-  | pretty_attribs ctxt srcs =
-      [Pretty.enclose "[" "]" (Pretty.commas (map (pretty_src ctxt) srcs))];
-
 end;