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