summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 19:00:59 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 19:00:59 -0400
commitc954ed92f02b8947a4ff636ff10a49c3d6fb4519 (patch)
tree71d76fa0fac221faef1b3db5c749fdb0489b20f2
parent4b54ea891652138a8d58399bbbfdbb852b70eabd (diff)
Preserve tutorial indentation
-rw-r--r--doc/intro.ur20
-rw-r--r--src/tutorial.sml1
2 files changed, 20 insertions, 1 deletions
diff --git a/doc/intro.ur b/doc/intro.ur
index b9b15b72..b90e2214 100644
--- a/doc/intro.ur
+++ b/doc/intro.ur
@@ -74,7 +74,7 @@ fun compose [a] [b] [c] (f : b -> c) (g : a -> b) (x : a) : c = f (g x)
compose inc inc 3
(* end *)
-(* The "option" type family is like ML's "option" or Haskell's "maybe." Note that, while Ur follows most syntactic conventions of ML, one key difference is that type families appear before their arguments, as in Haskell. *)
+(* The "option" type family is like ML's "option" or Haskell's "maybe." We also have a "case" expression form lifted directly from ML. Note that, while Ur follows most syntactic conventions of ML, one key difference is that type families appear before their arguments, as in Haskell. *)
fun predecessor (n : int) : option int = if n >= 1 then Some (n - 1) else None
@@ -92,3 +92,21 @@ predecessor 6
(* begin eval *)
predecessor 0
(* end *)
+
+(* Naturally, there are lists, too! *)
+
+val numbers : list int = 1 :: 2 :: 3 :: []
+val strings : list string = "a" :: "bc" :: []
+
+fun length [a] (ls : list a) : int =
+ case ls of
+ [] => 0
+ | _ :: ls' => 1 + length ls'
+
+(* begin eval *)
+length numbers
+(* end *)
+
+(* begin eval *)
+length strings
+(* end *)
diff --git a/src/tutorial.sml b/src/tutorial.sml
index 8d60ed11..605b1f5e 100644
--- a/src/tutorial.sml
+++ b/src/tutorial.sml
@@ -182,6 +182,7 @@ fun doUr fname =
| #"{" => "&#123;"
| #"(" => "&#40;"
| #"\n" => "&#40;*NL*)\n"
+ | #" " => "&#40;*NL*) "
| ch => str ch) o Substring.string
val (befor, after) = Substring.position "(* begin " source