diff --git a/src/Init/Data/ByteArray/Utf8.lean b/src/Init/Data/ByteArray/Utf8.lean
index 06e09d3c9a..8467ec8cba 100644
--- a/src/Init/Data/ByteArray/Utf8.lean
+++ b/src/Init/Data/ByteArray/Utf8.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 prelude
 import Init.Data.ByteArray.Basic
 import Init.Data.List.Control
@@ -36,12 +42,10 @@ private partial def utf8ToStringAux : Nat → ByteArray → Option (List Char)
           -- parse the rest of the bytes
           bytes ← (List.range j).mapM (fun k => convertUtf8Byte utf8 (i+k+1));
           some (concatUtf8Bytes (msb :: bytes), j+1));
-    if h : isValidChar charVal then do
-      let ch : Char := ⟨charVal, h⟩;
-      tail ← utf8ToStringAux (i+nextCharOffset) utf8;
-      some (ch :: tail)
-    else
-      failure
+    ⟨h⟩ ← assert (isValidChar charVal);
+    let ch : Char := ⟨charVal, h⟩;
+    tail ← utf8ToStringAux (i+nextCharOffset) utf8;
+    some (ch :: tail)
   else
     some []
 
diff --git a/src/Lean/Data/Json/Handle.lean b/src/Lean/Data/Json/Handle.lean
index 80444fca75..137c85dc39 100644
--- a/src/Lean/Data/Json/Handle.lean
+++ b/src/Lean/Data/Json/Handle.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga
+-/
 import Init.System.IO
 import Lean.Data.Json.Parser
 import Lean.Data.Json.Printer
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 31aa08fdc1..c956c33648 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Init.Control
 import Init.System.IO
 import Std.Data.RBTree
diff --git a/src/Lean/Data/Lsp.lean b/src/Lean/Data/Lsp.lean
index d90bd0d64e..b33f8bfce3 100644
--- a/src/Lean/Data/Lsp.lean
+++ b/src/Lean/Data/Lsp.lean
@@ -1,8 +1,8 @@
 /-
-Copyright (c) 2019 Gabriel Ebner. All rights reserved.
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Authors: Gabriel Ebner, Marc Huisinga
+Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 import Lean.Data.Lsp.Basic
 import Lean.Data.Lsp.Capabilities
diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean
index 5cbe8b8760..64a3e22c5b 100644
--- a/src/Lean/Data/Lsp/Basic.lean
+++ b/src/Lean/Data/Lsp/Basic.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Lean.Data.Json
 
 /-! Defines most of the 'Basic Structures' in the LSP specification
diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index 0190865549..584599ab0f 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Lean.Data.JsonRpc
 import Lean.Data.Lsp.TextSync
 
diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean
index 5209ffa471..446243c2a4 100644
--- a/src/Lean/Data/Lsp/Communication.lean
+++ b/src/Lean/Data/Lsp/Communication.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Init.System.IO
 import Lean.Data.JsonRpc
 
diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index efa0076960..842f4edde5 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Lean.Data.Json
 import Lean.Data.Lsp.Basic
 import Lean.Data.Lsp.Utf16
diff --git a/src/Lean/Data/Lsp/Hover.lean b/src/Lean/Data/Lsp/Hover.lean
index 30026aced3..111ce5c2a1 100644
--- a/src/Lean/Data/Lsp/Hover.lean
+++ b/src/Lean/Data/Lsp/Hover.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
 import Lean.Data.Json
 import Lean.Data.Lsp.Basic
 
diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean
index 2b3f0f06a3..0b4e118047 100644
--- a/src/Lean/Data/Lsp/InitShutdown.lean
+++ b/src/Lean/Data/Lsp/InitShutdown.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Lean.Data.Lsp.Capabilities
 import Lean.Data.Lsp.Workspace
 import Lean.Data.Json
diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean
index 36b8ac0940..3c8d8835ce 100644
--- a/src/Lean/Data/Lsp/TextSync.lean
+++ b/src/Lean/Data/Lsp/TextSync.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Lean.Data.Json
 import Lean.Data.Lsp.Basic
 
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
index 7161a08c05..ce8999f079 100644
--- a/src/Lean/Data/Lsp/Utf16.lean
+++ b/src/Lean/Data/Lsp/Utf16.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Init.Data.String
 import Init.Data.Array
 import Lean.Data.Lsp.Basic
diff --git a/src/Lean/Data/Lsp/Workspace.lean b/src/Lean/Data/Lsp/Workspace.lean
index e1640a20c0..32a839d0e7 100644
--- a/src/Lean/Data/Lsp/Workspace.lean
+++ b/src/Lean/Data/Lsp/Workspace.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
 import Lean.Data.Lsp.Basic
 import Lean.Data.Json
 
diff --git a/src/Lean/Server.lean b/src/Lean/Server.lean
index f662586084..22212e8a9b 100644
--- a/src/Lean/Server.lean
+++ b/src/Lean/Server.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Marc Huisinga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga, Wojciech Nawrocki
+-/
 import Init.System.IO
 import Std.Data.RBMap
 
diff --git a/src/Lean/Server/ServerBin.lean b/src/Lean/Server/ServerBin.lean
index ee4cfa81b5..5fb2e698ee 100644
--- a/src/Lean/Server/ServerBin.lean
+++ b/src/Lean/Server/ServerBin.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
 import Init.System.IO
 import Lean.Server
 
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 96850fd8f0..4d39d3bd8f 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
 import Init.System.IO
 
 import Lean.Elab.Import