Fix code blocks in the documentation

A previous commit disabled indentation-based code blocks because it's 
incompatible with liquid template inclusion.

This commit replaces all indented code blocks by backticks-surrounded 
code blocks. It also adds missing language declarations (for syntax 
highlighting) and removes some annoying extra indentation.

docs/blog/_posts/2016-02-03-essence-of-scala.md

@@ -24,34 +24,34 @@ has been machine-checked for correctness.
 A calculus is a kind of mini-language that is small enough to be
 studied formally. Translated to Scala notation, the language covered
 by DOT is described by the following abstract grammar:
-
-    Value       v  =  (x: T) => t            Function
-                      new { x: T => ds }     Object
-
-    Definition  d  =  def a = t              Method definition
-                      type A = T             Type
-
-    Term        t  =  v                      Value
-                      x                      Variable
-                      t1(t2)                 Application
-                      t.a                    Selection
-                      { val x = t1; t2 }     Local definition
-
-    Type        T  =  Any                    Top type
-                      Nothing                Bottom type
-                      x.A                    Selection
-                      (x: T1) => T2          Function
-                      { def a: T }           Method declaration
-                      { type T >: T1 <: T2 } Type declaration
-                      T1 & T2                Intersection
-                      { x => T }             Recursion
-
+```
+Value       v  =  (x: T) => t            Function
+                  new { x: T => ds }     Object
+
+Definition  d  =  def a = t              Method definition
+                  type A = T             Type
+
+Term        t  =  v                      Value
+                  x                      Variable
+                  t1(t2)                 Application
+                  t.a                    Selection
+                  { val x = t1; t2 }     Local definition
+
+Type        T  =  Any                    Top type
+                  Nothing                Bottom type
+                  x.A                    Selection
+                  (x: T1) => T2          Function
+                  { def a: T }           Method declaration
+                  { type T >: T1 <: T2 } Type declaration
+                  T1 & T2                Intersection
+                  { x => T }             Recursion
+```
 The grammar uses several kinds of names:
-
-    x      for (immutable) variables
-    a      for (parameterless) methods
-    A      for types
-
+```
+x      for (immutable) variables
+a      for (parameterless) methods
+A      for types
+```
 The full calculus adds to this syntax formal _typing rules_ that
 assign types `T` to terms `t` and formal _evaluation rules_ that
 describe how a program is evaluated. The following _type soundness_
@@ -67,12 +67,12 @@ because it uncovered some technical challenges that had not been
 studied in depth before. In DOT - as well as in many programming languages -
 you can have conflicting definitions. For instance you might have an abstract
 type declaration in a base class with two conflicting aliases in subclasses:
-
-     trait Base { type A }
-     trait Sub1 extends Base { type A = String }
-     trait Sub2 extends Base { type A = Int }
-     trait Bad extends Sub1 with Sub2
-
+```scala
+trait Base { type A }
+trait Sub1 extends Base { type A = String }
+trait Sub2 extends Base { type A = Int }
+trait Bad extends Sub1 with Sub2
+```
 Now, if you combine `Sub1` and `Sub2` in trait `Bad` you get a conflict,
 since the type `A` is supposed to be equal to both `String` and `Int`. If you do
 not detect the conflict and assume the equalities at face value you
@@ -108,10 +108,10 @@ project are important.
     Nominal typing means that a type is distinguished from others
     simply by having a different name.
     For instance, given two trait definitions
-
-          trait A extends AnyRef { def f: Int }
-          trait B extends AnyRef { def f: Int }
-
+    ```scala
+    trait A extends AnyRef { def f: Int }
+    trait B extends AnyRef { def f: Int }
+    ```
     we consider `A` and `B` to be different types, even though both
     traits have the same parents and both define the same members.
     The opposite of
@@ -143,4 +143,3 @@ project are important.
     either to increase our confidence that they are indeed sound, or
     to show that they are unsound. In my next blog I will
     present some of the issues we have discovered through that exercise.
-

docs/blog/_posts/2016-02-17-scaling-dot-soundness.md

@@ -17,14 +17,14 @@ guidelines on how to design a sound type system for full Scala.
 As was argued in the previous blog post, the danger a path-dependent type
 system like Scala's faces is inconsistent bounds or aliases. For
 instance, you might have a type alias
