src/Pure/Syntax/term_position.ML
changeset 50201 c26369c9eda6
parent 49685 4341e4d86872
child 52175 626a757d3c2d
equal deleted inserted replaced
50200:2c94c065564e 50201:c26369c9eda6
    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