From f56fbcf86e472262d07c6bd713f6955cfbcfee8a Mon Sep 17 00:00:00 2001
From: Inari Listenmaa <inari.listenmaa@gmail.com>
Date: Tue, 29 Sep 2020 09:23:36 +0200
Subject: [PATCH] (Tutorial) Remove mentions to pt -typecheck

The GF shell no longer has `put_tree -typecheck` option, and typechecking is done automatically when parsing.

The metavariable thing is a bit unclear: you don't get it when parsing "dim the light", or "switch on the fan, but you do get it when you `gt` after adding `switchOn` and `switchOff`.

```
> p "switch on the fan"
CAction fan (switchOff fan) (DKindOne fan)
> gt
CAction light dim (DKindOne light)
CAction ?3 (switchOff ?3) (DKindOne ?3)
CAction ?3 (switchOn ?3) (DKindOne ?3)
```

My hypothesis is that you don't get metavariable when parsing e.g. "dim the light", because even though `light` is suppressed in `CAction`, it still appears in `DKindOne`, so it gets to contribute to the whole tree with its string.
---
 doc/tutorial/gf-tutorial.t2t | 49 ++++++++----------------------------
 1 file changed, 10 insertions(+), 39 deletions(-)

diff --git a/doc/tutorial/gf-tutorial.t2t b/doc/tutorial/gf-tutorial.t2t
index 469166090..7467e107e 100644
--- a/doc/tutorial/gf-tutorial.t2t
+++ b/doc/tutorial/gf-tutorial.t2t
@@ -3718,49 +3718,25 @@ Concrete syntax does not know if a category is a dependent type.
 ```
 Notice that the ``Kind`` argument is suppressed in linearization.
 
-Parsing with dependent types is performed in two phases:
+Parsing with dependent types consists of two phases:
 + context-free parsing
 + filtering through type checker
 
+Parsing a type-correct command works as expected:
 
-By just doing the first phase, the ``kind`` argument is not found:
 ```
   > parse "dim the light"
-  CAction ? dim (DKindOne light)
-```
-Moreover, type-incorrect commands are not rejected:
-```
-  > parse "dim the fan"
-  CAction ? dim (DKindOne fan)
-```
-The term ``?`` is a **metavariable**, returned by the parser
-for any subtree that is suppressed by a linearization rule.
-These are the same kind of metavariables as were used #Rsecediting
-to mark incomplete parts of trees in the syntax editor.
-
-
-
-#NEW
-
-===Solving metavariables===
-
-Use the command ``put_tree = pt`` with the option ``-typecheck``:
-```
-  > parse "dim the light" | put_tree -typecheck
   CAction light dim (DKindOne light)
 ```
-The ``typecheck`` process may fail, in which case an error message
-is shown and no tree is returned:
+However, type-incorrect commands are rejected by the typecheck:
 ```
-  > parse "dim the fan" | put_tree -typecheck
-
-  Error in tree UCommand (CAction ? 0 dim (DKindOne fan)) :
-    (? 0 <> fan) (? 0 <> light)
+  > parse "dim the fan"
+  The parsing is successful but the type checking failed with error(s):
+    Couldn't match expected type Device light
+       against the interred type Device fan
+    In the expression: DKindOne fan       
 ```
 
-
-
-
 #NEW
 
 ==Polymorphism==
@@ -3786,23 +3762,19 @@ to express Haskell-type library functions:
     \_,_,_,f,x,y -> f y x ;
 ```
 
-
 #NEW
 
 ===Dependent types: exercises===
 
 1. Write an abstract syntax module with above contents
 and an appropriate English concrete syntax. Try to parse the commands
-//dim the light// and //dim the fan//, with and without ``solve`` filtering.
+//dim the light// and //dim the fan//.
 
-
-2. Perform random and exhaustive generation, with and without
-``solve`` filtering.
+2. Perform random and exhaustive generation.
 
 3. Add some device kinds and actions to the grammar.
 
 
-
 #NEW
 
 ==Proof objects==
@@ -3912,7 +3884,6 @@ fun
 Classes for new actions can be added incrementally.
 
 
-
 #NEW
 
 ==Variable bindings==