-
-      type T = String
-
+```scala
+type T = String
+```
 in scope in some part of the program, but in another part the same
 type member `T` is known as
-
-      type T = Int
-
+```scala
+type T = Int
+```
 If you connect the two parts, you end up allowing assigning a `String`
 to an `Int` and vice versa, which is unsound - it will crash at
 runtime with a `ClassCastException`. The problem is that there
@@ -51,17 +51,17 @@ a type selection might _not_ be a value that's constructed with a
 categories:
 
  1. The prefix value might be lazy, and never instantiated to anything, as in:
-
-        lazy val p: S = p
-        ... p.T ...
-
+    ```scala
+    lazy val p: S = p
+    ... p.T ...
+    ```
     Note that trying to access the lazy value `p` would result in an infinite loop. But using `p` in a type does not force its evaluation, so we might never evaluate `p`. Since `p` is not initialized with a `new`, bad bounds for `T` would go undetected.
 
  2. The prefix value might be initialized to `null`, as in
-
-        val p: S = null
-        ... p.T ...
-
+    ```scala
+    val p: S = null
+    ... p.T ...
+    ```
     The problem here is similar to the first one. `p` is not initialized
     with a `new` so we know nothing about the bounds of `T`.
 
@@ -73,16 +73,20 @@ at the discussion for issues [#50](https://github.com/lampepfl/dotty/issues/50)
 and [#1050](https://github.com/lampepfl/dotty/issues/1050) in the
 [Dotty](https://github.com/lampepfl/dotty/issues/1050) repository
 on GitHub. All issues work fundamentally in the same way: Construct a type `S`
-which has a type member `T` with bad bounds, say
+which has a type member `T` with bad bounds, say:
 
-    Any <: T <: Nothing
+```scala
+Any <: T <: Nothing
+```
 
 Then, use the left subtyping to turn an expression of type `Any` into
 an expression of type `T` and use the right subtyping to turn that
 expression into an expression of type `Nothing`:
 
-    def f(x: Any): p.T = x
-    def g(x: p.T): Nothing = x
+```scala
+def f(x: Any): p.T = x
+def g(x: p.T): Nothing = x
+```
 
 Taken together, `g(f(x))` will convert every expression into an
 expression of type `Nothing`. Since `Nothing` is a subtype of every
@@ -150,10 +154,3 @@ should make sure not to back-slide. And if the experience of the past
 10 years has taught us one thing, it is that the meta theory of type
 systems has many more surprises in store than one might think. That's
 why mechanical proofs are essential.
-
-
-
-
-
-
-

docs/blog/_posts/2016-05-05-multiversal-equality.md

@@ -24,14 +24,14 @@ How can `==` be fixed? It looks much harder to do this than adding an alternate
 
 The current status in Scala is that the compiler will give warnings for _some_ comparisons that are always `false`. But the coverage is weak. For instance this will give a warning:
 
-```
+```scala
 scala> 1 == "abc"
 <console>:12: warning: comparing values of types Int and String using `==' will always yield false
 ```
 
 But this will not:
 
-```
+```scala
 scala> "abc" == 1
 res2: Boolean = false
 ```
@@ -45,29 +45,29 @@ I believe to do better, we need to enlist the cooperation of developers. Ultimat
 
 The best known way to characterize such relationships is with type classes. Implicit values of a trait `Eq[T, U]` can capture the property that values of type `T` can be compared to values of type `U`. Here's the definition of `Eq`
 
-```
+```scala
 package scala
 
 trait Eq[-T, -U]
 ```
 
 That is, `Eq` is a pure marker trait with two type parameters and without any members.  Developers can define equality classes by giving implicit `Eq` instances. Here is a simple one:
 
-```
+```scala
 implicit def eqString: Eq[String, String] = Eq
 ```
 
 This states that strings can be only compared to strings, not to values of other types.  Here's a more complicated `Eq` instance:
 
-```
+```scala
 implicit def eqOption[T, U](implicit _eq: Eq[T, U]): Eq[Option[T], Option[U]] = Eq
 ```
 
 This states that `Option` values can be compared if their elements can be compared.
 
 It's foreseen that such `Eq` instances can be generated automatically. If we add an annotation `@equalityClass` to `Option` like this
 
-```
+```scala
 @equalityClass class Option[+T] { ... }
 ```