42 |
43 |
43 (** options for printing **) |
44 (** options for printing **) |
44 |
45 |
45 val show_types = ref false; |
46 val show_types = ref false; |
46 val show_sorts = ref false; |
47 val show_sorts = ref false; |
47 |
48 val show_brackets = ref false; |
48 |
49 |
49 |
50 |
50 (** convert term or typ to ast **) |
51 (** convert term or typ to ast **) |
51 |
52 |
52 fun apply_trans name a f args = |
53 fun apply_trans name a f args = |
225 let val (Ts, args') = synT (symbs, args); |
226 let val (Ts, args') = synT (symbs, args); |
226 in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end |
227 in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end |
227 | synT (_ :: _, []) = sys_error "synT" |
228 | synT (_ :: _, []) = sys_error "synT" |
228 |
229 |
229 and parT (pr, args, p, p': int) = |
230 and parT (pr, args, p, p': int) = |
230 if p > p' then |
231 if p > p' orelse !show_brackets then |
231 #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args)) |
232 #1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args)) |
232 else #1 (synT (pr, args)) |
233 else #1 (synT (pr, args)) |
233 |
234 |
234 and prefixT (_, a, [], _) = [Pretty.str a] |
235 and prefixT (_, a, [], _) = [Pretty.str a] |
235 | prefixT (c, _, args, p) = astT (appT (c, args), p) |
236 | prefixT (c, _, args, p) = astT (appT (c, args), p) |