src/Pure/Syntax/printer.ML
author wenzelm
Wed, 15 Mar 2000 18:19:06 +0100
changeset 8457 c5eb14ba754c
parent 6767 99797f2652d1
child 9910 f025cf787554
permissions -rw-r--r--
use Pretty.str / Pretty.raw_str;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/printer.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     4
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
Pretty printing of asts, terms, types and print (ast) translation.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
signature PRINTER0 =
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
     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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val show_types: bool ref
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    13
  val show_no_free_types: bool ref
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
    14
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
signature PRINTER =
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
    17
sig
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  include PRINTER0
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    19
  val term_to_ast: (string -> (bool -> typ -> term list -> term) list) -> term -> Ast.ast
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    20
  val typ_to_ast: (string -> (bool -> typ -> term list -> term) list) -> typ -> Ast.ast
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    21
  val sort_to_ast: (string -> (bool -> typ -> term list -> term) list) -> sort -> Ast.ast
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    22
  type prtabs
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    23
  val empty_prtabs: prtabs
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    24
  val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    25
  val merge_prtabs: prtabs -> prtabs -> prtabs
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    26
  val pretty_term_ast: bool -> prtabs
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    27
    -> (string -> (Ast.ast list -> Ast.ast) list)
6322
7047300264c9 token translation: real;
wenzelm
parents: 6280
diff changeset
    28
    -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    29
  val pretty_typ_ast: bool -> prtabs
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    30
    -> (string -> (Ast.ast list -> Ast.ast) list)
6322
7047300264c9 token translation: real;
wenzelm
parents: 6280
diff changeset
    31
    -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
    32
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
2365
38295260a740 added chartrans_of;
wenzelm
parents: 2229
diff changeset
    34
