1(*  Title:      Pure/General/antiquote.ML
2    Author:     Makarius
3
4Antiquotations within plain text.
5*)
6
7signature ANTIQUOTE =
8sig
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 text_antiquote_range: text_antiquote -> Position.range
14  val text_range: text_antiquote list -> Position.range
15  val split_lines: text_antiquote list -> text_antiquote list list
16  val antiq_reports: 'a antiquote list -> Position.report list
17  val scan_control: control scanner
18  val scan_antiq: antiq scanner
19  val scan_antiquote: text_antiquote scanner
20  val scan_antiquote_comments: text_antiquote scanner
21  val parse_comments: Position.T -> Symbol_Pos.T list -> text_antiquote list
22  val read_comments: Input.source -> text_antiquote list
23end;
24
25structure Antiquote: ANTIQUOTE =
26struct
27
28(* datatype antiquote *)
29
30type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
31type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
32datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
33
34type text_antiquote = Symbol_Pos.T list antiquote;
35
36fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
37  | text_antiquote_range (Control {range, ...}) = range
38  | text_antiquote_range (Antiq {range, ...}) = range;
39
40fun text_range ants =
41  if null ants then Position.no_range
42  else
43    Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants)));
44
45
46(* split lines *)
47
48fun split_lines input =
49  let
50    fun add a (line, lines) = (a :: line, lines);
51    fun flush (line, lines) = ([], rev line :: lines);
52    fun split (a as Text ss) =
53          (case chop_prefix (fn ("\n", _) => false | _ => true) ss of
54            ([], []) => I
55          | (_, []) => add a
56          | ([], _ :: rest) => flush #> split (Text rest)
57          | (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest))
58      | split a = add a;
59  in if null input then [] else rev (#2 (flush (fold split input ([], [])))) end;
60
61
62(* reports *)
63
64fun antiq_reports ants = ants |> maps
65  (fn Text _ => []
66    | Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)]
67    | Antiq {start, stop, range = (pos, _), ...} =>
68        [(start, Markup.antiquote),
69         (stop, Markup.antiquote),
70         (pos, Markup.antiquoted),
71         (pos, Markup.language_antiquotation)]);
72
73
74(* scan *)
75
76open Basic_Symbol_Pos;
77
78local
79
80val err_prefix = "Antiquotation lexical error: ";
81
82val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
83val scan_nl_opt = Scan.optional scan_nl [];
84
85val scan_plain_txt =
86  Scan.many1 (fn (s, _) =>
87    not (Comment.is_symbol s) andalso
88    not (Symbol.is_control s) andalso
89    s <> Symbol.open_ andalso
90    s <> "@" andalso
91    s <> "\n" andalso
92    Symbol.not_eof s) ||
93  Scan.one (Comment.is_symbol o Symbol_Pos.symbol) >> single ||
94  $$$ "@" --| Scan.ahead (~$$ "{");
95
96val scan_text =
97  scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
98
99val scan_text_comments =
100  scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
101
102val scan_antiq_body =
103  Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
104  Symbol_Pos.scan_cartouche err_prefix ||
105  Comment.scan --
106    Symbol_Pos.!!! (fn () => err_prefix ^ "bad formal comment in antiquote body") Scan.fail
107    >> K [] ||
108  Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
109
110fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name);
111
112in
113
114val scan_control =
115  Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) --
116  Symbol_Pos.scan_cartouche err_prefix >>
117    (fn (opt_control, body) =>
118      let
119        val (name, range) =
120          (case opt_control of
121            SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body))
122          | NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body));
123      in {name = name, range = range, body = body} end) ||
124  Scan.one (Symbol.is_control o Symbol_Pos.symbol) >>
125    (fn (sym, pos) =>
126      {name = (control_name sym, pos), range = Symbol_Pos.range [(sym, pos)], body = []});
127
128val scan_antiq =
129  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
130    Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
131      (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
132    (fn (pos1, (pos2, ((body, pos3), pos4))) =>
133      {start = Position.range_position (pos1, pos2),
134       stop = Position.range_position (pos3, pos4),
135       range = Position.range (pos1, pos4),
136       body = body});
137
138val scan_antiquote =
139  scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq;
140
141val scan_antiquote_comments =
142  scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq;
143
144end;
145
146
147(* parse and read (with formal comments) *)
148
149fun parse_comments pos syms =
150  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote_comments) syms of
151    SOME ants => ants
152  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
153
154fun read_comments source =
155  let
156    val ants = parse_comments (Input.pos_of source) (Input.source_explode source);
157    val _ = Position.reports (antiq_reports ants);
158  in ants end;
159
160end;
161