1structure term_grammar_dtype = 2struct 3 4open HOLgrammars 5type rule_record = {term_name : string, 6 elements : pp_element list, 7 timestamp : int, 8 block_style : PhraseBlockStyle * block_info, 9 paren_style : ParenStyle} 10 11datatype binder = 12 LAMBDA 13 | BinderString of {tok : string, term_name : string, timestamp : int} 14 15datatype prefix_rule = 16 STD_prefix of rule_record list 17 | BINDER of binder list 18 19datatype suffix_rule = 20 STD_suffix of rule_record list 21 | TYPE_annotation 22 23datatype infix_rule = 24 STD_infix of rule_record list * associativity 25 | RESQUAN_OP 26 | VSCONS 27 | FNAPP of rule_record list 28 29type listspec = 30 {separator : pp_element list, 31 leftdelim : pp_element list, 32 rightdelim : pp_element list, 33 block_info : block_info, 34 cons : string, 35 nilstr : string} 36 37datatype grammar_rule = 38 PREFIX of prefix_rule 39 | SUFFIX of suffix_rule 40 | INFIX of infix_rule 41 | CLOSEFIX of rule_record list 42 43datatype fixity = 44 Infix of associativity * int 45 | Closefix 46 | Suffix of int 47 | Prefix of int 48 | Binder 49 50type grule = {term_name : string, 51 fixity : fixity, 52 pp_elements: pp_element list, 53 paren_style : ParenStyle, 54 block_style : PhraseBlockStyle * block_info} 55 56type skid = string * {Name:string, Thy:string} 57datatype user_delta = 58 GRULE of grule 59 | RMTMTOK of {term_name : string, tok : string} 60 | RMTMNM of string 61 | RMTOK of string 62 | OVERLOAD_ON of string * Term.term 63 | IOVERLOAD_ON of string * Term.term 64 | ASSOC_RESTR of {binder: string option, resbinder : string} 65 | RMOVMAP of skid 66 | CLR_OVL of string 67 | GRMOVMAP of string * Term.term 68 | MOVE_OVLPOSN of {frontp : bool, skid : skid} 69 | ADD_NUMFORM of char * string option 70 | ADD_UPRINTER of {codename: string, pattern : Term.term} 71 | ADD_ABSYN_POSTP of {codename: string} 72 73 74end 75