author  nipkow 
Tue, 02 Aug 1994 20:08:57 +0200  
changeset 505  97eb677142d9 
parent 504  a4f09493d929 
child 506  e0ca460d6e51 
permissions  rwrr 
18  1 
(* Title: Pure/Syntax/printer.ML 
0  2 
ID: $Id$ 
3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 

18  4 

5 
Pretty printing of asts, terms, types and print (ast) translation. 

0  6 
*) 
7 

8 
signature PRINTER0 = 

9 
sig 

504
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset

10 
val show_brackets: bool ref 
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset

11 
val show_sorts: bool ref 
0  12 
val show_types: bool ref 
13 
end; 

14 

15 
signature PRINTER = 

16 
sig 

17 
include PRINTER0 

18 
structure Symtab: SYMTAB 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

19 
structure SynExt: SYN_EXT 
381  20 
local open SynExt SynExt.Ast in 
0  21 
val term_to_ast: (string > (term list > term) option) > term > ast 
22 
val typ_to_ast: (string > (term list > term) option) > typ > ast 

18  23 
type prtab 
24 
val empty_prtab: prtab 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

25 
val extend_prtab: prtab > xprod list > prtab 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

26 
val merge_prtabs: prtab > prtab > prtab 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

27 
val pretty_term_ast: prtab > (string > (ast list > ast) option) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

28 
> ast > Pretty.T 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

29 
val pretty_typ_ast: prtab > (string > (ast list > ast) option) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

30 
> ast > Pretty.T 
0  31 
end 
32 
end; 

33 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

34 
functor PrinterFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

35 
and SExtension: SEXTENSION sharing TypeExt.SynExt = SExtension.Parser.SynExt) 
258  36 
: PRINTER = 
0  37 
struct 
38 

39 
structure Symtab = Symtab; 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

40 
structure SynExt = TypeExt.SynExt; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

41 
open SExtension.Parser.Lexicon SynExt.Ast SynExt TypeExt SExtension; 
0  42 

43 

44 
(** options for printing **) 

45 

46 
val show_types = ref false; 

47 
val show_sorts = ref false; 

504
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset

48 
val show_brackets = ref false; 
0  49 

50 

18  51 
(** convert term or typ to ast **) 
0  52 

18  53 
fun apply_trans name a f args = 
54 
(f args handle 

0  55 
Match => raise Match 
18  56 
 exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn)); 
0  57 

58 

59 
fun ast_of_term trf show_types show_sorts tm = 

60 
let 

61 
fun prune_typs (t_seen as (Const _, _)) = t_seen 

62 
 prune_typs (t as Free (x, ty), seen) = 

63 
if ty = dummyT then (t, seen) 

64 
else if t mem seen then (Free (x, dummyT), seen) 

65 
else (t, t :: seen) 

66 
 prune_typs (t as Var (xi, ty), seen) = 

67 
if ty = dummyT then (t, seen) 

68 
else if t mem seen then (Var (xi, dummyT), seen) 

69 
else (t, t :: seen) 

70 
 prune_typs (t_seen as (Bound _, _)) = t_seen 

71 
 prune_typs (Abs (x, ty, t), seen) = 

72 
let val (t', seen') = prune_typs (t, seen); 

