[ refactor ] IDE protocol as a separate module hierarchy (#2171)

idris2api.ipkg

@@ -129,6 +129,7 @@ modules =
     Idris.IDEMode.Holes,
     Idris.IDEMode.MakeClause,
     Idris.IDEMode.Parser,
+    Idris.IDEMode.Pretty,
     Idris.IDEMode.REPL,
     Idris.IDEMode.SyntaxHighlight,
     Idris.IDEMode.TokenLine,
@@ -159,6 +160,7 @@ modules =
     Libraries.Data.NameMap.Traversable,
     Libraries.Data.PosMap,
     Libraries.Data.Primitives,
+    Libraries.Data.Span,
     Libraries.Data.SortedMap,
     Libraries.Data.SortedSet,
     Libraries.Data.String.Extra,
@@ -190,7 +192,6 @@ modules =
     Libraries.Text.Token,
 
     Libraries.Utils.Binary,
-    Libraries.Utils.Hex,
     Libraries.Utils.Octal,
     Libraries.Utils.Path,
     Libraries.Utils.Scheme,
@@ -210,6 +211,17 @@ modules =
     Parser.Rule.Package,
     Parser.Rule.Source,
 
+    Protocol.IDE,
+    Protocol.IDE.Command,
+    Protocol.IDE.Decoration,
+    Protocol.IDE.FileContext,
+    Protocol.IDE.Formatting,
+    Protocol.IDE.Holes,
+    Protocol.IDE.Result,
+    Protocol.IDE.Highlight,
+    Protocol.Hex,
+    Protocol.SExp,
+
     TTImp.BindImplicits,
     TTImp.Elab,
     TTImp.Impossible,

idris2protocols.ipkg.hide

@@ -0,0 +1,20 @@
+package idris-protocols
+version = 0.0.1
+
+modules
+  = Protocol.Hex
+  , Protocol.IDE
+  , Protocol.IDE.Command
+  , Protocol.IDE.Decoration
+  , Protocol.SExp
+  , Libraries.Data.Span
+  , Protocol.IDE.FileContext
+  , Protocol.IDE.Formatting
+  , Protocol.IDE.Holes
+  , Protocol.IDE.Result
+  , Protocol.IDE.Highlight
+
+
+--depends =
+
+sourcedir = "src"

src/Compiler/ES/Codegen.idr

@@ -14,7 +14,7 @@ import Compiler.ES.TailRec
 import Compiler.ES.State
 import Compiler.NoMangle
 import Libraries.Data.SortedMap
-import Libraries.Utils.Hex
+import Protocol.Hex
 import Libraries.Data.String.Extra
 
 import Data.Vect

src/Compiler/RefC/RefC.idr

@@ -20,7 +20,7 @@ import Data.Vect
 import System
 import System.File
 
-import Libraries.Utils.Hex
+import Protocol.Hex
 import Libraries.Utils.Path
 
 %default covering

src/Compiler/Scheme/Chez.idr

@@ -11,7 +11,7 @@ import Core.Directory
 import Core.Name
 import Core.Options
 import Core.TT
-import Libraries.Utils.Hex
+import Protocol.Hex
 import Libraries.Utils.Path
 
 import Data.List

src/Compiler/Scheme/Gambit.idr

@@ -10,7 +10,7 @@ import Core.Directory
 import Core.Name
 import Core.Options
 import Core.TT
-import Libraries.Utils.Hex
+import Protocol.Hex
 import Libraries.Utils.Path
 
 import Data.List

src/Compiler/Scheme/Racket.idr

@@ -11,7 +11,7 @@ import Core.Context.Log
 import Core.Directory
 import Core.Name
 import Core.TT
-import Libraries.Utils.Hex
+import Protocol.Hex
 import Libraries.Utils.Path
 
 import Data.List

src/Core/Metadata.idr

@@ -15,19 +15,9 @@ import System.File
 import Libraries.Data.PosMap
 import Libraries.Utils.Binary
 
-%default covering
+import public Protocol.IDE.Decoration as Protocol.IDE
 
-public export
-data Decoration : Type where
-  Comment   : Decoration
-  Typ       : Decoration
-  Function  : Decoration
-  Data      : Decoration
-  Keyword   : Decoration
-  Bound     : Decoration
-  Namespace : Decoration
-  Postulate : Decoration
-  Module    : Decoration
+%default covering
 
 export
 nameDecoration : Name -> NameType -> Decoration
@@ -51,34 +41,6 @@ public export
 SemanticDecorations : Type
 SemanticDecorations = List ASemanticDecoration
 
-public export
-Eq Decoration where
-  Comment   == Comment   = True
-  Typ       == Typ       = True
-  Function  == Function  = True
-  Data      == Data      = True
-  Keyword   == Keyword   = True
-  Bound     == Bound     = True
-  Namespace == Namespace = True
-  Postulate == Postulate = True
-  Module    == Module    = True
-  _         == _         = False
-
--- CAREFUL: this instance is used in SExpable Decoration. If you change
--- it then you need to fix the SExpable implementation in order not to
--- break the IDE mode.
-public export
-Show Decoration where
-  show Comment   = "comment"
-  show Typ       = "type"
-  show Function  = "function"
-  show Data      = "data"
-  show Keyword   = "keyword"
-  show Bound     = "bound"
-  show Namespace = "namespace"
-  show Postulate = "postulate"
-  show Module    = "module"
-
 TTC Decoration where
   toBuf b Typ       = tag 0
   toBuf b Function  = tag 1

src/Core/Name/Namespace.idr

@@ -204,9 +204,7 @@ DecEq Namespace where
 -- TODO: move somewhere more appropriate
 export
 showSep : String -> List String -> String
-showSep sep [] = ""
-showSep sep [x] = x
-showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
+showSep sep = Libraries.Data.String.Extra.join sep
 
 export
 showNSWithSep : String -> Namespace -> String