fix text comments

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -31,10 +31,10 @@ ppParams = \case
     ps <- mapM ppCode params
     return $ Just $ parens (hsep (punctuate comma ps))
 
-ppComment :: Maybe Text -> Sem r (Doc Ann)
-ppComment = \case
+ppJudocComment :: Maybe Text -> Sem r (Doc Ann)
+ppJudocComment = \case
   Nothing -> return ""
-  Just c -> return $ annotate AnnComment "text {*" <> line <> pretty c <> line <> annotate AnnComment "*}" <> line
+  Just c -> return $ annotate AnnComment "text \\<open>" <> line <> annotate AnnComment (pretty c) <> line <> annotate AnnComment "\\<close>" <> line
 
 instance PrettyCode Name where
   ppCode = return . prettyName False
@@ -195,15 +195,15 @@ instance PrettyCode Statement where
 
 instance PrettyCode Definition where
   ppCode Definition {..} = do
-    comment <- ppComment _definitionComment
+    comment <- ppJudocComment _definitionComment
     n <- ppCode _definitionName
     ty <- ppCodeQuoted _definitionType
     body <- ppCode _definitionBody
     return $ comment <> kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (dquotes (n <+> "=" <> oneLineOrNext body))
 
 instance PrettyCode Function where
   ppCode Function {..} = do
-    comment <- ppComment _functionComment
+    comment <- ppJudocComment _functionComment
     n <- ppCode _functionName
     ty <- ppCodeQuoted _functionType
     cls <- mapM ppCode _functionClauses
@@ -218,37 +218,37 @@ instance PrettyCode Clause where
 
 instance PrettyCode Synonym where
   ppCode Synonym {..} = do
-    comment <- ppComment _synonymComment
+    comment <- ppJudocComment _synonymComment
     n <- ppCode _synonymName
     ty <- ppCodeQuoted _synonymType
     return $ comment <> kwTypeSynonym <+> n <+> "=" <> oneLineOrNext ty
 
 instance PrettyCode Datatype where
   ppCode Datatype {..} = do
-    comment <- ppComment _datatypeComment
+    comment <- ppJudocComment _datatypeComment
     n <- ppCode _datatypeName
     params <- ppParams _datatypeParams
     ctrs <- mapM ppCode _datatypeConstructors
     return $ comment <> kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> align (vsep (punctuate (space <> kwPipe) ctrs)))
 
 instance PrettyCode Constructor where
   ppCode Constructor {..} = do
-    comment <- ppComment _constructorComment
+    comment <- ppJudocComment _constructorComment
     n <- ppCode _constructorName
     tys <- mapM ppCodeQuoted _constructorArgTypes
     return $ comment <> hsep (n : tys)
 
 instance PrettyCode Record where
   ppCode Record {..} = do
-    comment <- ppComment _recordComment
+    comment <- ppJudocComment _recordComment
     n <- ppCode _recordName
     params <- ppParams _recordParams
     fields <- mapM ppCode _recordFields
     return $ comment <> kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
 
 instance PrettyCode RecordField where
   ppCode RecordField {..} = do
-    comment <- ppComment _recordFieldComment
+    comment <- ppJudocComment _recordFieldComment
     n <- ppCode _recordFieldName
     ty <- ppCodeQuoted _recordFieldType
     return $ comment <> n <+> "::" <+> ty

src/Juvix/Compiler/Concrete/Pretty.hs

@@ -25,4 +25,4 @@ ppTrace :: (PrettyPrint c) => c -> Text
 ppTrace = toAnsiText True . ppOut traceOptions
 
 ppPrintJudoc :: (SingI s) => Judoc s -> Text
-ppPrintJudoc = toAnsiText True . Print.ppOutJudoc
+ppPrintJudoc = toAnsiText False . Print.ppOutJudoc

tests/positive/Isabelle/isabelle/Program.thy

@@ -51,6 +51,9 @@ fun bool_fun :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
 fun bool_fun' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bool_fun' x y z = (x \<and> y \<or> z)"
 
+text \<open>
+A type of Queues
+\<close>
 datatype 'A Queue
   = queue "'A list" "'A list"
 
@@ -74,6 +77,9 @@ fun push_back :: "'A Queue \<Rightarrow> 'A \<Rightarrow> 'A Queue" where
        [] \<Rightarrow> queue [x] (qsnd q) |
        q' \<Rightarrow> queue q' (x # qsnd q))"
 
+text \<open>
+Checks if the queue is empty
+\<close>
 fun is_empty :: "'A Queue \<Rightarrow> bool" where
   "is_empty q =
     (case qfst q of
@@ -95,6 +101,9 @@ fun funkcja :: "nat \<Rightarrow> nat" where
                                   n' \<Rightarrow> n' + 1
      in plusOne n + nat1 + nat2)"
 
+text \<open>
+An Either' type
+\<close>
 datatype ('A, 'B) Either'
   = Left' 'A |
     Right' 'B