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