1structure term_pp_types =
2struct
3  type ('a,'b) smppt = ('a,'b) smpp.t
4  datatype grav = Top | RealTop | Prec of (int * string)
5
6  type printing_info =
7       {seen_frees : Term.term HOLset.set,
8        current_bvars : Term.term HOLset.set,
9        last_string : string, in_gspec : bool}
10
11  type 'a printer = (printing_info,'a)smppt
12  type uprinter = unit printer
13  type sysprinter = { gravs : (grav * grav * grav), binderp : bool,
14                      depth : int } -> Term.term -> uprinter
15
16  datatype lit_type = FldName | StringLit | NumLit | CharLit
17
18  datatype annotation =
19    BV of Type.hol_type * (unit -> string)
20  | FV of Type.hol_type * (unit -> string)
21  | TyV
22  | TyOp of (unit -> string)
23  | TySyn of (unit -> string)
24  | Const of {Thy:string,Name:string,Ty:Type.hol_type * (unit -> string)}
25  | SymConst of {Thy:string,Name:string,Ty:Type.hol_type * (unit -> string)}
26  | Note of string
27  | Literal of lit_type
28
29  type xstring = {s:string,sz:int option,ann:annotation option}
30
31  datatype pp_color =
32      Black
33    | RedBrown
34    | Green
35    | BrownGreen
36    | DarkBlue
37    | Purple
38    | BlueGreen
39    | DarkGrey
40    | LightGrey
41    | OrangeRed
42    | VividGreen
43    | Yellow
44    | Blue
45    | PinkPurple
46    | LightBlue
47    | White
48
49  datatype pp_style =
50      FG of pp_color
51    | BG of pp_color
52    | Bold
53    | Underline
54    | UserStyle of string
55
56  type 'a ppstream_funs0 =
57      {add_break      : int * int -> uprinter,
58       add_newline    : uprinter,
59       add_string     : string -> uprinter,
60       add_xstring    : xstring -> uprinter,
61       ustyle         : pp_style list -> uprinter -> uprinter,
62       ublock         : PP.break_style -> int -> uprinter -> uprinter,
63       extras         : 'a}
64
65  type 'tmg upd = {
66    tm_grammar_upd : 'tmg -> 'tmg,
67    ty_grammar_upd : type_grammar.grammar -> type_grammar.grammar,
68    name : string
69  }
70
71  type 'tmg ppbackend = 'tmg upd ppstream_funs0
72  type ppstream_funs = unit ppstream_funs0
73
74  type ('a,'tmg) userprinter =
75    'a -> 'tmg ppbackend -> sysprinter -> ppstream_funs ->
76    (grav * grav * grav) -> int -> Term.term -> uprinter
77  exception UserPP_Failed
78  fun dummyprinter _ _ _ _ _ _ _ = raise Fail "Called dummyprinter"
79end;
80