Merge pull request #31 from Seasawher/Seasawher/issue30

change / add ignore pattern

MkExercise/Extract.lean

@@ -19,8 +19,17 @@ and replace it with `sorry` -/
 def extractExercise (lines : List String) : String := Id.run do
   let mut listen := true
   let mut content := ""
+  let mut «--##--» := false
   for line in lines do
-    if line.endsWith "--#" then
+    -- ignore pattern for a line
+    if line.endsWith "--##" then
+      continue
+
+    -- ignore pattern for a block
+    if line.trim = "--##--" then
+      «--##--» := ! «--##--»
+      continue
+    if «--##--» then
       continue
 
     if let some index := findWhere line "-- sorry" then

README.md

@@ -25,7 +25,8 @@ GitHub Action allows you to run this every time a particular branch is updated,
 
 * Replace the code enclosed by `-- sorry` with `sorry`, preserving indentation.
 * Replace the code after `/- sorry -/` with sorry.
-* Lines ending with `--#` are ignored.
+* Lines ending with `--##` are ignored.
+* Blocks enclosed with `--##--` are ignored.
 
 Check the test code for more information.
 

Test/Exp/Solution.lean

@@ -22,8 +22,14 @@ example : 1 + n = n + 1 := by
     1 + n = n + 1 := by sorry
     _ = n + 1 := by sorry
 
-/-- ignore some sentences -/
+/-- ignore pattern for a line -/
 example : 1 + n = n + 1 := by
   calc
     1 + n = 1 + n := by rfl
     _ = n + 1 := by sorry
+
+/-- ignore pattern for a block -/
+example : 1 + n = n + 1 := by
+  calc
+    1 + n = 1 + n := by rfl
+    _ = n + 1 := by ac_rfl

Test/Src/Solution.lean

@@ -34,12 +34,24 @@ example : 1 + n = n + 1 := by
     1 + n = n + 1 := by /- sorry -/ rw [Nat.add_comm]
     _ = n + 1 := by /- sorry -/ rfl
 
-/-- ignore some sentences -/
+/-- ignore pattern for a line -/
 example : 1 + n = n + 1 := by
   calc
     1 + n = 1 + n := by rfl
-    _ = 1 + n := by rfl --#
-    _ = 1 + n := by rfl --#
-    _ = 1 + n := by rfl --#
-    _ = 1 + n := by rfl --#
+    _ = 1 + n := by rfl --##
+    _ = 1 + n := by rfl --##
+    _ = 1 + n := by rfl --##
+    _ = 1 + n := by rfl --##
     _ = n + 1 := by /- sorry -/ rw [Nat.add_comm]
+
+/-- ignore pattern for a block -/
+example : 1 + n = n + 1 := by
+  calc
+    1 + n = 1 + n := by rfl
+    --##--
+    _ = 1 + n := by rfl
+    _ = 1 + n := by rfl
+    _ = 1 + n := by rfl
+    _ = 1 + n := by rfl
+    --##--
+    _ = n + 1 := by ac_rfl