equal
deleted
inserted
replaced
42 case_fixed: string -> 'a, |
42 case_fixed: string -> 'a, |
43 case_default: string -> 'a} -> string -> 'a |
43 case_default: string -> 'a} -> string -> 'a |
44 val is_marked: string -> bool |
44 val is_marked: string -> bool |
45 val dummy_type: term |
45 val dummy_type: term |
46 val fun_type: term |
46 val fun_type: term |
47 val pretty_position: Position.T -> Pretty.T |
|
48 val encode_position: Position.T -> string |
|
49 val decode_position: string -> Position.T option |
|
50 end; |
47 end; |
51 |
48 |
52 signature LEXICON = |
49 signature LEXICON = |
53 sig |
50 sig |
54 include LEXICON0 |
51 include LEXICON0 |
457 in |
454 in |
458 {mant = sign * #1 (Library.read_int (intpart @ fracpart)), |
455 {mant = sign * #1 (Library.read_int (intpart @ fracpart)), |
459 exp = length fracpart} |
456 exp = length fracpart} |
460 end; |
457 end; |
461 |
458 |
462 |
459 end; |
463 (* positions *) |
|
464 |
|
465 val position_dummy = "<position>"; |
|
466 val position_text = XML.Text position_dummy; |
|
467 |
|
468 fun pretty_position pos = |
|
469 Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy]; |
|
470 |
|
471 fun encode_position pos = |
|
472 YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text])); |
|
473 |
|
474 fun decode_position str = |
|
475 (case YXML.parse_body str handle Fail msg => error msg of |
|
476 [XML.Elem ((name, props), [arg])] => |
|
477 if name = Markup.positionN andalso arg = position_text |
|
478 then SOME (Position.of_properties props) |
|
479 else NONE |
|
480 | _ => NONE); |
|
481 |
|
482 end; |
|