generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles

--- a/src/Pure/Thy/term_style.ML	Wed Oct 07 14:01:26 2009 +0200
+++ b/src/Pure/Thy/term_style.ML	Wed Oct 07 16:57:56 2009 +0200
@@ -1,18 +1,17 @@
 (*  Title:      Pure/Thy/term_style.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Styles for terms, to use with the "term_style" and "thm_style"
-antiquotations.
+Styles for term printing.
 *)
 
 signature TERM_STYLE =
 sig
-  val the_style: theory -> string -> (Proof.context -> term -> term)
-  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
-  val print_styles: theory -> unit
+  val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory
+  val parse: (term -> term) context_parser
+  val parse_bare: (term -> term) context_parser
 end;
 
-structure TermStyle: TERM_STYLE =
+structure Term_Style: TERM_STYLE =
 struct
 
 (* style data *)
@@ -22,7 +21,7 @@
 
 structure StyleData = TheoryDataFun
 (
-  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
+  type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
@@ -30,9 +29,6 @@
     handle Symtab.DUP dup => err_dup_style dup;
 );
 
-fun print_styles thy =
-  Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
-
 
 (* accessors *)
 
@@ -41,51 +37,69 @@
     NONE => error ("Unknown antiquote style: " ^ quote name)
   | SOME (style, _) => style);
 
-fun add_style name style thy =
+fun setup name style thy =
   StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
     handle Symtab.DUP _ => err_dup_style name;
 
 
+(* style parsing *)
+
+fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse)
+  >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
+       (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
+         (Args.src x) ctxt |>> (fn f => f ctxt)));
+
+val parse = Args.context :|-- (fn ctxt => Scan.lift 
+  (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
+      >> fold I
+  || Scan.succeed I));
+
+val parse_bare = Args.context :|-- (fn ctxt => Scan.lift Args.liberal_name
+  >> (fn name => fst (Args.context_syntax "style"
+       (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
+          (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt))));
+
+
 (* predefined styles *)
 
-fun style_binargs ctxt t =
+fun style_binargs proj = Scan.succeed (fn ctxt => fn t =>
   let
     val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
       (Logic.strip_imp_concl t)
   in
-    case concl of (_ $ l $ r) => (l, r)
+    case concl of (_ $ l $ r) => proj (l, r)
     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
-  end;
+  end);
 
-fun style_parm_premise i ctxt t =
+fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
   let val prems = Logic.strip_imp_prems t in
     if i <= length prems then nth prems (i - 1)
     else error ("Not enough premises for prem" ^ string_of_int i ^
       " in propositon: " ^ Syntax.string_of_term ctxt t)
-  end;
+  end);
 
 val _ = Context.>> (Context.map_theory
- (add_style "lhs" (fst oo style_binargs) #>
-  add_style "rhs" (snd oo style_binargs) #>
-  add_style "prem1" (style_parm_premise 1) #>
-  add_style "prem2" (style_parm_premise 2) #>
-  add_style "prem3" (style_parm_premise 3) #>
-  add_style "prem4" (style_parm_premise 4) #>
-  add_style "prem5" (style_parm_premise 5) #>
-  add_style "prem6" (style_parm_premise 6) #>
-  add_style "prem7" (style_parm_premise 7) #>
-  add_style "prem8" (style_parm_premise 8) #>
-  add_style "prem9" (style_parm_premise 9) #>
-  add_style "prem10" (style_parm_premise 10) #>
-  add_style "prem11" (style_parm_premise 11) #>
-  add_style "prem12" (style_parm_premise 12) #>
-  add_style "prem13" (style_parm_premise 13) #>
-  add_style "prem14" (style_parm_premise 14) #>
-  add_style "prem15" (style_parm_premise 15) #>
-  add_style "prem16" (style_parm_premise 16) #>
-  add_style "prem17" (style_parm_premise 17) #>
-  add_style "prem18" (style_parm_premise 18) #>
-  add_style "prem19" (style_parm_premise 19) #>
-  add_style "concl" (K Logic.strip_imp_concl)));
+ (setup "lhs" (style_binargs fst) #>
+  setup "rhs" (style_binargs snd) #>
+  setup "prem1" (style_parm_premise 1) #>
+  setup "prem2" (style_parm_premise 2) #>
+  setup "prem3" (style_parm_premise 3) #>
+  setup "prem4" (style_parm_premise 4) #>
+  setup "prem5" (style_parm_premise 5) #>
+  setup "prem6" (style_parm_premise 6) #>
+  setup "prem7" (style_parm_premise 7) #>
+  setup "prem8" (style_parm_premise 8) #>
+  setup "prem9" (style_parm_premise 9) #>
+  setup "prem10" (style_parm_premise 10) #>
+  setup "prem11" (style_parm_premise 11) #>
+  setup "prem12" (style_parm_premise 12) #>
+  setup "prem13" (style_parm_premise 13) #>
+  setup "prem14" (style_parm_premise 14) #>
+  setup "prem15" (style_parm_premise 15) #>
+  setup "prem16" (style_parm_premise 16) #>
+  setup "prem17" (style_parm_premise 17) #>
+  setup "prem18" (style_parm_premise 18) #>
+  setup "prem19" (style_parm_premise 19) #>
+  setup "concl" (Scan.succeed (K Logic.strip_imp_concl))));
 
 end;

--- a/src/Pure/Thy/thy_output.ML	Wed Oct 07 14:01:26 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed Oct 07 16:57:56 2009 +0200
@@ -470,11 +470,11 @@
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
-fun pretty_term_style ctxt (name, t) =
-  pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t);
+fun pretty_term_style ctxt (style, t) =
+  pretty_term ctxt (style t);
 
-fun pretty_thm_style ctxt (name, th) =
-  pretty_term_style ctxt (name, Thm.full_prop_of th);
+fun pretty_thm_style ctxt (style, th) =
+  pretty_term_style ctxt (style, Thm.full_prop_of th);
 
 fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
 
@@ -513,15 +513,19 @@
 fun basic_entities name scan pretty = antiquotation name scan
   (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
 
+fun basic_entities_style name scan pretty = antiquotation name scan
+  (fn {source, context, ...} => fn (style, xs) =>
+    output (maybe_pretty_source (fn x => pretty context (style, x)) source xs));
+
 fun basic_entity name scan = basic_entities name (scan >> single);
 
 in
 
-val _ = basic_entities "thm" Attrib.thms pretty_thm;
-val _ = basic_entity "thm_style" (Scan.lift Args.liberal_name -- Attrib.thm) pretty_thm_style;
-val _ = basic_entity "prop" Args.prop pretty_term;
-val _ = basic_entity "term" Args.term pretty_term;
-val _ = basic_entity "term_style" (Scan.lift Args.liberal_name -- Args.term) pretty_term_style;
+val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
+val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
+val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
+val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
+val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
 val _ = basic_entity "term_type" Args.term pretty_term_typ;
 val _ = basic_entity "typeof" Args.term pretty_term_typeof;
 val _ = basic_entity "const" Args.const_proper pretty_const;