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