changeset 2360 | 1b6bc618c356 |
parent 2253 | 95b615550b8b |
child 2385 | 73d1435aa729 |
2359:97b88cafe1e8 | 2360:1b6bc618c356 |
---|---|
292 |
292 |
293 val type_decl = type_args -- name -- |
293 val type_decl = type_args -- name -- |
294 optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None |
294 optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None |
295 -- opt_infix >> mk_type_decl; |
295 -- opt_infix >> mk_type_decl; |
296 |
296 |
297 val type_decls = repeat1 (old_type_decl || type_decl) >> |
297 val type_decls = |
298 (mk_type_decls o flat); |
298 repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat); |
299 |
299 |
300 |
300 |
301 (* consts *) |
301 (* consts *) |
302 |
302 |
303 val const_decls = repeat1 (names1 --$$ "::" -- !! |
303 val const_decls = |
304 ((string || const_type false >> quote) -- opt_mixfix)) >> |
304 repeat1 |
305 (mk_big_list o map mk_triple2 o split_decls); |
305 (names1 --$$ "::" -- !! ((string || const_type false >> quote) -- opt_mixfix)) |
306 |
306 >> (mk_big_list o map mk_triple2 o split_decls); |
307 val syntax_decls = |
307 |
308 optional ("(" $$-- !! (name --$$ ")")) "\"\"" -- const_decls |
308 val opt_mode = |
309 >> (fn (mode, txt) => mode ^ "\n" ^ txt); |
309 optional |
310 ("(" $$-- !! (name -- optional ($$ "output" >> K "false") "true" --$$ ")")) |
|
311 ("\"\"", "true") |
|
312 >> mk_pair; |
|
313 |
|
314 val syntax_decls = opt_mode -- const_decls >> (fn (mode, txt) => mode ^ "\n" ^ txt); |
|
310 |
315 |
311 |
316 |
312 (* translations *) |
317 (* translations *) |
313 |
318 |
314 val trans_pat = |
319 val trans_pat = |
528 fun section name pretxt parse = |
533 fun section name pretxt parse = |
529 axm_section name pretxt (parse >> rpair []); |
534 axm_section name pretxt (parse >> rpair []); |
530 |
535 |
531 |
536 |
532 val pure_keywords = |
537 val pure_keywords = |
533 ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<", |
538 ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=", |
534 "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
539 "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="]; |
535 |
540 |
536 val pure_sections = |
541 val pure_sections = |
537 [section "oracle" "|> set_oracle" (name >> strip_quotes), |
542 [section "oracle" "|> set_oracle" (name >> strip_quotes), |
538 section "classes" "|> add_classes" class_decls, |
543 section "classes" "|> add_classes" class_decls, |
539 section "default" "|> add_defsort" sort, |
544 section "default" "|> add_defsort" sort, |