73 
in (Abs (x, ty, t'), seen') end 

74 
 prune_typs (t1 $ t2, seen) = 

75 
let 

76 
val (t1', seen') = prune_typs (t1, seen); 

77 
val (t2', seen'') = prune_typs (t2, seen'); 

78 
in 

79 
(t1' $ t2', seen'') 

80 
end; 

81 

82 

83 
fun ast_of (Const (a, _)) = trans a [] 

84 
 ast_of (Free (x, ty)) = constrain x (Free (x, dummyT)) ty 

85 
 ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (Var (xi, dummyT)) ty 

86 
 ast_of (Bound i) = Variable ("B." ^ string_of_int i) 

87 
 ast_of (t as Abs _) = ast_of (abs_tr' t) 

88 
 ast_of (t as _ $ _) = 

89 
(case strip_comb t of 

90 
(Const (a, _), args) => trans a args 

91 
 (f, args) => Appl (map ast_of (f :: args))) 

92 

93 
and trans a args = 

94 
(case trf a of 

18  95 
Some f => ast_of (apply_trans "print translation" a f args) 
0  96 
 None => raise Match) 
97 
handle Match => mk_appl (Constant a) (map ast_of args) 

98 

99 
and constrain x t ty = 

100 
if show_types andalso ty <> dummyT then 

101 
ast_of (Const (constrainC, dummyT) $ t $ term_of_typ show_sorts ty) 

102 
else Variable x; 

103 
in 

381  104 
if show_types then 
105 
ast_of (#1 (prune_typs (prop_tr' show_sorts tm, []))) 

106 
else ast_of (prop_tr' show_sorts tm) 

0  107 
end; 
108 

109 

110 
(* term_to_ast *) 

111 

112 
fun term_to_ast trf tm = 

113 
ast_of_term trf (! show_types) (! show_sorts) tm; 

114 

115 

116 
(* typ_to_ast *) 

117 

118 
fun typ_to_ast trf ty = 

119 
ast_of_term trf false false (term_of_typ (! show_sorts) ty); 

120 

121 

122 

18  123 
(** type prtab **) 
0  124 

125 
datatype symb = 

126 
Arg of int  

127 
TypArg of int  

128 
String of string  

129 
Break of int  

130 
Block of int * symb list; 

131 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

132 
type prtab = (symb list * int * int) Symtab.table; 
18  133 

134 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

135 
(* xprods_to_fmts *) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

136 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

137 
fun xprod_to_fmt (XProd (_, _, "", _)) = None 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

138 
 xprod_to_fmt (XProd (_, xsymbs, const, pri)) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

139 
let 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

140 
fun cons_str s (String s' :: syms) = String (s ^ s') :: syms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

141 
 cons_str s syms = String s :: syms; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

142 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

143 
fun arg (s, p) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

144 
(if s = "type" then TypArg else Arg) 
381  145 
(if is_terminal s then 1000 else p); 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

146 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

147 
fun xsyms_to_syms (Delim s :: xsyms) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

148 
apfst (cons_str s) (xsyms_to_syms xsyms) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

149 
 xsyms_to_syms (Argument s_p :: xsyms) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

150 
apfst (cons (arg s_p)) (xsyms_to_syms xsyms) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

151 
 xsyms_to_syms (Space s :: xsyms) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

152 
apfst (cons_str s) (xsyms_to_syms xsyms) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

153 
 xsyms_to_syms (Bg i :: xsyms) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

154 
let 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

155 
val (bsyms, xsyms') = xsyms_to_syms xsyms; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

156 
val (syms, xsyms'') = xsyms_to_syms xsyms'; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

157 
in 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

158 
(Block (i, bsyms) :: syms, xsyms'') 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

159 
end 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

160 
 xsyms_to_syms (Brk i :: xsyms) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

161 
apfst (cons (Break i)) (xsyms_to_syms xsyms) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

162 
 xsyms_to_syms (En :: xsyms) = ([], xsyms) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

163 
 xsyms_to_syms [] = ([], []); 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

164 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

165 
fun nargs (Arg _ :: syms) = nargs syms + 1 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

166 
 nargs (TypArg _ :: syms) = nargs syms + 1 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

167 
 nargs (String _ :: syms) = nargs syms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

168 
 nargs (Break _ :: syms) = nargs syms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

169 
 nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

170 
 nargs [] = 0; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

171 
in 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

172 
(case xsyms_to_syms xsymbs of 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

173 
(symbs, []) => Some (const, (symbs, nargs symbs, pri)) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

174 
 _ => sys_error "xprod_to_fmt: unbalanced blocks") 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

175 
end; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

176 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

177 
fun xprods_to_fmts xprods = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

178 
gen_distinct eq_fst (mapfilter xprod_to_fmt xprods); 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

179 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

180 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

181 
(* empty, extend, merge prtabs *) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

182 

381  183 
fun err_dup_fmts cs = 
184 
error ("Duplicate formats in printer table for " ^ commas_quote cs); 

18  185 

186 
val empty_prtab = Symtab.null; 

0  187 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

188 
fun extend_prtab tab xprods = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

189 
Symtab.extend (op =) (tab, xprods_to_fmts xprods) 
381  190 
handle Symtab.DUPS cs => err_dup_fmts cs; 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

191 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

192 
fun merge_prtabs tab1 tab2 = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

193 
Symtab.merge (op =) (tab1, tab2) 
381  194 
handle Symtab.DUPS cs => err_dup_fmts cs; 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

195 

0  196 

197 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

198 
(** pretty term or typ asts **) 
0  199 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

200 
fun pretty prtab trf type_mode ast0 p0 = 
0  201 
let 
18  202 
val trans = apply_trans "print ast translation"; 
203 

204 
val appT = if type_mode then tappl_ast_tr' else appl_ast_tr'; 

205 

0  206 
fun synT ([], args) = ([], args) 
207 
 synT (Arg p :: symbs, t :: args) = 

18  208 
let val (Ts, args') = synT (symbs, args); 
0  209 
in (astT (t, p) @ Ts, args') end 
210 
 synT (TypArg p :: symbs, t :: args) = 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

211 
let 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

212 
val (Ts, args') = synT (symbs, args); 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

213 
in 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

214 
if type_mode then (astT (t, p) @ Ts, args') 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

215 
else (pretty prtab trf true t p @ Ts, args') 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

216 
end 
0  217 
 synT (String s :: symbs, args) = 
18  218 
let val (Ts, args') = synT (symbs, args); 
0  219 
in (Pretty.str s :: Ts, args') end 
220 
 synT (Block (i, bsymbs) :: symbs, args) = 

221 
let 

222 
val (bTs, args') = synT (bsymbs, args); 

223 
val (Ts, args'') = synT (symbs, args'); 

224 
in (Pretty.blk (i, bTs) :: Ts, args'') end 

225 
 synT (Break i :: symbs, args) = 

18  226 
let val (Ts, args') = synT (symbs, args); 
227 
in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

228 
 synT (_ :: _, []) = sys_error "synT" 
0  229 

230 
and parT (pr, args, p, p': int) = 

505
97eb677142d9
minimized () in forced printing of barckets (show_brackets)
nipkow
parents:
504
diff
changeset

231 
if p > p' orelse (!show_brackets andalso p' <> max_pri) then 
18  232 
#1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args)) 
233 
else #1 (synT (pr, args)) 

0  234 

235 
and prefixT (_, a, [], _) = [Pretty.str a] 

236 
 prefixT (c, _, args, p) = astT (appT (c, args), p) 

237 

18  238 
and splitT 0 ([x], ys) = (x, ys) 
239 
 splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys) 

240 
 splitT n (rev_xs, y :: ys) = splitT (n  1) (y :: rev_xs, ys) 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

241 
 splitT _ _ = sys_error "splitT" 
18  242 

0  243 
and combT (tup as (c, a, args, p)) = 
244 
let 

245 
val nargs = length args; 

18  246 

0  247 
fun prnt (pr, n, p') = 
18  248 
if nargs = n then parT (pr, args, p, p') 
249 
else if nargs < n orelse type_mode then prefixT tup 

250 
else astT (appT (splitT n ([c], args)), p); 

0  251 
in 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

252 
(case (trf a, Symtab.lookup (prtab, a)) of 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

253 
(None, None) => prefixT tup 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

254 
 (None, Some prnp) => prnt prnp 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

255 
 (Some f, None) => 
18  256 
(astT (trans a f args, p) handle Match => prefixT tup) 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

257 
 (Some f, Some prnp) => 
18  258 
(astT (trans a f args, p) handle Match => prnt prnp)) 
0  259 
end 
260 

261 
and astT (c as Constant a, p) = combT (c, a, [], p) 

262 
 astT (Variable x, _) = [Pretty.str x] 

18  263 
 astT (Appl ((c as Constant a) :: (args as _ :: _)), p) = 
264 
combT (c, a, args, p) 

0  265 
 astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) 
18  266 
 astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast]; 
0  267 
in 
268 
astT (ast0, p0) 

269 
end; 

270 

271 

272 
(* pretty_term_ast *) 

273 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

274 
fun pretty_term_ast prtab trf ast = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

275 
Pretty.blk (0, pretty prtab trf false ast 0); 
0  276 

277 

278 
(* pretty_typ_ast *) 

279 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

280 
fun pretty_typ_ast prtab trf ast = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

281 
Pretty.blk (0, pretty prtab trf true ast 0); 
0  282 

283 

284 
end; 

285 