src/Pure/Thy/term_style.ML
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (20 months ago)
changeset 66987 352b23c97ac8
parent 62969 9f394a16c557
child 67147 dea94b1aabc3
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
     1 (*  Title:      Pure/Thy/term_style.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Styles for term printing.
     5 *)
     6 
     7 signature TERM_STYLE =
     8 sig
     9   val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory
    10   val parse: (term -> term) context_parser
    11 end;
    12 
    13 structure Term_Style: TERM_STYLE =
    14 struct
    15 
    16 (* theory data *)
    17 
    18 structure Data = Theory_Data
    19 (
    20   type T = (Proof.context -> term -> term) parser Name_Space.table;
    21   val empty : T = Name_Space.empty_table "antiquotation_style";
    22   val extend = I;
    23   fun merge data : T = Name_Space.merge_tables data;
    24 );
    25 
    26 val get_data = Data.get o Proof_Context.theory_of;
    27 
    28 fun setup binding style thy =
    29   Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy;
    30 
    31 
    32 (* style parsing *)
    33 
    34 fun parse_single ctxt =
    35   Parse.token Parse.name ::: Parse.args >> (fn src0 =>
    36     let
    37       val (src, parse) = Token.check_src ctxt get_data src0;
    38       val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
    39     in f ctxt end);
    40 
    41 val parse = Args.context :|-- (fn ctxt => Scan.lift
    42   (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    43       >> fold I
    44   || Scan.succeed I));
    45 
    46 
    47 (* predefined styles *)
    48 
    49 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
    50   let
    51     val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t);
    52   in
    53     (case concl of
    54       _ $ l $ r => proj (l, r)
    55     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl))
    56   end);
    57 
    58 val style_prem = Parse.nat >> (fn i => fn ctxt => fn t =>
    59   let
    60     val prems = Logic.strip_imp_prems t;
    61   in
    62     if i <= length prems then nth prems (i - 1)
    63     else
    64       error ("Not enough premises for prem " ^ string_of_int i ^
    65         " in propositon: " ^ Syntax.string_of_term ctxt t)
    66   end);
    67 
    68 fun sub_symbols (d :: s :: ss) =
    69       if Symbol.is_ascii_digit d andalso not (Symbol.is_control s)
    70       then d :: "\<^sub>" :: sub_symbols (s :: ss)
    71       else d :: s :: ss
    72   | sub_symbols cs = cs;
    73 
    74 val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;
    75 
    76 fun sub_term (Free (n, T)) = Free (sub_name n, T)
    77   | sub_term (Var ((n, idx), T)) =
    78       if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
    79       else Var ((sub_name n, 0), T)
    80   | sub_term (t $ u) = sub_term t $ sub_term u
    81   | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
    82   | sub_term t = t;
    83 
    84 val _ = Theory.setup
    85  (setup @{binding lhs} (style_lhs_rhs fst) #>
    86   setup @{binding rhs} (style_lhs_rhs snd) #>
    87   setup @{binding prem} style_prem #>
    88   setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
    89   setup @{binding sub} (Scan.succeed (K sub_term)));
    90 
    91 end;