equal
deleted
inserted
replaced
374 Parsing YXML is pretty straight-forward: split the text into chunks |
374 Parsing YXML is pretty straight-forward: split the text into chunks |
375 separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into |
375 separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into |
376 sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start |
376 sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start |
377 with an empty sub-chunk, and a second empty sub-chunk indicates |
377 with an empty sub-chunk, and a second empty sub-chunk indicates |
378 close of an element. Any other non-empty chunk consists of plain |
378 close of an element. Any other non-empty chunk consists of plain |
379 text. For example, see \verb|~~/src/Pure/General/yxml.ML| or |
379 text. For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or |
380 \verb|~~/src/Pure/General/yxml.scala|. |
380 \verb|~~/src/Pure/PIDE/yxml.scala|. |
381 |
381 |
382 YXML documents may be detected quickly by checking that the first |
382 YXML documents may be detected quickly by checking that the first |
383 two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.% |
383 two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.% |
384 \end{isamarkuptext}% |
384 \end{isamarkuptext}% |
385 \isamarkuptrue% |
385 \isamarkuptrue% |