equal
deleted
inserted
replaced
107 val commentN: string val comment: T |
107 val commentN: string val comment: T |
108 val controlN: string val control: T |
108 val controlN: string val control: T |
109 val tokenN: string val token: Properties.T -> T |
109 val tokenN: string val token: Properties.T -> T |
110 val keyword1N: string val keyword1: T |
110 val keyword1N: string val keyword1: T |
111 val keyword2N: string val keyword2: T |
111 val keyword2N: string val keyword2: T |
|
112 val keyword3N: string val keyword3: T |
112 val elapsedN: string |
113 val elapsedN: string |
113 val cpuN: string |
114 val cpuN: string |
114 val gcN: string |
115 val gcN: string |
115 val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T |
116 val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T |
116 val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} |
117 val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} |
398 (* outer syntax *) |
399 (* outer syntax *) |
399 |
400 |
400 val (commandN, command) = markup_elem "command"; |
401 val (commandN, command) = markup_elem "command"; |
401 val (keyword1N, keyword1) = markup_elem "keyword1"; |
402 val (keyword1N, keyword1) = markup_elem "keyword1"; |
402 val (keyword2N, keyword2) = markup_elem "keyword2"; |
403 val (keyword2N, keyword2) = markup_elem "keyword2"; |
|
404 val (keyword3N, keyword3) = markup_elem "keyword3"; |
403 val (operatorN, operator) = markup_elem "operator"; |
405 val (operatorN, operator) = markup_elem "operator"; |
404 val (stringN, string) = markup_elem "string"; |
406 val (stringN, string) = markup_elem "string"; |
405 val (altstringN, altstring) = markup_elem "altstring"; |
407 val (altstringN, altstring) = markup_elem "altstring"; |
406 val (verbatimN, verbatim) = markup_elem "verbatim"; |
408 val (verbatimN, verbatim) = markup_elem "verbatim"; |
407 val (cartoucheN, cartouche) = markup_elem "cartouche"; |
409 val (cartoucheN, cartouche) = markup_elem "cartouche"; |