[ cleanup ] remove duplicate copy of header parsing (#3122)

idris-lang · Oct 27, 2023 · 73507a8 · 73507a8
1 parent 58ec72e
commit 73507a8
Showing 1 changed file with 8 additions and 15 deletions.
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
@@ -1929,33 +1929,26 @@ import_ fname indents
          (reexp, ns, nsAs) <- pure b.val
          pure (MkImport (boundToFC fname b) reexp ns nsAs)
 
-export
-prog : OriginDesc -> EmptyRule Module
-prog fname
-    = do b <- bounds (do doc    <- optDocumentation fname
-                         nspace <- option (nsAsModuleIdent mainNS)
-                                     (do decoratedKeyword fname "module"
-                                         decorate fname Module $ mustWork moduleIdent)
-                         imports <- block (import_ fname)
-                         pure (doc, nspace, imports))
-         ds      <- block (topDecl fname)
-         (doc, nspace, imports) <- pure b.val
-         pure (MkModule (boundToFC fname b)
-                        nspace imports doc (collectDefs (concat ds)))
-
 export
 progHdr : OriginDesc -> EmptyRule Module
 progHdr fname
     = do b <- bounds (do doc    <- optDocumentation fname
                          nspace <- option (nsAsModuleIdent mainNS)
                                      (do decoratedKeyword fname "module"
-                                         mustWork moduleIdent)
+                                         decorate fname Module $ mustWork moduleIdent)
                          imports <- block (import_ fname)
                          pure (doc, nspace, imports))
          (doc, nspace, imports) <- pure b.val
          pure (MkModule (boundToFC fname b)
                         nspace imports doc [])
 
+export
+prog : OriginDesc -> EmptyRule Module
+prog fname
+    = do mod <- progHdr fname
+         ds <- block (topDecl fname)
+         pure $ { decls := collectDefs (concat ds)} mod
+
 parseMode : Rule REPLEval
 parseMode
      = do exactIdent "typecheck"