src/Pure/Isar/antiquote.ML
changeset 12881 eeb36b66480e
parent 9138 6a4fae41a75f
child 14598 7009f59711e3
equal deleted inserted replaced
12880:21485940c8b9 12881:eeb36b66480e
     6 Text with antiquotations of inner items (terms, types etc.).
     6 Text with antiquotations of inner items (terms, types etc.).
     7 *)
     7 *)
     8 
     8 
     9 signature ANTIQUOTE =
     9 signature ANTIQUOTE =
    10 sig
    10 sig
       
    11   exception ANTIQUOTE_FAIL of (string * Position.T) * exn
    11   datatype antiquote = Text of string | Antiq of string * Position.T
    12   datatype antiquote = Text of string | Antiq of string * Position.T
    12   val is_antiq: antiquote -> bool
    13   val is_antiq: antiquote -> bool
    13   val antiquotes_of: string * Position.T -> antiquote list
    14   val antiquotes_of: string * Position.T -> antiquote list
    14 end;
    15 end;
    15 
    16 
    16 structure Antiquote: ANTIQUOTE =
    17 structure Antiquote: ANTIQUOTE =
    17 struct
    18 struct
    18 
    19 
    19 (* datatype antiquote *)
    20 (* datatype antiquote *)
       
    21 
       
    22 exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
    20 
    23 
    21 datatype antiquote =
    24 datatype antiquote =
    22   Text of string |
    25   Text of string |
    23   Antiq of string * Position.T;
    26   Antiq of string * Position.T;
    24 
    27