equal
deleted
inserted
replaced
30 |
30 |
31 |
31 |
32 (** theory data **) |
32 (** theory data **) |
33 |
33 |
34 fun err_unfinished () = error "An unfinished SPARK environment is still open." |
34 fun err_unfinished () = error "An unfinished SPARK environment is still open." |
|
35 (* |
|
36 ERROR: Found the end of the theory, but the last SPARK environment is still open. |
|
37 ..is OK, since "spark_end" does NOT work here for some reason. |
|
38 fun err_unfinished () = () |
|
39 *) |
35 |
40 |
36 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode; |
41 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode; |
37 |
42 |
38 val name_ord = prod_ord string_ord (option_ord int_ord) o |
43 val name_ord = prod_ord string_ord (option_ord int_ord) o |
39 apply2 (strip_number ##> Int.fromString); |
44 apply2 (strip_number ##> Int.fromString); |