353 map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ |
353 map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ |
354 [(SOME (Token.content_of cmd, Token.pos_of cmd, tags), |
354 [(SOME (Token.content_of cmd, Token.pos_of cmd, tags), |
355 (Basic_Token cmd, (markup_false, d)))])); |
355 (Basic_Token cmd, (markup_false, d)))])); |
356 |
356 |
357 val cmt = Scan.peek (fn d => |
357 val cmt = Scan.peek (fn d => |
358 Scan.one is_black_comment >> |
358 Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); |
359 (fn tok => (NONE, (Basic_Token tok, ("", d)))) || |
|
360 (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |-- |
|
361 Parse.!!!! (improper |-- Parse.document_source) >> |
|
362 (fn source => (NONE, (Markup_Token ("cmt", source), ("", d))))); |
|
363 |
359 |
364 val other = Scan.peek (fn d => |
360 val other = Scan.peek (fn d => |
365 Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); |
361 Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); |
366 |
362 |
367 val tokens = |
363 val tokens = |