equal
deleted
inserted
replaced
24 |
24 |
25 val position_dummy = "<position>"; |
25 val position_dummy = "<position>"; |
26 val position_text = XML.Text position_dummy; |
26 val position_text = XML.Text position_dummy; |
27 |
27 |
28 fun pretty pos = |
28 fun pretty pos = |
29 Pretty.markup (Position.markup pos Isabelle_Markup.position) [Pretty.str position_dummy]; |
29 Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy]; |
30 |
30 |
31 fun encode pos = |
31 fun encode pos = |
32 YXML.string_of (XML.Elem (Position.markup pos Isabelle_Markup.position, [position_text])); |
32 YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text])); |
33 |
33 |
34 fun decode str = |
34 fun decode str = |
35 (case YXML.parse_body str handle Fail msg => error msg of |
35 (case YXML.parse_body str handle Fail msg => error msg of |
36 [XML.Elem ((name, props), [arg])] => |
36 [XML.Elem ((name, props), [arg])] => |
37 if name = Isabelle_Markup.positionN andalso arg = position_text |
37 if name = Markup.positionN andalso arg = position_text |
38 then SOME (Position.of_properties props) |
38 then SOME (Position.of_properties props) |
39 else NONE |
39 else NONE |
40 | _ => NONE); |
40 | _ => NONE); |
41 |
41 |
42 |
42 |