From 0b9831e3c57a9a49bd5ee508febd669453e781b8 Mon Sep 17 00:00:00 2001 From: Johann Rudloff Date: Thu, 29 Apr 2021 10:47:31 +0200 Subject: [PATCH] [ refactor ] Move HTML docs specific code into its own module --- src/Idris/Doc/HTML.idr | 101 ++++++++++++++++++ src/Idris/Package.idr | 83 +------------- .../PrettyPrint/Prettyprinter/Render/HTML.idr | 16 --- 3 files changed, 105 insertions(+), 95 deletions(-) create mode 100644 src/Idris/Doc/HTML.idr diff --git a/src/Idris/Doc/HTML.idr b/src/Idris/Doc/HTML.idr new file mode 100644 index 000000000..1f6a836c5 --- /dev/null +++ b/src/Idris/Doc/HTML.idr @@ -0,0 +1,101 @@ +module Idris.Doc.HTML + +import Core.Context +import Core.Core +import Core.Directory + +import Data.Strings + +import Parser.Lexer.Source + +import Libraries.Text.PrettyPrint.Prettyprinter +import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML +import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree + +import Idris.DocString +import Idris.Pretty +import Idris.Version + +getNS : Name -> String +getNS (NS ns _) = show ns +getNS _ = "" + +hasNS : Name -> Bool +hasNS (NS _ _) = True +hasNS _ = False + +tryCanonicalName : {auto c : Ref Ctxt Defs} -> + FC -> Name -> Core (Maybe Name) +tryCanonicalName fc n with (hasNS n) + tryCanonicalName fc n | True + = do defs <- get Ctxt + case !(lookupCtxtName n (gamma defs)) of + [(n, _, _)] => pure $ Just n + _ => pure Nothing + tryCanonicalName fc n | False = pure Nothing + +packageInternal : {auto c : Ref Ctxt Defs} -> + Name -> Core Bool +packageInternal (NS ns _) = + do let mi = nsAsModuleIdent ns + catch ((const True) <$> nsToSource emptyFC mi) (\_ => pure False) +packageInternal _ = pure False + +prettyNameRoot : Name -> String +prettyNameRoot n = + let root = nameRoot n in + if isOpName n then "(" ++ root ++ ")" else root + +renderHtml : {auto c : Ref Ctxt Defs} -> + SimpleDocTree IdrisDocAnn -> + Core String +renderHtml STEmpty = pure neutral +renderHtml (STChar c) = pure $ cast c +renderHtml (STText _ text) = pure text +renderHtml (STLine _) = pure "
" +renderHtml (STAnn Declarations rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" +renderHtml (STAnn (Decl n) rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" +renderHtml (STAnn DocStringBody rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" +renderHtml (STAnn DCon rest) = do + resthtml <- renderHtml rest + pure $ "" <+> resthtml <+> "" +renderHtml (STAnn (TCon n) rest) = do + pure $ "" <+> (prettyNameRoot n) <+> "" +renderHtml (STAnn (Fun n) rest) = do + pure $ "" <+> (prettyNameRoot n) <+> "" +renderHtml (STAnn Header rest) = do + resthtml <- renderHtml rest + pure $ "" <+> resthtml <+> "" +renderHtml (STAnn (Syntax (SynRef n)) rest) = do + resthtml <- renderHtml rest + Just cName <- tryCanonicalName emptyFC n + | Nothing => pure $ "" <+> resthtml <+> "" + True <- packageInternal cName + | False => pure $ " (htmlEscape $ show cName) <+> "\">" <+> (htmlEscape $ nameRoot cName) <+> "" + pure $ "" <+> (htmlEscape $ nameRoot cName) <+> "" +renderHtml (STAnn ann rest) = do + resthtml <- renderHtml rest + pure $ "" ++ resthtml ++ "" +renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs) + +export +docDocToHtml : {auto c : Ref Ctxt Defs} -> + Doc IdrisDocAnn -> + Core String +docDocToHtml doc = + let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in + renderHtml dt + +export +htmlPreamble : String -> String -> String -> String +htmlPreamble title root class = "" + ++ "" ++ htmlEscape title ++ "" + ++ "" + ++ "" + ++ "
Idris2Doc : " ++ htmlEscape title + ++ "
" + ++ "
" + +export +htmlFooter : String +htmlFooter = "
" diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index f29f4b4e9..074ff398e 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -15,7 +15,6 @@ import Data.Maybe import Data.Strings import Data.These -import Parser.Lexer.Source import Parser.Package import System import System.Directory @@ -25,21 +24,18 @@ import Libraries.Data.StringMap import Libraries.Data.StringTrie import Libraries.Text.Parser import Libraries.Text.PrettyPrint.Prettyprinter -import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML -import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree import Libraries.Utils.Binary import Libraries.Utils.String import Libraries.Utils.Path import Idris.CommandLine +import Idris.Doc.HTML import Idris.DocString import Idris.ModTree -import Idris.Pretty import Idris.ProcessIdr import Idris.REPL import Idris.REPL.Common import Idris.REPL.Opts -import Idris.Resugar import Idris.SetOptions import Idris.Syntax import Idris.Version @@ -416,77 +412,6 @@ check pkg opts = runScript (postbuild pkg) pure [] -getNS : Name -> String -getNS (NS ns _) = show ns -getNS _ = "" - -hasNS : Name -> Bool -hasNS (NS _ _) = True -hasNS _ = False - -tryCanonicalName : {auto c : Ref Ctxt Defs} -> - FC -> Name -> Core (Maybe Name) -tryCanonicalName fc n with (hasNS n) - tryCanonicalName fc n | True - = do defs <- get Ctxt - case !(lookupCtxtName n (gamma defs)) of - [(n, _, _)] => pure $ Just n - _ => pure Nothing - tryCanonicalName fc n | False = pure Nothing - -packageInternal : {auto c : Ref Ctxt Defs} -> - Name -> Core Bool -packageInternal (NS ns _) = - do let mi = nsAsModuleIdent ns - catch ((const True) <$> nsToSource emptyFC mi) (\_ => pure False) -packageInternal _ = pure False - -prettyNameRoot : Name -> String -prettyNameRoot n = - let root = nameRoot n in - if isOpName n then "(" ++ root ++ ")" else root - - -renderHtml : {auto c : Ref Ctxt Defs} -> - SimpleDocTree IdrisDocAnn -> - Core String -renderHtml STEmpty = pure neutral -renderHtml (STChar c) = pure $ cast c -renderHtml (STText _ text) = pure text -renderHtml (STLine _) = pure "
" -renderHtml (STAnn Declarations rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" -renderHtml (STAnn (Decl n) rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" -renderHtml (STAnn DocStringBody rest) = pure $ "
" <+> !(renderHtml rest) <+> "
" -renderHtml (STAnn DCon rest) = do - resthtml <- renderHtml rest - pure $ "" <+> resthtml <+> "" -renderHtml (STAnn (TCon n) rest) = do - pure $ "" <+> (prettyNameRoot n) <+> "" -renderHtml (STAnn (Fun n) rest) = do - pure $ "" <+> (prettyNameRoot n) <+> "" -renderHtml (STAnn Header rest) = do - resthtml <- renderHtml rest - pure $ "" <+> resthtml <+> "" -renderHtml (STAnn (Syntax (SynRef n)) rest) = do - resthtml <- renderHtml rest - Just cName <- tryCanonicalName emptyFC n - | Nothing => pure $ "" <+> resthtml <+> "" - True <- packageInternal cName - | False => pure $ " (htmlEscape $ show cName) <+> "\">" <+> (htmlEscape $ nameRoot cName) <+> "" - pure $ "" <+> (htmlEscape $ nameRoot cName) <+> "" -renderHtml (STAnn ann rest) = do - resthtml <- renderHtml rest - pure $ "" ++ resthtml ++ "" -renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs) - -docDocToHtml : {auto c : Ref Ctxt Defs} -> - Doc IdrisDocAnn -> - Core String -docDocToHtml doc = - let ds = layoutUnbounded doc - dt = SimpleDocTree.fromStream ds in - renderHtml dt - makeDoc : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> @@ -514,13 +439,13 @@ makeDoc pkg opts = addImport (MkImport emptyFC False mod ns) defs <- get Ctxt names <- allNames (gamma defs) - let allNs = filter (inNS ns) names - allNs <- filterM (visible defs) allNs + let allInNamespace = filter (inNS ns) names + visibleNames <- filterM (visible defs) allInNamespace writeHtml $ htmlPreamble (show mod) "../" "namespace" writeHtml ("

" ++ show mod ++ "

") writeHtml ("
") - ignore $ for (sort allNs) (\name => do + ignore $ for (sort visibleNames) (\name => do doc <- getDocsForName emptyFC name writeHtml !(docDocToHtml doc) ) diff --git a/src/Libraries/Text/PrettyPrint/Prettyprinter/Render/HTML.idr b/src/Libraries/Text/PrettyPrint/Prettyprinter/Render/HTML.idr index 53d131a23..0750518be 100644 --- a/src/Libraries/Text/PrettyPrint/Prettyprinter/Render/HTML.idr +++ b/src/Libraries/Text/PrettyPrint/Prettyprinter/Render/HTML.idr @@ -3,8 +3,6 @@ module Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML import Data.List import Data.Strings -import Idris.Version - export htmlEscape : String -> String htmlEscape s = fastAppend $ reverse $ go [] s @@ -36,17 +34,3 @@ htmlEscape s = fastAppend $ reverse $ go [] s (safe, rest) => let c = assert_total (strIndex rest 0) escaped = htmlQuote c in go (escaped::safe::acc) (assert_total $ strTail rest) - -export -htmlPreamble : String -> String -> String -> String -htmlPreamble title root class = "" - ++ "" ++ htmlEscape title ++ "" - ++ "" - ++ "" - ++ "
Idris2Doc : " ++ htmlEscape title - ++ "
" - ++ "
" - -export -htmlFooter : String -htmlFooter = "
"