src/Pure/General/antiquote.ML
changeset 67426 6311cf9dc943
parent 67193 4ade0d387429
child 67467 482b62d694ca
equal deleted inserted replaced
67425:7d4a088dbc0e 67426:6311cf9dc943
    11   datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
    11   datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
    12   type text_antiquote = Symbol_Pos.T list antiquote
    12   type text_antiquote = Symbol_Pos.T list antiquote
    13   val range: text_antiquote list -> Position.range
    13   val range: text_antiquote list -> Position.range
    14   val split_lines: text_antiquote list -> text_antiquote list list
    14   val split_lines: text_antiquote list -> text_antiquote list list
    15   val antiq_reports: 'a antiquote list -> Position.report list
    15   val antiq_reports: 'a antiquote list -> Position.report list
    16   val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
    16   val scan_control: control scanner
    17   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
    17   val scan_antiq: antiq scanner
    18   val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
    18   val scan_antiquote: text_antiquote scanner
    19   val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
    19   val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
    20   val read: Input.source -> text_antiquote list
    20   val read: Input.source -> text_antiquote list
    21 end;
    21 end;
    22 
    22 
    23 structure Antiquote: ANTIQUOTE =
    23 structure Antiquote: ANTIQUOTE =