src/Pure/General/antiquote.ML
author wenzelm
Fri Apr 01 17:37:46 2016 +0200 (2016-04-01)
changeset 62797 e08c44eed27f
parent 62749 eba34ff9671c
child 67193 4ade0d387429
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/antiquote.ML
     2     Author:     Makarius
     3 
     4 Antiquotations within plain text.
     5 *)
     6 
     7 signature ANTIQUOTE =
     8 sig
     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}
    11   datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
    12   type text_antiquote = Symbol_Pos.T list antiquote
    13   val range: text_antiquote list -> Position.range
    14   val split_lines: text_antiquote list -> text_antiquote list list
    15   val antiq_reports: 'a antiquote list -> Position.report list
    16   val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
    17   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
    18   val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
    19   val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
    20   val read: Input.source -> text_antiquote list
    21 end;
    22 
    23 structure Antiquote: ANTIQUOTE =
    24 struct
    25 
    26 (* datatype antiquote *)
    27 
    28 type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
    29 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 
    32 type text_antiquote = Symbol_Pos.T list antiquote;
    33 
    34 fun antiquote_range (Text ss) = Symbol_Pos.range ss
    35   | antiquote_range (Control {range, ...}) = range
    36   | antiquote_range (Antiq {range, ...}) = range;
    37 
    38 fun range ants =
    39   if null ants then Position.no_range
    40   else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
    41 
    42 
    43 (* split lines *)
    44 
    45 fun split_lines input =
    46   let
    47     fun add a (line, lines) = (a :: line, lines);
    48     fun flush (line, lines) = ([], rev line :: lines);
    49     fun split (a as Text ss) =
    50           (case take_prefix (fn ("\n", _) => false | _ => true) ss of
    51             ([], []) => I
    52           | (_, []) => add a
    53           | ([], _ :: rest) => flush #> split (Text rest)
    54           | (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest))
    55       | split a = add a;
    56   in if null input then [] else rev (#2 (flush (fold split input ([], [])))) end;
    57 
    58 
    59 (* reports *)
    60 
    61 fun antiq_reports ants = ants |> maps
    62   (fn Text _ => []
    63     | Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)]
    64     | Antiq {start, stop, range = (pos, _), ...} =>
    65         [(start, Markup.antiquote),
    66          (stop, Markup.antiquote),
    67          (pos, Markup.antiquoted),
    68          (pos, Markup.language_antiquotation)]);
    69 
    70 
    71 (* scan *)
    72 
    73 open Basic_Symbol_Pos;
    74 
    75 local
    76 
    77 val err_prefix = "Antiquotation lexical error: ";
    78 
    79 val scan_txt =
    80   Scan.repeats1
    81    (Scan.many1 (fn (s, _) =>
    82       not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
    83     $$$ "@" --| Scan.ahead (~$$ "{"));
    84 
    85 val scan_antiq_body =
    86   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    87   Symbol_Pos.scan_cartouche err_prefix ||
    88   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
    89 
    90 fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name);
    91 
    92 in
    93 
    94 val scan_control =
    95   Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) --
    96   Symbol_Pos.scan_cartouche err_prefix >>
    97     (fn (opt_control, body) =>
    98       let
    99         val (name, range) =
   100           (case opt_control of
   101             SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body))
   102           | NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body));
   103       in {name = name, range = range, body = body} end) ||
   104   Scan.one (Symbol.is_control o Symbol_Pos.symbol) >>
   105     (fn (sym, pos) =>
   106       {name = (control_name sym, pos), range = Symbol_Pos.range [(sym, pos)], body = []});
   107 
   108 val scan_antiq =
   109   Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
   110     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
   111       (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
   112     (fn (pos1, (pos2, ((body, pos3), pos4))) =>
   113       {start = Position.range_position (pos1, pos2),
   114        stop = Position.range_position (pos3, pos4),
   115        range = Position.range (pos1, pos4),
   116        body = body});
   117 
   118 val scan_antiquote =
   119   scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq;
   120 
   121 end;
   122 
   123 
   124 (* read *)
   125 
   126 fun parse pos syms =
   127   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
   128     SOME ants => ants
   129   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
   130 
   131 fun read source =
   132   let
   133     val ants = parse (Input.pos_of source) (Input.source_explode source);
   134     val _ = Position.reports (antiq_reports ants);
   135   in ants end;
   136 
   137 end;