src/Pure/Thy/term_style.ML
changeset 32890 77df12652210
parent 29606 fedb8be05f24
child 32891 d403b99287ff
     1.1 --- a/src/Pure/Thy/term_style.ML	Wed Oct 07 14:01:26 2009 +0200
     1.2 +++ b/src/Pure/Thy/term_style.ML	Wed Oct 07 16:57:56 2009 +0200
     1.3 @@ -1,18 +1,17 @@
     1.4  (*  Title:      Pure/Thy/term_style.ML
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Styles for terms, to use with the "term_style" and "thm_style"
     1.8 -antiquotations.
     1.9 +Styles for term printing.
    1.10  *)
    1.11  
    1.12  signature TERM_STYLE =
    1.13  sig
    1.14 -  val the_style: theory -> string -> (Proof.context -> term -> term)
    1.15 -  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
    1.16 -  val print_styles: theory -> unit
    1.17 +  val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory
    1.18 +  val parse: (term -> term) context_parser
    1.19 +  val parse_bare: (term -> term) context_parser
    1.20  end;
    1.21  
    1.22 -structure TermStyle: TERM_STYLE =
    1.23 +structure Term_Style: TERM_STYLE =
    1.24  struct
    1.25  
    1.26  (* style data *)
    1.27 @@ -22,7 +21,7 @@
    1.28  
    1.29  structure StyleData = TheoryDataFun
    1.30  (
    1.31 -  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
    1.32 +  type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
    1.33    val empty = Symtab.empty;
    1.34    val copy = I;
    1.35    val extend = I;
    1.36 @@ -30,9 +29,6 @@
    1.37      handle Symtab.DUP dup => err_dup_style dup;
    1.38  );
    1.39  
    1.40 -fun print_styles thy =
    1.41 -  Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
    1.42 -
    1.43  
    1.44  (* accessors *)
    1.45  
    1.46 @@ -41,51 +37,69 @@
    1.47      NONE => error ("Unknown antiquote style: " ^ quote name)
    1.48    | SOME (style, _) => style);
    1.49  
    1.50 -fun add_style name style thy =
    1.51 +fun setup name style thy =
    1.52    StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
    1.53      handle Symtab.DUP _ => err_dup_style name;
    1.54  
    1.55  
    1.56 +(* style parsing *)
    1.57 +
    1.58 +fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse)
    1.59 +  >> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
    1.60 +       (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
    1.61 +         (Args.src x) ctxt |>> (fn f => f ctxt)));
    1.62 +
    1.63 +val parse = Args.context :|-- (fn ctxt => Scan.lift 
    1.64 +  (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    1.65 +      >> fold I
    1.66 +  || Scan.succeed I));
    1.67 +
    1.68 +val parse_bare = Args.context :|-- (fn ctxt => Scan.lift Args.liberal_name
    1.69 +  >> (fn name => fst (Args.context_syntax "style"
    1.70 +       (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
    1.71 +          (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt))));
    1.72 +
    1.73 +
    1.74  (* predefined styles *)
    1.75  
    1.76 -fun style_binargs ctxt t =
    1.77 +fun style_binargs proj = Scan.succeed (fn ctxt => fn t =>
    1.78    let
    1.79      val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
    1.80        (Logic.strip_imp_concl t)
    1.81    in
    1.82 -    case concl of (_ $ l $ r) => (l, r)
    1.83 +    case concl of (_ $ l $ r) => proj (l, r)
    1.84      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
    1.85 -  end;
    1.86 +  end);
    1.87  
    1.88 -fun style_parm_premise i ctxt t =
    1.89 +fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
    1.90    let val prems = Logic.strip_imp_prems t in
    1.91      if i <= length prems then nth prems (i - 1)
    1.92      else error ("Not enough premises for prem" ^ string_of_int i ^
    1.93        " in propositon: " ^ Syntax.string_of_term ctxt t)
    1.94 -  end;
    1.95 +  end);
    1.96  
    1.97  val _ = Context.>> (Context.map_theory
    1.98 - (add_style "lhs" (fst oo style_binargs) #>
    1.99 -  add_style "rhs" (snd oo style_binargs) #>
   1.100 -  add_style "prem1" (style_parm_premise 1) #>
   1.101 -  add_style "prem2" (style_parm_premise 2) #>
   1.102 -  add_style "prem3" (style_parm_premise 3) #>
   1.103 -  add_style "prem4" (style_parm_premise 4) #>
   1.104 -  add_style "prem5" (style_parm_premise 5) #>
   1.105 -  add_style "prem6" (style_parm_premise 6) #>
   1.106 -  add_style "prem7" (style_parm_premise 7) #>
   1.107 -  add_style "prem8" (style_parm_premise 8) #>
   1.108 -  add_style "prem9" (style_parm_premise 9) #>
   1.109 -  add_style "prem10" (style_parm_premise 10) #>
   1.110 -  add_style "prem11" (style_parm_premise 11) #>
   1.111 -  add_style "prem12" (style_parm_premise 12) #>
   1.112 -  add_style "prem13" (style_parm_premise 13) #>
   1.113 -  add_style "prem14" (style_parm_premise 14) #>
   1.114 -  add_style "prem15" (style_parm_premise 15) #>
   1.115 -  add_style "prem16" (style_parm_premise 16) #>
   1.116 -  add_style "prem17" (style_parm_premise 17) #>
   1.117 -  add_style "prem18" (style_parm_premise 18) #>
   1.118 -  add_style "prem19" (style_parm_premise 19) #>
   1.119 -  add_style "concl" (K Logic.strip_imp_concl)));
   1.120 + (setup "lhs" (style_binargs fst) #>
   1.121 +  setup "rhs" (style_binargs snd) #>
   1.122 +  setup "prem1" (style_parm_premise 1) #>
   1.123 +  setup "prem2" (style_parm_premise 2) #>
   1.124 +  setup "prem3" (style_parm_premise 3) #>
   1.125 +  setup "prem4" (style_parm_premise 4) #>
   1.126 +  setup "prem5" (style_parm_premise 5) #>
   1.127 +  setup "prem6" (style_parm_premise 6) #>
   1.128 +  setup "prem7" (style_parm_premise 7) #>
   1.129 +  setup "prem8" (style_parm_premise 8) #>
   1.130 +  setup "prem9" (style_parm_premise 9) #>
   1.131 +  setup "prem10" (style_parm_premise 10) #>
   1.132 +  setup "prem11" (style_parm_premise 11) #>
   1.133 +  setup "prem12" (style_parm_premise 12) #>
   1.134 +  setup "prem13" (style_parm_premise 13) #>
   1.135 +  setup "prem14" (style_parm_premise 14) #>
   1.136 +  setup "prem15" (style_parm_premise 15) #>
   1.137 +  setup "prem16" (style_parm_premise 16) #>
   1.138 +  setup "prem17" (style_parm_premise 17) #>
   1.139 +  setup "prem18" (style_parm_premise 18) #>
   1.140 +  setup "prem19" (style_parm_premise 19) #>
   1.141 +  setup "concl" (Scan.succeed (K Logic.strip_imp_concl))));
   1.142  
   1.143  end;