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