1.1 --- a/src/Pure/Syntax/printer.ML Mon May 31 19:36:13 2010 +0200
1.2 +++ b/src/Pure/Syntax/printer.ML Mon May 31 21:06:57 2010 +0200
1.3 @@ -26,8 +26,8 @@
1.4 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
1.5 type prtabs
1.6 val empty_prtabs: prtabs
1.7 - val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
1.8 - val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
1.9 + val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
1.10 + val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
1.11 val merge_prtabs: prtabs -> prtabs -> prtabs
1.12 val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
1.13 extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
1.14 @@ -101,8 +101,8 @@
1.15 handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
1.16 in ast_of tm end;
1.17
1.18 -fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
1.19 -fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
1.20 +fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
1.21 +fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
1.22
1.23
1.24
1.25 @@ -114,7 +114,7 @@
1.26 val {structs, fixes} = idents;
1.27
1.28 fun mark_atoms ((t as Const (c, T)) $ u) =
1.29 - if member (op =) SynExt.standard_token_markers c
1.30 + if member (op =) Syn_Ext.standard_token_markers c
1.31 then t $ u else mark_atoms t $ mark_atoms u
1.32 | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
1.33 | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
1.34 @@ -130,7 +130,7 @@
1.35 else Lexicon.const "_free" $ t
1.36 end
1.37 | mark_atoms (t as Var (xi, T)) =
1.38 - if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
1.39 + if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
1.40 else Lexicon.const "_var" $ t
1.41 | mark_atoms a = a;
1.42
1.43 @@ -155,7 +155,7 @@
1.44
1.45 fun ast_of tm =
1.46 (case strip_comb tm of
1.47 - (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
1.48 + (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts)
1.49 | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
1.50 Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
1.51 | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
1.52 @@ -176,12 +176,12 @@
1.53
1.54 and constrain t T =
1.55 if show_types andalso T <> dummyT then
1.56 - Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
1.57 - ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
1.58 + Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
1.59 + ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
1.60 else simple_ast_of t;
1.61 in
1.62 tm
1.63 - |> SynTrans.prop_tr'
1.64 + |> Syn_Trans.prop_tr'
1.65 |> show_types ? (#1 o prune_typs o rpair [])
1.66 |> mark_atoms
1.67 |> ast_of
1.68 @@ -211,29 +211,29 @@
1.69
1.70 (* xprod_to_fmt *)
1.71
1.72 -fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
1.73 - | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
1.74 +fun xprod_to_fmt (Syn_Ext.XProd (_, _, "", _)) = NONE
1.75 + | xprod_to_fmt (Syn_Ext.XProd (_, xsymbs, const, pri)) =
1.76 let
1.77 fun arg (s, p) =
1.78 (if s = "type" then TypArg else Arg)
1.79 - (if Lexicon.is_terminal s then SynExt.max_pri else p);
1.80 + (if Lexicon.is_terminal s then Syn_Ext.max_pri else p);
1.81
1.82 - fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
1.83 + fun xsyms_to_syms (Syn_Ext.Delim s :: xsyms) =
1.84 apfst (cons (String s)) (xsyms_to_syms xsyms)
1.85 - | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
1.86 + | xsyms_to_syms (Syn_Ext.Argument s_p :: xsyms) =
1.87 apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
1.88 - | xsyms_to_syms (SynExt.Space s :: xsyms) =
1.89 + | xsyms_to_syms (Syn_Ext.Space s :: xsyms) =
1.90 apfst (cons (Space s)) (xsyms_to_syms xsyms)
1.91 - | xsyms_to_syms (SynExt.Bg i :: xsyms) =
1.92 + | xsyms_to_syms (Syn_Ext.Bg i :: xsyms) =
1.93 let
1.94 val (bsyms, xsyms') = xsyms_to_syms xsyms;
1.95 val (syms, xsyms'') = xsyms_to_syms xsyms';
1.96 in
1.97 (Block (i, bsyms) :: syms, xsyms'')
1.98 end
1.99 - | xsyms_to_syms (SynExt.Brk i :: xsyms) =
1.100 + | xsyms_to_syms (Syn_Ext.Brk i :: xsyms) =
1.101 apfst (cons (Break i)) (xsyms_to_syms xsyms)
1.102 - | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
1.103 + | xsyms_to_syms (Syn_Ext.En :: xsyms) = ([], xsyms)
1.104 | xsyms_to_syms [] = ([], []);
1.105
1.106 fun nargs (Arg _ :: syms) = nargs syms + 1
1.107 @@ -263,7 +263,7 @@
1.108 fun remove_prtabs mode xprods prtabs =
1.109 let
1.110 val tab = mode_tab prtabs mode;
1.111 - val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
1.112 + val fmts = map_filter (fn xprod as Syn_Ext.XProd (_, _, c, _) =>
1.113 if null (Symtab.lookup_list tab c) then NONE
1.114 else xprod_to_fmt xprod) xprods;
1.115 val tab' = fold (Symtab.remove_list (op =)) fmts tab;
1.116 @@ -290,15 +290,15 @@
1.117 fun token_trans a x =
1.118 (case tokentrf a of
1.119 NONE =>
1.120 - if member (op =) SynExt.standard_token_classes a
1.121 + if member (op =) Syn_Ext.standard_token_classes a
1.122 then SOME (Pretty.str x) else NONE
1.123 | SOME f => SOME (f ctxt x));
1.124
1.125 (*default applications: prefix / postfix*)
1.126 val appT =
1.127 - if type_mode then TypeExt.tappl_ast_tr'
1.128 - else if curried then SynTrans.applC_ast_tr'
1.129 - else SynTrans.appl_ast_tr';
1.130 + if type_mode then Type_Ext.tappl_ast_tr'
1.131 + else if curried then Syn_Trans.applC_ast_tr'
1.132 + else Syn_Trans.appl_ast_tr';
1.133
1.134 fun synT _ ([], args) = ([], args)
1.135 | synT markup (Arg p :: symbs, t :: args) =
1.136 @@ -333,7 +333,7 @@
1.137
1.138 and parT markup (pr, args, p, p': int) = #1 (synT markup
1.139 (if p > p' orelse
1.140 - (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
1.141 + (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
1.142 then [Block (1, Space "(" :: pr @ [Space ")"])]
1.143 else pr, args))
1.144