src/Pure/General/antiquote.ML
changeset 67467 482b62d694ca
parent 67426 6311cf9dc943
child 67522 9e712280cc37
equal deleted inserted replaced
67466:82bc0d5d1ef3 67467:482b62d694ca
     8 sig
     8 sig
     9   type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
     9   type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
    10   type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
    10   type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
    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 text_antiquote_range: text_antiquote -> Position.range
       
    14   val text_range: text_antiquote list -> Position.range
    14   val split_lines: text_antiquote list -> text_antiquote list list
    15   val split_lines: text_antiquote list -> text_antiquote list list
    15   val antiq_reports: 'a antiquote list -> Position.report list
    16   val antiq_reports: 'a antiquote list -> Position.report list
    16   val scan_control: control scanner
    17   val scan_control: control scanner
    17   val scan_antiq: antiq scanner
    18   val scan_antiq: antiq scanner
    18   val scan_antiquote: text_antiquote scanner
    19   val scan_antiquote: text_antiquote scanner
    29 type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
    30 type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
    30 datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
    31 datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
    31 
    32 
    32 type text_antiquote = Symbol_Pos.T list antiquote;
    33 type text_antiquote = Symbol_Pos.T list antiquote;
    33 
    34 
    34 fun antiquote_range (Text ss) = Symbol_Pos.range ss
    35 fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
    35   | antiquote_range (Control {range, ...}) = range
    36   | text_antiquote_range (Control {range, ...}) = range
    36   | antiquote_range (Antiq {range, ...}) = range;
    37   | text_antiquote_range (Antiq {range, ...}) = range;
    37 
    38 
    38 fun range ants =
    39 fun text_range ants =
    39   if null ants then Position.no_range
    40   if null ants then Position.no_range
    40   else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
    41   else
       
    42     Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants)));
    41 
    43 
    42 
    44 
    43 (* split lines *)
    45 (* split lines *)
    44 
    46 
    45 fun split_lines input =
    47 fun split_lines input =