parse \r\n in discouragements

metamath · Jan 3, 2024 · d665bd9 · d665bd9
1 parent ee02227
commit d665bd9
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/metamath-rs/src/comment_parser.rs b/metamath-rs/src/comment_parser.rs
@@ -475,8 +475,8 @@ impl Discouragements {
         static MODIFICATION: OnceLock<RegexSet> = OnceLock::new();
         let modification = MODIFICATION.get_or_init(|| {
             RegexSet::new([
-                r"\(Proof[ \n]+modification[ \n]+is[ \n]+discouraged\.\)",
-                r"\(New[ \n]+usage[ \n]+is[ \n]+discouraged\.\)",
+                r"\(Proof[ \r\n]+modification[ \r\n]+is[ \r\n]+discouraged\.\)",
+                r"\(New[ \r\n]+usage[ \r\n]+is[ \r\n]+discouraged\.\)",
             ])
             .unwrap()
         });

diff --git a/metamath-rs/src/comment_parser_tests.rs b/metamath-rs/src/comment_parser_tests.rs
@@ -326,6 +326,16 @@ fn test_discouragements() {
             usage_discouraged: true,
         }
     );
+    assert_eq!(
+        Discouragements::new(
+            b"A false axiom, experimental.  (Proof modification\r\n\
+            is discouraged.)  (New usage is discouraged.)"
+        ),
+        Discouragements {
+            modification_discouraged: true,
+            usage_discouraged: true,
+        }
+    );
 }
 
 #[track_caller]