1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Pure/Syntax/syntax.thy	Tue Mar 01 15:23:59 2011 +0100
     1.3 @@ -0,0 +1,34 @@
     1.4 +theory syntaxe imports Main begin
     1.5 +
     1.6 +section {* Old parsing *}
     1.7 +text {* Old parsing in ISAC used theories *}
     1.8 +ML {*
     1.9 +val thy = @{theory};
    1.10 +fun parse thy str = Syntax.read_term_global thy str;
    1.11 +val env = 
    1.12 +  [(parse thy "equ::bool", parse thy "x + (1::int) = 2"),
    1.13 +   (parse thy "var::int",  parse thy "x::int"),
    1.14 +   (parse thy "sol::bool", parse thy "(x::int) = 1")
    1.15 +  ];
    1.16 +val precond = parse thy "(0::int) < x"
    1.17 +*}
    1.18 +text {* However, user input could not be parsed ...*}
    1.19 +ML {* parse thy "x = 2 - 1" *}
    1.20 +text {* ... because the type 'int' is lost (we have type 'a now).
    1.21 +  The learner would need to input x::int all the time. *}
    1.22 +
    1.23 +section {* Contexts *}
    1.24 +ML {* 
    1.25 +val ctxt = ProofContext.init_global thy;
    1.26 +
    1.27 +(*... prepare ctxt ...*)
    1.28 +
    1.29 +fun parseNEW ctxt str = Syntax.read_term ctxt str;
    1.30 +*}
    1.31 +
    1.32 +section {* New parsing *}
    1.33 +text {* New parsing in ISAC uses contexts, which are rigorously updated
    1.34 +  by the Lucas-Interpreter. Then ...*}
    1.35 +ML {* parse thy "x = 2 - 1" *}
    1.36 +text {* ... x gets type 'int' from the context. *}
    1.37 +end