From 6a6afcd7c0fbb318751ad0c643dde3099401db7d Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sun, 1 Aug 2021 16:50:53 -0400
Subject: [PATCH] refactor: spawn `ActiveBuildTarget` from `BuildTarget`

---
 Lake/BuildTarget.lean | 52 +++++++++++++++++++++----------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 2e0913d3df..692ca97646 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -41,32 +41,6 @@ end Target
 -- # Build Targets
 --------------------------------------------------------------------------------
 
--- ## Build Target
-
-abbrev BuildTarget (t : Type) (a : Type) := Target t (IO BuildTask) a
-
-namespace BuildTarget
-
-def mk (artifact : a) (trace : t) (task : IO BuildTask) : BuildTarget t a :=
-  ⟨artifact, trace, task⟩
-
-def opaque (trace : t) (task : IO BuildTask) : BuildTarget t PUnit :=
-  ⟨(), trace, task⟩
-
-def pure (artifact : a) (trace : t) : BuildTarget t a :=
-  ⟨artifact, trace, BuildTask.nop⟩
-
-def nil [Inhabited t] : BuildTarget t PUnit :=
-  pure () Inhabited.default
-
-def spawn (self : BuildTarget t α) : IO BuildTask :=
-  self.task
-
-def materialize (self : BuildTarget t α) : IO PUnit := do
-  (← self.task).await
-
-end BuildTarget
-
 -- ## Active Build Target
 
 abbrev ActiveBuildTarget (t : Type) (a : Type) := Target t BuildTask a
@@ -104,6 +78,32 @@ instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO BuildTask) :=
 
 end ActiveBuildTarget
 
+-- ## Build Target
+
+abbrev BuildTarget (t : Type) (a : Type) := Target t (IO BuildTask) a
+
+namespace BuildTarget
+
+def mk (artifact : a) (trace : t) (task : IO BuildTask) : BuildTarget t a :=
+  ⟨artifact, trace, task⟩
+
+def opaque (trace : t) (task : IO BuildTask) : BuildTarget t PUnit :=
+  ⟨(), trace, task⟩
+
+def pure (artifact : a) (trace : t) : BuildTarget t a :=
+  ⟨artifact, trace, BuildTask.nop⟩
+
+def nil [Inhabited t] : BuildTarget t PUnit :=
+  pure () Inhabited.default
+
+def spawn (self : BuildTarget t a) : IO (ActiveBuildTarget t a) := do
+  return {self with task := (← self.task)}
+
+def materialize (self : BuildTarget t a) : IO PUnit := do
+  (← self.task).await
+
+end BuildTarget
+
 --------------------------------------------------------------------------------
 -- # File Targets
 --------------------------------------------------------------------------------