From 53414380e6b641a6483e0f7c32251dc77300c978 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 27 Aug 2024 19:21:07 +0200
Subject: [PATCH] comments

---
 app/Commands/Isabelle.hs                              | 5 +++--
 src/Juvix/Compiler/Backend/Isabelle/Pretty.hs         | 8 ++++----
 src/Juvix/Compiler/Backend/Isabelle/Pretty/Options.hs | 8 +++++---
 3 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
index c2731fc2a1..410855d7c9 100644
--- 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
index b9989c1845..324472bf8d 100644
--- 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
index 0d60385755..679abac8c3 100644
--- 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