theory syntaxe imports Main begin

 section {* Old parsing *}

 text {* Old parsing in ISAC used theories *}

 ML {*

 val thy = @{theory};

 fun parse thy str = Syntax.read_term_global thy str;

 val env = 

   [(parse thy "equ::bool", parse thy "x + (1::int) = 2"),

    (parse thy "var::int",  parse thy "x::int"),

    (parse thy "sol::bool", parse thy "(x::int) = 1")

   ];

 val precond = parse thy "(0::int) < x"

 *}

 text {* However, user input could not be parsed ...*}

 ML {* parse thy "x = 2 - 1" *}

 text {* ... because the type 'int' is lost (we have type 'a now).

   The learner would need to input x::int all the time. *}

 section {* Contexts *}

 ML {* 

 val ctxt = ProofContext.init_global thy;

 (*... prepare ctxt ...*)

 fun parseNEW ctxt str = Syntax.read_term ctxt str;

 *}

 section {* New parsing *}

 text {* New parsing in ISAC uses contexts, which are rigorously updated

   by the Lucas-Interpreter. Then ...*}

 ML {* parse thy "x = 2 - 1" *}

 text {* ... x gets type 'int' from the context. *}

 end