src/Pure/General/markup.ML
changeset 23642 10672e025b83
parent 23637 f3e16ee56f32
child 23644 e28b8e8a85b6
equal deleted inserted replaced
23641:d6f9d3acffaa 23642:10672e025b83
    44 
    44 
    45 type T = string * property list;
    45 type T = string * property list;
    46 
    46 
    47 val none = ("", []);
    47 val none = ("", []);
    48 
    48 
    49 fun markup kind = (kind, (kind, []));
    49 fun markup kind = (kind, (kind, []): T);
    50 fun markup_name kind = (kind, fn name => (kind, [(nameN, name)]): T);
    50 fun markup_name kind = (kind, fn name => (kind, [(nameN, name)]): T);
    51 
    51 
    52 
    52 
    53 (* logical entities *)
    53 (* logical entities *)
    54 
    54