src/Pure/PIDE/sendback.ML
changeset 50172 1a28109edc6d
parent 50164 77668b522ffe
child 50201 c26369c9eda6
equal deleted inserted replaced
50171:d655dda100c5 50172:1a28109edc6d
    23       | NONE => []);
    23       | NONE => []);
    24   in Markup.properties props Isabelle_Markup.sendback end;
    24   in Markup.properties props Isabelle_Markup.sendback end;
    25 
    25 
    26 fun markup s = Markup.markup (make_markup ()) s;
    26 fun markup s = Markup.markup (make_markup ()) s;
    27 
    27 
    28 val markup_implicit = Markup.markup Isabelle_Markup.sendback;
    28 fun markup_implicit s = Markup.markup Isabelle_Markup.sendback s;
    29 
    29 
    30 end;
    30 end;
    31 
    31