130 |
129 |
131 (* outer syntax *) |
130 (* outer syntax *) |
132 |
131 |
133 local |
132 local |
134 |
133 |
135 val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) ""; |
134 val property = |
136 val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) []; |
135 Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) ""; |
|
136 |
|
137 val properties = |
|
138 Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) []; |
137 |
139 |
138 in |
140 in |
139 |
141 |
140 val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof) |
142 val antiq = |
|
143 Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof) |
141 >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); |
144 >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); |
142 |
145 |
143 end; |
146 end; |
144 |
147 |
145 |
148 |
247 | _ => I); |
250 | _ => I); |
248 |
251 |
249 val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; |
252 val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; |
250 |
253 |
251 val (tag, tags) = tag_stack; |
254 val (tag, tags) = tag_stack; |
252 val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag)); |
255 val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag)); |
253 |
256 |
254 val active_tag' = |
257 val active_tag' = |
255 if is_some tag' then tag' |
258 if is_some tag' then tag' |
256 else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE |
259 else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE |
257 else try hd (default_tags cmd_name); |
260 else try hd (default_tags cmd_name); |
314 >> pair (d + 1)) || |
317 >> pair (d + 1)) || |
315 Scan.depend (fn d => Scan.one T.is_end_ignore --| |
318 Scan.depend (fn d => Scan.one T.is_end_ignore --| |
316 (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline) |
319 (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline) |
317 >> pair (d - 1)); |
320 >> pair (d - 1)); |
318 |
321 |
319 val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end); |
322 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end); |
320 |
323 |
321 val locale = |
324 val locale = |
322 Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |-- |
325 Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |-- |
323 P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")"))); |
326 Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")"))); |
324 |
327 |
325 in |
328 in |
326 |
329 |
327 fun present_thy lex default_tags is_markup command_results src = |
330 fun present_thy lex default_tags is_markup command_results src = |
328 let |
331 let |
330 |
333 |
331 val ignored = Scan.state --| ignore |
334 val ignored = Scan.state --| ignore |
332 >> (fn d => (NONE, (NoToken, ("", d)))); |
335 >> (fn d => (NONE, (NoToken, ("", d)))); |
333 |
336 |
334 fun markup mark mk flag = Scan.peek (fn d => |
337 fun markup mark mk flag = Scan.peek (fn d => |
335 improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) -- |
338 improper |-- |
|
339 Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) -- |
336 Scan.repeat tag -- |
340 Scan.repeat tag -- |
337 P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end) |
341 Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end) |
338 >> (fn (((tok, pos), tags), txt) => |
342 >> (fn (((tok, pos), tags), txt) => |
339 let val name = T.content_of tok |
343 let val name = T.content_of tok |
340 in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end)); |
344 in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end)); |
341 |
345 |
342 val command = Scan.peek (fn d => |
346 val command = Scan.peek (fn d => |
343 P.position (Scan.one (T.is_kind T.Command)) -- |
347 Parse.position (Scan.one (T.is_kind T.Command)) -- |
344 Scan.repeat tag |
348 Scan.repeat tag |
345 >> (fn ((tok, pos), tags) => |
349 >> (fn ((tok, pos), tags) => |
346 let val name = T.content_of tok |
350 let val name = T.content_of tok |
347 in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end)); |
351 in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end)); |
348 |
352 |
349 val cmt = Scan.peek (fn d => |
353 val cmt = Scan.peek (fn d => |
350 P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source) |
354 Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source) |
351 >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d))))); |
355 >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d))))); |
352 |
356 |
353 val other = Scan.peek (fn d => |
357 val other = Scan.peek (fn d => |
354 P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d))))); |
358 Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d))))); |
355 |
359 |
356 val token = |
360 val token = |
357 ignored || |
361 ignored || |
358 markup Markup MarkupToken Latex.markup_true || |
362 markup Markup MarkupToken Latex.markup_true || |
359 markup MarkupEnv MarkupEnvToken Latex.markup_true || |
363 markup MarkupEnv MarkupEnvToken Latex.markup_true || |