equal
deleted
inserted
replaced
94 val numeralN: string val numeral: T |
94 val numeralN: string val numeral: T |
95 val literalN: string val literal: T |
95 val literalN: string val literal: T |
96 val delimiterN: string val delimiter: T |
96 val delimiterN: string val delimiter: T |
97 val inner_stringN: string val inner_string: T |
97 val inner_stringN: string val inner_string: T |
98 val inner_cartoucheN: string val inner_cartouche: T |
98 val inner_cartoucheN: string val inner_cartouche: T |
99 val inner_commentN: string val inner_comment: T |
|
100 val token_rangeN: string val token_range: T |
99 val token_rangeN: string val token_range: T |
101 val sortingN: string val sorting: T |
100 val sortingN: string val sorting: T |
102 val typingN: string val typing: T |
101 val typingN: string val typing: T |
103 val class_parameterN: string val class_parameter: T |
102 val class_parameterN: string val class_parameter: T |
104 val ML_keyword1N: string val ML_keyword1: T |
103 val ML_keyword1N: string val ML_keyword1: T |
143 val keyword2N: string val keyword2: T |
142 val keyword2N: string val keyword2: T |
144 val keyword3N: string val keyword3: T |
143 val keyword3N: string val keyword3: T |
145 val quasi_keywordN: string val quasi_keyword: T |
144 val quasi_keywordN: string val quasi_keyword: T |
146 val improperN: string val improper: T |
145 val improperN: string val improper: T |
147 val operatorN: string val operator: T |
146 val operatorN: string val operator: T |
|
147 val comment1N: string val comment1: T |
|
148 val comment2N: string val comment2: T |
|
149 val comment3N: string val comment3: T |
148 val elapsedN: string |
150 val elapsedN: string |
149 val cpuN: string |
151 val cpuN: string |
150 val gcN: string |
152 val gcN: string |
151 val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T |
153 val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T |
152 val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} |
154 val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} |
438 val (numeralN, numeral) = markup_elem "numeral"; |
440 val (numeralN, numeral) = markup_elem "numeral"; |
439 val (literalN, literal) = markup_elem "literal"; |
441 val (literalN, literal) = markup_elem "literal"; |
440 val (delimiterN, delimiter) = markup_elem "delimiter"; |
442 val (delimiterN, delimiter) = markup_elem "delimiter"; |
441 val (inner_stringN, inner_string) = markup_elem "inner_string"; |
443 val (inner_stringN, inner_string) = markup_elem "inner_string"; |
442 val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; |
444 val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; |
443 val (inner_commentN, inner_comment) = markup_elem "inner_comment"; |
|
444 |
445 |
445 val (token_rangeN, token_range) = markup_elem "token_range"; |
446 val (token_rangeN, token_range) = markup_elem "token_range"; |
446 |
447 |
447 val (sortingN, sorting) = markup_elem "sorting"; |
448 val (sortingN, sorting) = markup_elem "sorting"; |
448 val (typingN, typing) = markup_elem "typing"; |
449 val (typingN, typing) = markup_elem "typing"; |
520 val (stringN, string) = markup_elem "string"; |
521 val (stringN, string) = markup_elem "string"; |
521 val (alt_stringN, alt_string) = markup_elem "alt_string"; |
522 val (alt_stringN, alt_string) = markup_elem "alt_string"; |
522 val (verbatimN, verbatim) = markup_elem "verbatim"; |
523 val (verbatimN, verbatim) = markup_elem "verbatim"; |
523 val (cartoucheN, cartouche) = markup_elem "cartouche"; |
524 val (cartoucheN, cartouche) = markup_elem "cartouche"; |
524 val (commentN, comment) = markup_elem "comment"; |
525 val (commentN, comment) = markup_elem "comment"; |
|
526 |
|
527 |
|
528 (* comments *) |
|
529 |
|
530 val (comment1N, comment1) = markup_elem "comment1"; |
|
531 val (comment2N, comment2) = markup_elem "comment2"; |
|
532 val (comment3N, comment3) = markup_elem "comment3"; |
525 |
533 |
526 |
534 |
527 (* timing *) |
535 (* timing *) |
528 |
536 |
529 val elapsedN = "elapsed"; |
537 val elapsedN = "elapsed"; |