comments

anoma · Aug 27, 2024 · 5341438 · 5341438
1 parent 2b76f5d
commit 5341438
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 9 deletions.
diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
@@ -14,10 +14,11 @@ runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
   res <- runPipeline opts inputFile upToIsabelle
   let thy = res ^. resultTheory
+      comments = res ^. resultComments
   outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
   if
       | opts ^. isabelleStdout -> do
-          renderStdOut (ppOutDefault thy)
+          renderStdOut (ppOutDefault comments thy)
           putStrLn ""
       | otherwise -> do
           ensureDir outputDir
@@ -29,4 +30,4 @@ runCommand opts = do
                   )
               absPath :: Path Abs File
               absPath = outputDir <//> file
-          writeFileEnsureLn absPath (ppPrint thy <> "\n")
+          writeFileEnsureLn absPath (ppPrint comments thy <> "\n")
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs
@@ -6,8 +6,8 @@ import Juvix.Data.PPOutput
 import Juvix.Prelude
 import Prettyprinter.Render.Terminal qualified as Ansi
 
-ppOutDefault :: (PrettyCode c) => c -> AnsiText
-ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions
+ppOutDefault :: (PrettyCode c) => [Comment] -> c -> AnsiText
+ppOutDefault comments = mkAnsiText . PPOutput . doc (defaultOptions comments)
 
 ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText
 ppOut o = mkAnsiText . PPOutput . doc (project o)
@@ -18,5 +18,5 @@ ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLa
 ppTrace :: (PrettyCode c) => c -> Text
 ppTrace = ppTrace' traceOptions
 
-ppPrint :: (PrettyCode c) => c -> Text
-ppPrint = show . ppOutDefault
+ppPrint :: (PrettyCode c) => [Comment] -> c -> Text
+ppPrint comments = show . ppOutDefault comments
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Options.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Options.hs
@@ -3,17 +3,19 @@ module Juvix.Compiler.Backend.Isabelle.Pretty.Options where
 import Juvix.Prelude
 
 data Options = Options
+  { _optComments :: [Comment]
+  }
 
 makeLenses ''Options
 
-defaultOptions :: Options
+defaultOptions :: [Comment] -> Options
 defaultOptions = Options
 
 traceOptions :: Options
-traceOptions = defaultOptions
+traceOptions = defaultOptions []
 
 fromGenericOptions :: GenericOptions -> Options
-fromGenericOptions _ = defaultOptions
+fromGenericOptions _ = defaultOptions []
 
 instance CanonicalProjection GenericOptions Options where
   project = fromGenericOptions