idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 21:23:53 +03:00
Code Issues Projects Releases Wiki Activity

[ cleanup ] move DocString to Doc.String

Browse Source
This commit is contained in:
Guillaume ALLAIS 2021-05-21 11:37:08 +01:00 committed by G. Allais
parent e9f5038cb7
commit ee7956b318
9 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
idris2api.ipkg
View File

@ -73,7 +73,7 @@ modules =
Idris.Desugar.Mutual, Idris.Desugar.Mutual,
Idris.Env, Idris.Env,
Idris.Doc.HTML, Idris.Doc.HTML,
Idris.DocString, Idris.Doc.String,
Idris.Driver, Idris.Driver,
Idris.Error, Idris.Error,
Idris.ModTree, Idris.ModTree,

2
src/Idris/Desugar.idr
View File

@ -16,7 +16,7 @@ import Libraries.Data.StringMap
import Libraries.Data.String.Extra import Libraries.Data.String.Extra
import Libraries.Data.ANameMap import Libraries.Data.ANameMap
import Idris.DocString import Idris.Doc.String
import Idris.Syntax import Idris.Syntax
import Idris.Elab.Implementation import Idris.Elab.Implementation

2
src/Idris/Doc/HTML.idr
View File

@ -12,7 +12,7 @@ import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML
import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree
import Idris.DocString import Idris.Doc.String
import Idris.Package.Types import Idris.Package.Types
import Idris.Pretty import Idris.Pretty
import Idris.Version import Idris.Version

2
src/Idris/DocString.idr → src/Idris/Doc/String.idr
View File

@ -1,4 +1,4 @@
module Idris.DocString module Idris.Doc.String
import Core.Context import Core.Context
import Core.Context.Log import Core.Context.Log

2
src/Idris/IDEMode/SyntaxHighlight.idr
View File

@ -8,7 +8,7 @@ import Core.TT
import Idris.REPL import Idris.REPL
import Idris.Syntax import Idris.Syntax
import Idris.DocString import Idris.Doc.String
import Idris.IDEMode.Commands import Idris.IDEMode.Commands
import Data.List import Data.List

2
src/Idris/Package.idr
View File

@ -30,7 +30,7 @@ import Libraries.Utils.Path
import Idris.CommandLine import Idris.CommandLine
import Idris.Doc.HTML import Idris.Doc.HTML
import Idris.DocString import Idris.Doc.String
import Idris.ModTree import Idris.ModTree
import Idris.ProcessIdr import Idris.ProcessIdr
import Idris.REPL import Idris.REPL

2
src/Idris/REPL.idr
View File

@ -29,7 +29,7 @@ import Core.Unify
import Parser.Unlit import Parser.Unlit
import Idris.Desugar import Idris.Desugar
import Idris.DocString import Idris.Doc.String
import Idris.Error import Idris.Error
import Idris.IDEMode.CaseSplit import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands import Idris.IDEMode.Commands

2
src/Idris/REPL/Common.idr
View File

@ -9,7 +9,7 @@ import Core.TT
import Core.Unify import Core.Unify
import Core.UnifyState import Core.UnifyState
import Idris.DocString import Idris.Doc.String
import Idris.Error import Idris.Error
import Idris.IDEMode.Commands import Idris.IDEMode.Commands
import Idris.IDEMode.Holes import Idris.IDEMode.Holes

2
src/Idris/REPL/FuzzySearch.idr
View File

@ -16,7 +16,7 @@ import Core.TT
import Core.Unify import Core.Unify
import Idris.Desugar import Idris.Desugar
import Idris.DocString import Idris.Doc.String
import Idris.Error import Idris.Error
import Idris.IDEMode.CaseSplit import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands import Idris.IDEMode.Commands