]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/bin/xhtbl/textParser.mly
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / bin / xhtbl / textParser.mly
1 %{
2
3 module S = Str
4 module L = List
5 module T = Table
6
7 let split s =
8    S.split (S.regexp "[ \r\n\t]+") s
9
10 let mk_css_atom s rs =
11    let cs = split s in
12    let map (b, (x1, x2)) = cs, b, x1, x2 in 
13    L.map map rs
14
15 let mk_string_atom s rs =
16    let map (b, (x1, x2)) = s, b, x1, x2 in 
17    L.map map rs
18
19 %}
20
21 %token <int> NUM
22 %token <string> TEXT 
23 %token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS CF OP CP AT EOF
24
25 %start script
26 %type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script
27
28 %%
29
30 space:
31    | SPACE TEXT TEXT { $2, $3 }
32 ;
33
34 spaces:
35    |              { []       }
36    | space spaces { $1 :: $2 }
37 ;
38
39 text:
40    | TEXT                  { T.Plain $1             }
41    | AT OP TEXT TEXT CP    { T.Link (true, $3, $4)  }
42    | AT AT OP TEXT TEXT CP { T.Link (false, $4, $5) }
43    | AT TEXT               { T.Link (true, $2, $2)  }
44    | AT AT TEXT            { T.Link (false, $3, $3) }   
45 ;
46
47 texts:
48   | text          { [$1]                    }
49   | text PS texts { $1 :: T.Plain " " :: $3 }
50   | text CF texts { $1 :: $3                }
51 ;
52
53 key:
54    | texts { T.Text $1        }
55    | SR    { T.Glue None      }
56    | NUM   { T.Glue (Some $1) }
57 ;
58
59 css:
60    |          { []       }
61    | CSS TEXT { split $2 }
62 ;
63
64 uri:
65    |          { "" }
66    | URI TEXT { $2 }
67 ;
68
69 ext:
70    |          { "" }
71    | EXT TEXT { $2 }
72 ;
73
74 table:
75    | css uri ext name key     { T.mk_key        $5 $1 $2 $3 $4 }
76    | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 "" }
77    | css uri ext OB tables CB { T.mk_line true  $5 $1 $2 $3 "" }
78 ;
79
80 tables:
81    |              { []       }
82    | table tables { $1 :: $2 }
83 ;
84
85 name:
86    |           { "" }
87    | NAME TEXT { $2 }
88 ;
89
90 interval:
91    | NUM     { Some $1, Some $1 }
92    | SR      { None, None       } 
93    | NUM NUM { Some $1, Some $2 }
94    | NUM SR  { Some $1, None    }
95    | SR NUM  { None, Some $2    }
96    | SR SR   { None, None       }
97 ;
98
99 range:
100    | OB interval CB { true, $2  }
101    | OC interval CC { false, $2 }
102 ;
103
104 ranges:
105    |              { []       }
106    | range ranges { $1 :: $2 }
107 ;
108
109 catom:
110    | CSS TEXT ranges { mk_css_atom $2 $3 }
111 ;
112
113 catoms:
114    |              { []      }
115    | catom catoms { $1 @ $2 }
116 ;
117
118 uatom:
119    | URI TEXT ranges { mk_string_atom $2 $3 }
120 ;
121
122 uatoms:
123    |              { []      }
124    | uatom uatoms { $1 @ $2 }
125 ;
126
127 xatom:
128    | EXT TEXT ranges { mk_string_atom $2 $3 }
129 ;
130
131 xatoms:
132    |              { []      }
133    | xatom xatoms { $1 @ $2 }
134 ;
135
136 directive:
137    | name TABLE table catoms uatoms xatoms { $1, $3, $4, $5, $6 }
138 ;
139
140 directives:
141    |                      { []       }
142    | directive directives { $1 :: $2 }
143 ;
144
145 script:
146    | spaces directives EOF { $1, $2 }
147 ;