@@ -131,9 +131,11 @@ def enrich_sentences(fragments):
131131 IOAnnots .DOTTED_RE .pattern , POLARIZED_PATH_SEGMENT )
132132ONE_IO_ANNOT_RE = re .compile (
133133 ISOLATED .format (ONE_IO_ANNOT ), re .VERBOSE )
134- IO_COMMENT_RE = re .compile (
135- r"[ \t]*[(][*]\s+(?:{}\s+)+[*][)]" .format (ONE_IO_ANNOT ),
136- re .VERBOSE )
134+ IO_COMMENT_RE = {
135+ "coq" : re .compile (
136+ r"[ \t]*[(][*]\s+(?:{}\s+)+[*][)]" .format (ONE_IO_ANNOT ),
137+ re .VERBOSE )
138+ }
137139
138140def _parse_path (path ):
139141 path = markers .parse_path (path )
@@ -182,10 +184,10 @@ def inherit_io_annots(fragments, annots):
182184 fr .annots .inherit (annots )
183185 yield fr
184186
185- def _read_io_comments (annots , contents ):
186- for m in IO_COMMENT_RE .finditer (contents ):
187+ def _read_io_comments (annots , contents , lang ):
188+ for m in IO_COMMENT_RE [ lang ] .finditer (contents ):
187189 _update_io_annots (annots , m .group (0 ), ONE_IO_ANNOT_RE , required = True )
188- return IO_COMMENT_RE .sub ("" , contents )
190+ return IO_COMMENT_RE [ lang ] .sub ("" , contents )
189191
190192def _contents (obj ):
191193 if isinstance (obj , RichSentence ):
@@ -197,7 +199,7 @@ def _replace_contents(fr, contents):
197199 return fr ._replace (input = fr .input ._replace (contents = contents ))
198200 return fr ._replace (contents = contents )
199201
200- def read_io_comments (fragments ):
202+ def read_io_comments (fragments , lang ):
201203 """Strip IO comments and update ``.annots`` fields accordingly.
202204
203205 This pass assumes that consecutive ``Text`` fragments have been
@@ -209,13 +211,16 @@ def read_io_comments(fragments):
209211 if sentence :
210212 assert isinstance (sentence , RichSentence )
211213 try :
212- contents = _read_io_comments (sentence .annots , _contents (fr )) # type: ignore
214+ contents = _read_io_comments (sentence .annots , _contents (fr ), lang ) # type: ignore
213215 fr = _replace_contents (fr , contents )
214216 except ValueError as e :
215217 yield e
216218 last_sentence = fr
217219 yield fr
218220
221+ def read_coq_io_comments (fragments ):
222+ return read_io_comments (fragments , lang = "coq" )
223+
219224def _find_marked (sentence , path ):
220225 assert isinstance (sentence , RichSentence )
221226
@@ -424,11 +429,11 @@ def group_whitespace_with_code(fragments):
424429 grouped [idx ] = Text (rest ) if rest else None
425430 return [g for g in grouped if g is not None ]
426431
427- BULLET = re .compile (r"\A\s*[-+*]+\s*\Z" )
428- def is_bullet (fr ):
429- return BULLET .match (fr .input .contents )
432+ COQ_BULLET = re .compile (r"\A\s*[-+*]+\s*\Z" )
433+ def is_coq_bullet (fr ):
434+ return COQ_BULLET .match (fr .input .contents )
430435
431- def attach_comments_to_code (fragments , predicate = lambda _ : True ):
436+ def attach_coq_comments_to_code (fragments , predicate = lambda _ : True ):
432437 """Attach comments immediately following a sentence to the sentence itself.
433438
434439 This is to support this common pattern::
@@ -444,14 +449,14 @@ def attach_comments_to_code(fragments, predicate=lambda _: True):
444449 capture ‘(* n = S _ *) (* the hard case *)’, without the final space).
445450
446451 Only sentences for which `predicate` returns ``True`` are considered (to
447- restrict the behavior to just bullets, pass ``is_bullet ``.
452+ restrict the behavior to just bullets, pass ``is_coq_bullet ``.
448453
449454 >>> from .core import Sentence as S, Text as T
450455 >>> frs = [S("-", [], []), T(" (* … *) "), S("cbn.", [], []), T("(* … *)")]
451- >>> attach_comments_to_code (frs) # doctest: +ELLIPSIS
456+ >>> attach_coq_comments_to_code (frs) # doctest: +ELLIPSIS
452457 [RichSentence(...contents='- (* … *)'...), Text(contents=' '),
453458 RichSentence(...contents='cbn.(* … *)'...)]
454- >>> attach_comments_to_code (frs, predicate=is_bullet ) # doctest: +ELLIPSIS
459+ >>> attach_coq_comments_to_code (frs, predicate=is_coq_bullet ) # doctest: +ELLIPSIS
455460 [RichSentence(...contents='- (* … *)'...), Text(contents=' '),
456461 RichSentence(...contents='cbn.'...), Text(contents='(* … *)')]
457462 """
@@ -517,16 +522,20 @@ def group_hypotheses(fragments):
517522 g .hypotheses [:] = hyps
518523 return fragments
519524
520- FAIL_RE = re .compile (r"^Fail\s+" )
521- FAIL_MSG_RE = re .compile (r"^The command has indeed failed with message:\s+" )
525+ COQ_FAIL_RE = re .compile (r"^Fail\s+" )
526+ COQ_FAIL_MSG_RE = re .compile (r"^The command has indeed failed with message:\s+" )
527+
528+ def is_coq_fail (fr ):
529+ return (isinstance (fr , RichSentence ) and fr .annots .fails
530+ and COQ_FAIL_RE .match (fr .input .contents ))
522531
523- def strip_failures (fragments ):
532+ def strip_coq_failures (fragments ):
524533 for fr in fragments :
525- if isinstance (fr , RichSentence ) and fr . annots . fails and FAIL_RE . match ( fr . input . contents ):
534+ if is_coq_fail (fr ):
526535 for msgs in fragment_message_sets (fr ):
527536 for idx , r in enumerate (msgs ):
528- msgs [idx ] = r ._replace (contents = FAIL_MSG_RE .sub ("" , r .contents ))
529- fr = _replace_contents (fr , FAIL_RE .sub ("" , fr .input .contents ))
537+ msgs [idx ] = r ._replace (contents = COQ_FAIL_MSG_RE .sub ("" , r .contents ))
538+ fr = _replace_contents (fr , COQ_FAIL_RE .sub ("" , fr .input .contents ))
530539 yield fr
531540
532541def dedent (fragments ):
@@ -665,18 +674,24 @@ def isolate_coqdoc(fragments):
665674 strip_text (part .fragments )
666675 return partitioned
667676
668- DEFAULT_TRANSFORMS = [
669- enrich_sentences ,
670- attach_comments_to_code ,
671- group_hypotheses ,
672- read_io_comments ,
673- process_io_annots ,
674- strip_failures ,
675- dedent ,
677+ DEFAULT_TRANSFORMS = {
678+ "coq" : [
679+ enrich_sentences ,
680+ attach_coq_comments_to_code ,
681+ group_hypotheses ,
682+ read_coq_io_comments ,
683+ process_io_annots ,
684+ strip_coq_failures ,
685+ dedent ,
686+ ],
687+ "lean3" : [
688+ enrich_sentences ,
689+ process_io_annots ,
690+ ]
676691 # Not included:
677692 # group_whitespace_with_code (not semantically relevant except)
678693 # commit_io_annotations (breaks mref resolution by removing elements)
679- ]
694+ }
680695
681696def filter_errors (outputs , delay_errors = False ):
682697 transformed , errors = [], []
@@ -700,5 +715,5 @@ def apply_transforms(fragments, transforms, delay_errors):
700715 raise CollectedErrors (* errors )
701716 return fragments
702717
703- def default_transform (fragments , delay_errors = False ):
704- return apply_transforms (fragments , DEFAULT_TRANSFORMS , delay_errors )
718+ def default_transform (fragments , lang , delay_errors = False ):
719+ return apply_transforms (fragments , DEFAULT_TRANSFORMS [ lang ] , delay_errors )
0 commit comments