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