structure Printer: PRINTER =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
struct
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    36
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
    37
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(** options for printing **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val show_types = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val show_sorts = ref false;
504
a4f09493d929 added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents: 381
diff changeset
    42
val show_brackets = ref false;
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    43
val show_no_free_types = ref false;
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    44
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    47
(** misc utils **)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    48
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    49
(* apply print (ast) translation function *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    51
fun apply_first [] x = raise Match
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    52
  | apply_first (f :: fs) x = f x handle Match => apply_first fs x;
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    53
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    54
fun apply_trans name a fs args =
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    55
  (apply_first fs args handle
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    Match => raise Match
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    57
  | exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    59
fun apply_typed x y fs = map (fn f => f x y) fs;
4147
e57d03a5fc73 print translation: added show_sorts argument;
wenzelm
parents: 3816
diff changeset
    60
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    62
(* simple_ast_of *)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    63
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    64
fun simple_ast_of (Const (c, _)) = Ast.Constant c
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    65
  | simple_ast_of (Free (x, _)) = Ast.Variable x
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    66
  | simple_ast_of (Var (xi, _)) = Ast.Variable (Lexicon.string_of_vname xi)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    67
  | simple_ast_of (t as _ $ _) =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    68
      let val (f, args) = strip_comb t in
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    69
        Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    70
      end
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    71
  | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    72
  | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    73
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    74
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    75
3776
38f8ec304b95 added sort_to_ast;
wenzelm
parents: 2913
diff changeset
    76
(** sort_to_ast, typ_to_ast **)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    77
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    78
fun ast_of_termT trf tm =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  let
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    80
    (* FIXME improve: lookup token classes *)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    81
    fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    82
      | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    83
      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    84
      | ast_of (Const (a, _)) = trans a []
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    85
      | ast_of (t as _ $ _) =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    86
          (case strip_comb t of
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    87
            (Const (a, _), args) => trans a args
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    88
          | (f, args) => Ast.Appl (map ast_of (f :: args)))
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    89
      | ast_of t = simple_ast_of t
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    90
    and trans a args =
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    91
      ast_of (apply_trans "print translation" a (apply_typed false dummyT (trf a)) args)
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    92
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    93
  in ast_of tm end;
617
94436ad4b60d added flag show_no_free_types: bool ref;
wenzelm
parents: 554
diff changeset
    94
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    95
fun sort_to_ast trf S = ast_of_termT trf (TypeExt.term_of_sort S);
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
    96
fun typ_to_ast trf T = ast_of_termT trf (TypeExt.term_of_typ (! show_sorts) T);
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    97
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    98
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
    99
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   100
(** term_to_ast **)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   101
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   102
fun mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   103
  | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   104
  | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
6767
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   105
  | mark_freevars (t as Var (xi, T)) =
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   106
      if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   107
      else Lexicon.const "_var" $ t
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   108
  | mark_freevars a = a;
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   109
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   110
fun ast_of_term trf no_freeTs show_types show_sorts tm =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   111
  let
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
    fun prune_typs (t_seen as (Const _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
      | prune_typs (t as Free (x, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
          if ty = dummyT then (t, seen)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   115
          else if no_freeTs orelse t mem seen then (Lexicon.free x, seen)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
      | prune_typs (t as Var (xi, ty), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
          if ty = dummyT then (t, seen)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   119
          else if no_freeTs orelse t mem seen then (Lexicon.var xi, seen)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
          else (t, t :: seen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
      | prune_typs (t_seen as (Bound _, _)) = t_seen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
      | prune_typs (Abs (x, ty, t), seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
          let val (t', seen') = prune_typs (t, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
          in (Abs (x, ty, t'), seen') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
      | prune_typs (t1 $ t2, seen) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
            val (t1', seen') = prune_typs (t1, seen);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
            val (t2', seen'') = prune_typs (t2, seen');
6767
99797f2652d1 print "..." variable;
wenzelm
parents: 6322
diff changeset
   129
          in (t1' $ t2', seen'') end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   131
    fun ast_of tm =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   132
      (case strip_comb tm of
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   133
        (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   134
      | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   135
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   136
      | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   137
          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   138
      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   139
          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   140
      | (Const (c, T), ts) => trans c T ts
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   141
      | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   143
    and trans a T args =
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   144
      ast_of (apply_trans "print translation" a (apply_typed show_sorts T (trf a)) args)
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   145
        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   147
    and constrain t T =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   148
      if show_types andalso T <> dummyT then
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   149
        Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   150
          ast_of_termT trf (TypeExt.term_of_typ show_sorts T)]
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   151
      else simple_ast_of t
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
  in
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   153
    tm
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   154
    |> SynTrans.prop_tr'
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   155
    |> (if show_types then #1 o prune_typs o rpair [] else I)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   156
    |> mark_freevars
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   157
    |> ast_of
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
fun term_to_ast trf tm =
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   161
  ast_of_term trf (! show_no_free_types) (! show_types orelse ! show_sorts)
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   162
    (! show_sorts) tm;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   166
(** type prtabs **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
datatype symb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
  Arg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
  TypArg of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
  String of string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
  Break of int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
  Block of int * symb list;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   175
type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   176
3816
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   177
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   178
(*find tab for mode*)
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   179
fun get_tab prtabs mode =
4487
9b4c1db5aca1 renamed Symtab.null to Symtab.empty;
wenzelm
parents: 4147
diff changeset
   180
  if_none (assoc (prtabs, mode)) Symtab.empty;
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   181
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   182
(*collect tabs for mode hierarchy (default "")*)
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   183
fun tabs_of prtabs modes =
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   184
  mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]);
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   185
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   186
3816
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   187
(* xprod_to_fmt *)
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   188
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   189
fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = None
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   190
  | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   191
      let
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   192
        fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   193
          | cons_str s syms = String s :: syms;
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   194
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   195
        fun arg (s, p) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   196
          (if s = "type" then TypArg else Arg)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   197
          (if Lexicon.is_terminal s then SynExt.max_pri else p);
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   198
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   199
        fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
6273
94ce639eb7e5 proper handling of print_mode wrt. Pretty.sym;
wenzelm
parents: 6164
diff changeset
   200
              apfst (cons_str s) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   201
          | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   202
              apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   203
          | xsyms_to_syms (SynExt.Space s :: xsyms) =
6273
94ce639eb7e5 proper handling of print_mode wrt. Pretty.sym;
wenzelm
parents: 6164
diff changeset
   204
              apfst (cons_str s) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   205
          | xsyms_to_syms (SynExt.Bg i :: xsyms) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   206
              let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   207
                val (bsyms, xsyms') = xsyms_to_syms xsyms;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   208
                val (syms, xsyms'') = xsyms_to_syms xsyms';
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   209
              in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   210
                (Block (i, bsyms) :: syms, xsyms'')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   211
              end
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   212
          | xsyms_to_syms (SynExt.Brk i :: xsyms) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   213
              apfst (cons (Break i)) (xsyms_to_syms xsyms)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   214
          | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   215
          | xsyms_to_syms [] = ([], []);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   216
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   217
        fun nargs (Arg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   218
          | nargs (TypArg _ :: syms) = nargs syms + 1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   219
          | nargs (String _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   220
          | nargs (Break _ :: syms) = nargs syms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   221
          | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   222
          | nargs [] = 0;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   223
      in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   224
        (case xsyms_to_syms xsymbs of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   225
          (symbs, []) => Some (const, (symbs, nargs symbs, pri))
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   226
        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   227
      end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   228
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   229
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   230
(* empty, extend, merge prtabs *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   231
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   232
val empty_prtabs = [];
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   233
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   234
fun extend_prtabs prtabs mode xprods =
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   235
  let
3816
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   236
    val fmts = rev (mapfilter xprod_to_fmt xprods);
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   237
    val tab = get_tab prtabs mode;
3816
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   238
    val new_tab =
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   239
      if null fmts then tab
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   240
      else Symtab.make_multi (fmts @ Symtab.dest_multi tab)     (*prefer new entries*)
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   241
  in overwrite (prtabs, (mode, new_tab)) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   243
fun merge_prtabs prtabs1 prtabs2 =
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   244
  let
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   245
    val modes = distinct (map fst (prtabs1 @ prtabs2));
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   246
    fun merge mode =
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   247
      (mode,
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   248
        generic_merge (op =) Symtab.dest_multi Symtab.make_multi
3816
7e1b695bcc5e changed preference order of prtab entries;
wenzelm
parents: 3776
diff changeset
   249
          (get_tab prtabs2 mode) (get_tab prtabs1 mode));       (*prefer 2nd over 1st*)
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   250
  in
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   251
    map merge modes
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   252
  end;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   253
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   256
(** pretty term or typ asts **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   258
fun is_chain [Block (_, pr)] = is_chain pr
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   259
  | is_chain [Arg _] = true
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   260
  | is_chain _  = false;
506
e0ca460d6e51 improved show_brackets again - Trueprop does not create () any more.
nipkow
parents: 505
diff changeset
   261
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   262
fun pretty tabs trf tokentrf type_mode curried ast0 p0 =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
  let
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
    val trans = apply_trans "print ast translation";
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   265
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   266
    fun token_trans c [Ast.Variable x] =
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   267
          (case tokentrf c of
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   268
            None => None
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   269
          | Some f => Some (f x))
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   270
      | token_trans _ _ = None;
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   271
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   272
    (*default applications: prefix / postfix*)
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   273
    val appT =
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   274
      if type_mode then TypeExt.tappl_ast_tr'
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   275
      else if curried then SynTrans.applC_ast_tr'
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   276
      else SynTrans.appl_ast_tr';
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   277
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
    fun synT ([], args) = ([], args)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
      | synT (Arg p :: symbs, t :: args) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   280
          let val (Ts, args') = synT (symbs, args);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
          in (astT (t, p) @ Ts, args') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
      | synT (TypArg p :: symbs, t :: args) =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   283
          let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   284
            val (Ts, args') = synT (symbs, args);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   285
          in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   286
            if type_mode then (astT (t, p) @ Ts, args')
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   287
            else (pretty tabs trf tokentrf true curried t p @ Ts, args')
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 62
diff changeset
   288
          end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
      | synT (String s :: symbs, args) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   290
          let val (Ts, args') = synT (symbs, args);
8457
c5eb14ba754c use Pretty.str / Pretty.raw_str;
wenzelm
parents: 6767
diff changeset
   291
          in (Pretty.str s :: Ts, args') end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
      | synT (Block (i, bsymbs) :: symbs, args) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
          let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
            val (bTs, args') = synT (bsymbs, args);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
            val (Ts, args'') = synT (symbs, args');
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
          in (Pretty.blk (i, bTs) :: Ts, args'') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
      | synT (Break i :: symbs, args) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   298
          let val (Ts, args') = synT (symbs, args);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   299
          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
   300
      | synT (_ :: _, []) = sys_error "synT"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   302
    and parT (pr, args, p, p': int) = #1 (synT
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   303
          (if p > p' orelse
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   304
            (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
554
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   305
            then [Block (1, String "(" :: pr @ [String ")"])]
c7d9018cc9e6 various minor internal changes;
wenzelm
parents: 506
diff changeset
   306
            else pr, args))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
8457
c5eb14ba754c use Pretty.str / Pretty.raw_str;
wenzelm
parents: 6767
diff changeset
   308
    and prefixT (_, a, [], _) = [Pretty.str a]
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   309
      | prefixT (c, _, args, p) =
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   310
          if c = Ast.Constant "_appl" orelse c = Ast.Constant "_applC" then
2507
d290b91e76b8 improved error msg;
wenzelm
parents: 2384
diff changeset
   311
            error "Syntax insufficient for printing prefix applications!"
2384
d360b395766e removed chartrans_of;
wenzelm
parents: 2365
diff changeset
   312
          else astT (appT (c, args), p)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   314
    and splitT 0 ([x], ys) = (x, ys)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   315
      | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   316
      | 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
   317
      | splitT _ _ = sys_error "splitT"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   318
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
    and combT (tup as (c, a, args, p)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
        val nargs = length args;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   322
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   323
        (*find matching table entry, or print as prefix / postfix*)
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   324
        fun prnt ([], []) = prefixT tup
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   325
          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi (tb, a), tbs)
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   326
          | prnt ((pr, n, p') :: prnps, tbs) =
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   327
              if nargs = n then parT (pr, args, p, p')
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   328
              else if nargs > n andalso not type_mode then
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   329
                astT (appT (splitT n ([c], args)), p)
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   330
              else prnt (prnps, tbs);
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   331
      in
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   332
        (case token_trans a args of     (*try token translation function*)
8457
c5eb14ba754c use Pretty.str / Pretty.raw_str;
wenzelm
parents: 6767
diff changeset
   333
          Some s_len => [Pretty.raw_str s_len]
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   334
        | None =>			(*try print translation functions*)
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   335
            astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
2200
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   336
      end
2538977e94fa added print_mode: string list ref (order of printer tables);
wenzelm
parents: 1509
diff changeset
   337
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   338
    and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
8457
c5eb14ba754c use Pretty.str / Pretty.raw_str;
wenzelm
parents: 6767
diff changeset
   339
      | astT (Ast.Variable x, _) = [Pretty.str x]
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   340
      | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
5691
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   341
      | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
3a6de95c09d0 no open;
wenzelm
parents: 4699
diff changeset
   342
      | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
6280
218733fb6987 tuned pretty format lookup;
wenzelm
parents: 6273
diff changeset
   343
  in astT (ast0, p0) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
(* pretty_term_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   348
fun pretty_term_ast curried prtabs trf tokentrf ast =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   349
  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   350
    trf tokentrf false curried ast 0);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
(* pretty_typ_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
2701
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   355
fun pretty_typ_ast _ prtabs trf tokentrf ast =
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   356
  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
348ec44248df split ast_of_term(T);
wenzelm
parents: 2507
diff changeset
   357
    trf tokentrf true false ast 0);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
end;